[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [csmith-dev] Generating ACSL \assigns clauses with programs
Hi Robert,
Take a look of FactMgr::map_stm_effect. I think it has the info you needed.
Csmith performs path-sensitive inter-procedural analysis. It is realized with the following steps:
1) Caller (foo) to callee (bar) handover, where foo passes the knowledge, e.g., y is pointing to x, to bar;
2) Effect analysis in bar;
3) Callee (bar) to caller (foo) handover, where bar tells foo that x is modified.
For details, check FunctionInvocationUser::revisit.
-Xuejun
-----Original Message-----
From: csmith-dev-bounces@flux.utah.edu [mailto:csmith-dev-bounces@flux.utah.edu] On Behalf Of John Regehr
Sent: Friday, November 6, 2015 2:30 PM
To: csmith-dev@flux.utah.edu
Subject: 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
>