Frama-C Do two jobs, and do them well In the previous post, I used the command: $ cat log? | grep \N " | sort | uniq This may be an inefficient way to get a list of unique lines containing "N ". The command sort does not know that it...
Read MoreIntroduction In the first post in the obfuscated animated donut series my colleague Anne pointed out that: The alarm about : assert \valid(". -~:;=!*#$@"+tmp_7); seems strange because the analysis tells us that tmp_7 ∈ [0..40] at this point... How can this be valid ? It is only safe to use...
Read MoreAnother facetious colleague reports a strange behavior with the following C program: int main (void) { int x = 100; int y = 042; int z = 005; printf (\%d" x+y+z); return (x+y+z) - 147; }
Read MoreA facetious colleague reports the following program as a bug: int main () { signed char c=0; while(1) c++; return 0; } The commandline frama-c -val -val-signed-overflow-alarms charpp.c, he says, does not emit any alarm for the c++; instruction. Indeed, the c++; above is equivalent to c = (signed char)...
Read More