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

- Yang