--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on July 2010 ---
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>