Re: [csmith-dev] Generating ACSL \assigns clauses with programs

[Xuejun Yang <xuyang@microsoft.com>]

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

-Xuejun

-----Original Message-----
From: Yang Chen [mailto:chenyang@cs.utah.edu] 
Sent: Friday, November 6, 2015 6:14 PM
To: Xuejun Yang <xuyang@microsoft.com>
Cc: John Regehr <regehr@cs.utah.edu>; csmith-dev@flux.utah.edu
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.

- Yang