[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[csmith-dev] Csmith-proof Frama-C released

Dear Csmith user,

you have found a great tool in Csmith. It finds tons of differences
between the compiler you are interested in testing and the reference
implementation of your choice. For each of them, you reduce
the program a bit between sending it off for someone else to treat
as a bug, or before donning your compiler debugger's hat.

There is still a slight problem, though. Csmith generates only
defined programs by design, but is the program still defined
once you have reduced it? The compiler debugger does not
like it one bit when you send an undefined program, regardless
of whether you send it to someone else or to yourself with
a funny hat.

It is not obvious to recognize an undefined program
at first sight. You may be forgiven for failing to, and the compiler
debugger does probably not recognize it immediately.
This is why he gets so angry and shouts that you should have
checked that the program was defined. He doesn't know
how to do it either.

Let me tell you (again) about Frama-C's value analysis. It is a static
analyzer with a big round button in the middle for precision.
If you turn the button all the way to the right, it becomes as precise as
executing the program — indeed, it executes the program, statement
after tedious statement. But it never lets an undefined behavior
slip by without saying something (*).

All this is old. Frama-C was alluded to before in this mailing list.
So what's new? The new thing is that it is now available from

The only required dependency is a recent OCaml, that you may
get in binary form for your commercial OS from INRIA, or
directly from your Open-Source Unix distribution.


~/csmith$ src/csmith --no-argc --no-volatiles -s 20111001 > t.c
~/csmith$ frama-c -val -val-signed-overflow-alarms -unspecified-access -obviously-terminates -machdep x86_64 -cpp-command "gcc -C -E -m64 -Dprintf=Frama_C_show_each -Iruntime" -precise-unions -big-ints-hex 0 -no-val-show-progress t.c
(no warning with the word "assert")
[value] Called Frama_C_show_each({{ &"checksum = %X\n" }},{0x9D2E015A})

This means that the Csmith program is defined and computes 0x9D2E015A as

The option -unspecified-access can sometimes cause warnings for
programs that are defined, but it should never let a program undefined
because of unsequenced side-effects unwarned. Other undefined
behaviors that can be found in a Csmith program should all be detected

The value analysis should work fine for already reduced programs
(the usage I am recommending here). If you are going to use it a lot,
there are tricks to make it a bit faster (tricks in addition to the already
long command-line above, I mean). But I should really stop before
the rightful owners of this mailing list boot me o

(*) terms and conditions apply. Any undefined program obtained
by reducing a Csmith program for which the value analysis
terminates normally without emitting a message with the word
"assert" is a bug and can be reported as such to be promptly