Re: [csmith-dev] Systems without variadic functions?, was Re: arthur's bugs

[Pascal Cuoq <pascal.cuoq@gmail.com>]

On Sat, Apr 30, 2011 at 12:05 AM, Pascal Cuoq <pascal.cuoq@gmail.com> wrote:

>> This is very convenient for systems that do not handle
>> variadic functions very well,

On Sat, Apr 30, 2011 at 11:37 PM, Arthur O'Dwyer
<arthur.j.odwyer@gmail.com> wrote:

> What's an example of a system that
> doesn't "handle variadic functions very well"?

Hello, Arthur.

I have been using Csmith to test Frama-C, an Open Source framework in
which a bunch of static analysis techniques and transformations for C
programs are implemented.

The static analyzer I have been testing is the value analysis plug-in,
which computes and records values that variables can take at run-time
in a C program http://frama-c.com/value.html .
This analyzer is supposed to be sound (all the values
that happen in an execution are predicted by the analyzer), when used
within some limits. And unfortunately, variadic functions are outside
these limits (there hasn't been any demand for them from our usual
industrial partners. The current applications of Frama-C are for
embedded C code).

Csmith-generated programs, with their current use of printf, are
within the limits of programs that are supposed to be handled (the
other prominent value analysis limitation is recursion, which they do
not use).  Since the value analysis is supposed to be sound, whenever
a program, when compiled and run, displays some behavior that was not
predicted, it's a bug.  John and I have found tens of bugs this way,
in the value analysis itself and in Frama-C's front-end.
Here is what a typical one looks like once reduced:
http://bts.frama-c.com/view.php?id=798
(bug reduction is as much a problem for me as for people who
test C compilers, and I am very much looking forward to improvements
that apply to my use).

As of mid-April, the value analysis has reached the point where you
can spend weeks of CPU time throwing Csmith programs at it without
uncovering issues, so I have moved on to other Frama-C
plug-ins that produce testable results: a slicing plug-in, and a
constant propagation plug-in, both of which are supposed to produce
a compilable, executable C program in some sense equivalent to the
original (again something that can be tested automatically).

The next Frama-C release will owe a lot to Csmith and its developers.