--- layout: fc_discuss_archives title: Message 77 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Jessie] Problem with simple search programm



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;
}