[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[csmith-dev] Generating ACSL \assigns clauses with programs
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