Profile

Cover photo
Iago Abal
Lives in EU
39,172 views
AboutPostsPhotosVideosReviews

Stream

Iago Abal

Shared publicly  - 
 
A compilation of 26 historical (single thread) double lock #bugs in #Linux. #EBA finds 22 of those.
bench-cstdl - A benchmark of single-thread double lock bugs.
1
Add a comment...

Iago Abal

Shared publicly  - 
 
Nice tool for testing command line applications.

For instance, I'm starting to use tests like

  $ cp -r "$TESTDIR"/linux .

  $ eba -L linux/cmt_speech.i 2>/dev/null | grep -A 2 "Double lock"
  Double lock (*) (glob)
  first at drivers/hsi/clients/cmt_speech.c:443
  second at drivers/hsi/clients/cmt_speech.c:407

to check that my changes to #EBA don't make it miss any previously detected bug.
Cram: It's test time. Cram is a functional testing framework for command line applications. Cram tests look like snippets of interactive shell sessions. Cram runs each command and compares the command output in the test with the command's actual output. Here's a snippet from Cram's own test ...
1
Add a comment...

Iago Abal

Shared publicly  - 
 
#EBA reported an spurious double-lock bug here, because from the context of `data_xfer' nothing indicates that `&acdev->host->lock' and `qc->ap->lock' are the same lock. Anyways, EBA still pointed out a situation that it's confusing for humans as well, and that deserved a cleanup patch.
1
Add a comment...

Iago Abal

Shared publicly  - 
 
What does it mean for software to be correct? Is this building "correct"? What about a bridge, can it be "correct"?

This said by a big (academic) name in software testing. Very much agree, in engineering we can achieve reliability, but not correctness. Correctness is a mathematical concept.
1
Add a comment...

Iago Abal

Shared publicly  - 
 
Indeed. I believe the use of __restrict in C would help, but it's not very popular.
I came across an article yesterday about programming languages, which hit on one of my major peeves, so I can’t resist responding. The article is at greythumb.org, and it’s called [Programmer’s rant: what should and should not be added to C/C++](http://www.greythumb.org/blog/index.php?/archives/152-Programmers-rant-what-should-and-should-not-be-added-to-CC++.html#extended). It’s a variation on the extremely common belief that C and C++ are the…
1
Add a comment...

Iago Abal

Shared publicly  - 
 
Do you manage to understand the flow of control?
Paste:#2002560112719298560; Author:Anonymous Coward; Language:C; Channel:-; Created:2016-05-19 15:17:27 UTC. 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 ...
1
Add a comment...

Communities

4 communities

Iago Abal

Shared publicly  - 
 
Insightful comment according to Slashdot crowd:

"University professors are under constant pressure to come up with something interesting to show they are a world class expert in their field. And grad students who do most of the grunt work are under pressure to prove themselves as well. So this is yet another impractical technique."
the_newsbeagle writes: By gaining access to the sensors in someone's smart watch, hackers could track the person's hand movements at an ATM and figure out his/her pin. The hacker needn't be anywhere near the ATM; data can be lifted from the smart watch by either a discreet wireless sniffer or by mal...
1
Add a comment...

Iago Abal

Shared publicly  - 
 
Another double spin_lock fixed in a #Linux #driver thanks to #EBA!
1
Add a comment...

Iago Abal

Shared publicly  - 
 
Second bug-fix submitted thanks to #EBA !
1
Add a comment...

Iago Abal

Shared publicly  - 
2
Add a comment...

Iago Abal

Shared publicly  - 
 
Happy to announce bv 0.4.1, a maintenance release that:

* Fixes compilation error with GHC 8.0.1; and
* Allows the user to disable index bounds checking (with -f -check-bounds).
Name, Description, Default, Type. gmp, Using Integer GMP backend. Enabled, Automatic. test, Build the test suite, and an executable to run it. Disabled, Manual. check-bounds, Bounds checking. Enabled, Manual. dev, Development options. Disabled, Manual. Use -f to enable a flag, ...
1
Add a comment...

Iago Abal

Shared publicly  - 
 
It seems that after dead code elimination, and unused structure fields elimination, EBA analyzed all the Linux files I tried in less than 3 seconds!
eba - EBA: An effect-based static analyzer for C.
1
Add a comment...
Communities
4 communities
Work
Occupation
Software Engineering & Formal methods
Places
Map of the places this user has livedMap of the places this user has livedMap of the places this user has lived
Currently
EU
Links
Other profiles
Contributor to
Story
Tagline
Computer Engineer, Formal Methods Advocate, and Functional Programmer
Introduction
I'm looking for lightweight approaches to formal methods that are useful for building today's software.
Education
  • 5-year Degree in Computer Engineering, 2004 - 2012
Basic Information
Gender
Male
A Loja do Cidadám nom atopa-se onde indíca-se, senón á beira do Distrital de Sam Marcos.
Public - 5 years ago
reviewed 5 years ago
It's name is "Granjinhos". I think would be good to point that there is the "loja do cidad~ao" building, since it is very intesting place for some foreigns.
Public - 6 years ago
reviewed 6 years ago
2 reviews
Map
Map
Map