[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [csmith-dev] Generating ACSL \assigns clauses with programs
On 2015-11-06 17:32, Xuejun Yang wrote:
Csmith's analysis is also context sensitive, but it produces a
context-insensitive effect summary for a function by merging effects
from all contexts. That summary is kept in Function::feffect.
Actually Function::feffect is printed out as comments when we print
the function. Isn't that enough for your purpose?
If I am correct, that's not what Robert wants. In his example, Csmith
would produce that "x" is modified by function bar. However, Robert
doesn't want to know the object that pointer p points to.