Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL annotation for making function calls

Hello Xiao-Lei,

Le 13/12/2013 06:27, Xiao-lei Cui a ?crit :
> But I still find it difficult to write post-conditions for foo(). In
> this case, the return value from bar1 and bar2 impact the value of x.
> How could we handle the function calls here?  As the code complexity
> grows, e.g. caller calls multiple functions which in turn call other
> functions,  then, writing post-condition could be headache:(   is
> there structured way of doing it?

Once again, your example is too abstract. Why do you do x=x-y? Why do 
you do x=x+y? Please find in attached file some (proved) contracts filed 
for foo()[1]. But don't ask me if they could be useful for anything. :-)

In regular programming, you use bar1() and bar2() to divide your complex 
foo() work item into simpler work items. You have a logic behind that, 
and that is this logic that you should put into barX() contracts. In 
other words, if you use barX() functions to do some work, you should 
state declaratively the result of this work into absX() post-conditions. 
And those post-conditions should be enough to prove your foo() 
post-conditions.


Best regards,
david


[1] Restriction of x to SHORT_MIN..SHORT_MAX is only here to easily 
ensure absence of Run Time Error.
-------------- next part --------------
#include <limits.h>

/*@ requires x==0;
    assigns \nothing;
    ensures \result==x;
 */
 extern int bar1(int x);

/*@ requires x!=0;
    assigns \nothing;
    ensures \result==-x;
 */
 extern int bar2(int x);

/*@ requires x >= SHRT_MIN && x <= SHRT_MAX;
    behavior equal_zero:
        assumes x==0;
        ensures \result == x;
    behavior non_zero:
        assumes x!=0;
        ensures \result == -\old(x);
 */
int foo(int x){
  int y;
  if (x==0) {
      y= bar1(x);
      x= x+y;
      return y;
  }
  y = bar2(x);
  x=x-y;
  return y;
}