[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