--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on October 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP plugin / question about address of variable on stack



Le 17/10/2011 10:40, sylvain nahas a ?crit :
> Still, I would really like to know the actual definition of \valid in
> the Frama-C framework.
> Does it only cover positive non zero integers or is there other constraints?

I think that \valid(p) holds at program points where
the memory location (*p) is allocated.

Hope this helps,
-- 
Anne.