How to give the right precondition to prove an assert statemnt in frama-c?

Question

I have been working on some basic programs in c to verify using the frama-c tool.I wanted to know why the assertion is not being proved in the program.Thanks in advance.

#include <limits.h>

/*@requires \valid(a) && \valid(b) && \separated(a,b);
 assigns \nothing;
 ensures (*a>*b ==> \result == *b) &&
        (*b>=*a ==> \result == *a);
*/

int max_ptr(int* a,int* b){
  return (*a>*b)?*b:*a;
}

extern int h;

//@assigns x;
int main(){
h=42;

 int a=24;
 int b=42;

 //@assert h ==42;
  int x;
  x=max_ptr(&a,&b);

  //@ assert x == 42;
  //@ assert h ==42;

  return 0;
}

All the scheduled goals were successfully proved but except for the assertion statement:

//@ assert x == 42;

It was a timeout on the above assertion.Should there be any modifications to the function contract?

Answer 1

The assertion is not proved because it does not hold. Your max_ptr function actually computes the minimum of both pointed values, so x == 24 at the assertion point.

Automatic provers can rarely tell when something is false, instead of simply not being able to prove it.

If you use WP, it will be unable to prove the assertion, but this won't tell you whether it is false, or just hard to prove. Some tools may help finding counterexamples and getting some false statuses to appear, but by default WP's provers will simply say unknown.

Checking some properties using an automatic value analysis, such as Eva

If you run Eva (with -eva), in your program you will get an Invalid property. You can use the GUI to inspect the value of x at the program point (in the Values tab) and you will see that its value is {24}. Then you can backtrack using the GUI to find out when this value got there, using for instance a right-click on the x and then Dependencies -> Show defs.