[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.
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 
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
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,