--- layout: fc_discuss_archives title: Message 78 from Frama-C-discuss on March 2009 ---
Hello Hollas, I'm just another Frama-C user, so my reply is not authoritative. On Wed, Mar 25, 2009 at 15:56, Hollas Boris (CR/AEY1) <Boris.Hollas at de.bosch.com> wrote: > Running Simplify results in two ? signs: > > - when I click on the first "?" labeled "postcondition", the following code is highlighted: > > insVal(int a[], int aLength, int val) { > ?int i = 0; > > ?//@ loop in > > ?I don't understand what that means. Is this a bug in gWhy's highlighting? I ran[1] your example on my own installation of Frama-C, the following code is highlighted[2]: "\result == true <==> \exists int j; 0 <= j <= aLength-1 && a[j] =" which means the postcondition "ensures \result == true <==> \exists int j; 0 <= j <= aLength-1 && a[j] == val;" is not verified. So you might have an issue with your setup of Frama-C. > - the second "?" is labeled "pointer dereferencing" and corresponds to > ? ? ?if(a[i] == val) return true; > ?Does this mean that frama-c doesn't detect that i<aLength holds at this point? More exactly, the "if" is highlighted and in the upper right corner you see "offset_min(int_P_a_20_alloc_table, a) <= integer_of_int32(i_27_0)" It means that you must check that "i" does not access a[] outside of a[] lower boundary. You should add a loop invariant: "loop invariant i >= 0;" With this added invariant, all properties are proven: ---- #define true 1 #define false 0 typedef int bool; /*@ requires \valid(a+ (0..aLength-1)); ensures \result == true <==> \exists int j; 0 <= j <= aLength-1 && a[j] == val; */ bool ContainsVal(int a[], int aLength, int val) { int i = 0; /*@ loop invariant \forall int j; 0 <= j <= i-1 ==> a[j] != val; loop invariant i >= 0; g */ while(i<aLength) { if(a[i] == val) return true; else i++; } return false; } ------ Sincerely yours, david [1] Command line: frama-c -jessie-analysis -jessie-std-stubs -jessie-atp alt-ergo -jessie-cpu-limit 2 -jessie-gui hollas-containsval.c [2] This is a known bug: https://gforge.inria.fr/tracker/index.php?func=detail&aid=7496&group_id=1123&atid=5488