[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [csmith-dev] Generating ACSL \assigns clauses with programs
Csmith's analysis is more concrete than what Robert wants. It wouldn't be too hard for Csmith to report that "*p is modified" instead of "the real objects represented by *p are modified".
From: Yang Chen [mailto:firstname.lastname@example.org]
Sent: Friday, November 6, 2015 6:14 PM
To: Xuejun Yang <email@example.com>
Cc: John Regehr <firstname.lastname@example.org>; email@example.com
Subject: 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.