--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on February 2013 ---
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