--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on February 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Strange results



On Fri, Feb 8, 2013 at 12:59 PM, Anne Pacalet <anne.pacalet at free.fr> wrote:
> So it means that I mustn't trust to much the GUI... to bad :-(

To explain in a bit more detail what happens, let us write \U(e) the
join of the evaluation of e in all possible states for the chosen
statement.
What is displayed by the gui is
- \U( v ) is e is a syntactically constant variable v
- \U( t[ \U(i) ])  if e == t[i]
- \U( (* (\U(p))).a ) if p == p->a
etc. So when p is not constant, instead of seing \U(p -> a) as you
might want, you see the over-approximation above.

Hope this clarifies things,

-- 
Boris