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

Re: [csmith-dev] Generating ACSL \assigns clauses with programs

Hi Robert, this is cool!  I hope we can help Csmith do what you want.
Although it seems like perhaps a weird way to do it, one idea you should keep in mind is instrumenting the program to record dynamic pointer behaviors, running it, and then using that information to create annotations. This would give you some insulation against imprecisions in Csmith's analyses for example. Also, by giving you an underapproximation instead of an overapproximation it would let you test Frama-C in the opposite direction. 

John



On 11/6/15 5:12 PM, Robert Clausecker wrote:

Greeting from Berlin!

I'm a student working for the Fraunhofer FOKUS research institute. I
currently work on a project where I want to use csmith to generate test
cases for the C static-analysis framework Frama C, specifically the WP
plugin. For this purpose, I want to expand csmith to generate ACSL [1]
annotations for the functions it generates. One of the annotations I
want to generate are \assigns clauses that specify what objects a
function assigns to. Generating these clauses has proven to be somewhat
tricky: while csmith keeps record of what objects a function modifies, I
haven't found a way to find out the expression through which this
modification is being performed. For example, if csmith generated these
two functions:

     int z;

     void foo()
     {
         int x;

         bar(&x);
     }

     void bar(int *y)
     {
         y = 0;
         z = 0;
     }

it would report that bar() modified x, but the identifier x is not in
scope in bar. Is there an easy way to find out what objects a function
mutates on its own, i.e. without the context of how it is called? For
example, for bar() I would like to receive information of the form "bar
mutates z and *y," specifically without making assumptions about the
place y points to.

I tried to work myself through the csmith source code, but I am a bit
overwhelmed and was so far not able to find the information I need.

Thank you for your help,
Your sincerely,
Robert Clausecker

[1]: https://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Language