--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on July 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] arrays in structures



In trying to understand what happens when valid_range applied is to an
array
in a structure I did the following experiment with
generating the proof conditions in PVS.

For    int a[3];     \valid_range(a,0,2) will (after some unfolding)
produces the
completely understandable proof obligation


{-1}  offset_min[int_P](int_P_a_1_alloc_table!1, a) <= 0 AND
       offset_max[int_P](int_P_a_1_alloc_table!1, a) >= 2
        ........

  |-----------------

[1] offset_min[int_P](int_P_a_1_alloc_table!1, a) <= 0


But for   struct SS {a[3];} ;
             struct SS xx;

I write
/*@ assert  \valid_range(xx.a,0,2); */

and I thought I would have gotten the same pretty much the same thing, but
nope
the consequent is basically the same, but the antecedent only has the bounds
on the
xx

{-1}  offset_min[SS](SS_xx_1_alloc_table, xx) <= 0 AND
       offset_max[SS](SS_xx_1_alloc_table, xx) >= 0

and never mentions the array xx.a and thus the proof becomes stuck.
So I'm guessing that the I need to say more in the assertion or
use something other than valid_range.  Any suggestions would be helpful
since it's kinda preventing me rolling out the tool for others to use.


-A



-- 
Alwyn E. Goodloe, Ph.D.
agoodloe at gmail.com

Computer Scientist
National Institute of Aerospace
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100728/6ac3f153/attachment.htm>