Assertion on pointer to array

Question

I have defined the following function which is well proved by frama-c:

//ensures array <= \result < array+length && *\result == element;
/*@
  requires 0 < length;
  requires \valid_read(array + (0 .. length-1));

  assigns  \nothing;

  behavior in:
    assumes \exists int off ; 0 <= off < length && array[off] == element;
    ensures *\result == element;

  behavior notin:
    assumes \forall int off ; 0 <= off < length ==> array[off] != element;
    ensures \result == 0;

  disjoint behaviors;
  complete behaviors;
*/
int* search(int* array, int length, int element){
   int *tmp;
  /*@
    loop invariant 0 <= i <= length;
    loop invariant \forall int j; 0 <= j < i ==> array[j] != element;
    loop assigns i;
    loop variant length-i;
  */ 
  for(int i = 0; i < length; i++)
  {
    if(array[i] == element) 
    {
        tmp = &array[i];
        //@ assert *tmp==element;
    }
    else
    {
        tmp = 0;    
    }
  }
  return tmp;
}

and I use it in the following main entry:

int main(){
  int arr[5]={1,2,3,4,5};
  int *p_arr;

  p_arr = search(arr,5,4);
  //@ assert *p_arr==30;

  return 0
}

I am wondering why frama-c give the assertion "//@ assert *p_arr==30;" as true, I do not understand.

Thanks

Which version of frama-c? with which options? who says the assertion is valid: WP ? — Anne
Thank you for your reply, the version is phosphorus, the option is: frama-c-gui -wp -rte -val <file.c>, the bullet on the GUI is orange. Is that enough info for you ? — Laurent Guillaume
I would say the bullet is green at the assertion line, sorry — Laurent Guillaume
After further analysis It seems the green bullet does not match the real status , value said "unknown" for this assertion it is not WP.=> p_arr ∈ {{ NULL ; &arr[3] }} => unknown — Laurent Guillaume
Use the -slevel option to have more precise result with -val: for instance, add -slevel 100 to your options. Don't know why the bullet is green in the GUI though (cannot try it now). — Anne

Anne Anne · Accepted Answer · 2017-09-07T09:43:47

Using the command line only, I saw some problems in your code:

tmp is missing in the loop assigns;
you need to:
- either add a break in the then branch of the seach function (then you would return the pointer on the first element that match)
- or initialize tmp = 0 at the beginning of the function and remove the else branch in the loop (then you would return a pointer on the last occurrence).

I didn't try the GUI, but it seems strange that you say that your example is:

well proved by frama-c

I suggest that you use the command line to begin with.

Assertion on pointer to array

2 Answers