Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] arrays in structures

  • Subject: [Frama-c-discuss] arrays in structures
  • From: agoodloe at gmail.com (Alwyn Goodloe)
  • Date: Wed, 28 Jul 2010 08:10:29 -0400
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>