--- layout: fc_discuss_archives title: Message 77 from Frama-C-discuss on March 2009 ---
Hello, I try to verify the simple search programm below. 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? - 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? What else should I annotate to verify the code? With Spec#, Boogie and Z3 I was able to verify the C# version of this. gWhy with Z3 however didn't terminate (see https://gforge.inria.fr/tracker/index.php?func=detail&aid=7533&group_id=1123&atid=5488) -Boris ------------------------- #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; while(i<aLength) { if(a[i] == val) return true; else i++; } return false; }