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

Hi Dillon,
?? Thanks for the hints!!
?? Following the steps you suggested, I invoked the frama-c gui tool, but? by right-click on the "y = bar1();" , I did not have the option "insert callees contract (all calls)"? in context menu.? There is a option: "prove preconditions with WP".? Perhaps I missed something..? Any ideas? Or alternative way to try it?
?
>? When using WP plug-in, upwarding the callees' contracts is done for you automatically.
?? WP indeed work something out by itself, for example, foo.c below, there is no annotation for function foo(). The result from below shows the pre-condition of callees are checked and proved. But the callee will affect the post-condition of caller, what then? could be done to specify the caller's post-conditions properly? 

thanks.
cheers
xiao-lei

--------------------------------------------------------------------------------
$ frama-c -pp-annot -wp -wp-print -wp-prover cvc3 foo.c
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_foo_call_bar1_pre : Valid
[wp] [Qed] Goal typed_foo_call_bar2_pre : Valid (4ms)
------------------------------------------------------------
? Function foo
------------------------------------------------------------

Goal bar1_pre: Pre-condition (file foobar.c, line 1) in 'foo' at call 'bar1' (file foobar.c, line 17):
Assume { }
Prove: true.
Prover Qed returns Valid

------------------------------------------------------------

Goal bar2_pre: Pre-condition (file foobar.c, line 7) in 'foo' at call 'bar2' (file foobar.c, line 20):
Assume { (* foobar.c:16: Else *) Have: 0!=x_3. }
Prove: true.
Prover Qed returns Valid (4ms)

--------------------------
/*@ 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);


int foo(int x){
? int y;
? if (x==0) {
????? y= bar1(x);
????? return y;
? }
? y = bar2(x);
? return y;
}
-------------------------------



-----------------------------------------------------------------------------------------------------------------------------------
From: Dillon.Pariente at dassault-aviation.com
To: frama-c-discuss at lists.gforge.inria.fr
Date: Thu, 12 Dec 2013 08:11:02 +0000
Subject: Re: [Frama-c-discuss] ACSL annotation for making function calls

Hi,
?
Let?s try on this code:
?
//@ requires x==0; assigns \nothing;ensures \result>=0;
extern int bar1(int x);
?
//@ requires x!=0; assigns \nothing;ensures \result<0;
extern int bar2(int x);
?
int foo(int x){
? int y;
? if (x==0) {????? y= bar1(x);????? return y;??? }
? y = bar2(x);
? return y;
}?? 

?
When using WP plug-in, upwarding the callees' contracts is done for you automatically.
?
If you want to give a look to what happens ?for real?, you can try the following:
frama-c-gui foo.c
and then right-click on the "y = bar1();" statement for instance,
and then select "insert callees contract (all calls)" contextual menu item.
This should insert automatically the callees' contracts with due substitutions.
?
HTH,
D.



________________________________
> From: Dillon.Pariente at dassault-aviation.com 
> To: frama-c-discuss at lists.gforge.inria.fr 
> Date: Thu, 12 Dec 2013 08:11:02 +0000 
> Subject: Re: [Frama-c-discuss] ACSL annotation for making function calls 
>  
>  
> Hi, 
>  
>  
>  
> Let?s try on this code: 
>  
>  
>  
> //@ requires x==0; assigns \nothing;ensures \result>=0; 
>  
> extern int bar1(int x); 
>  
>  
>  
> //@ requires x!=0; assigns \nothing;ensures \result<0; 
>  
> extern int bar2(int x); 
>  
>  
>  
> int foo(int x){ 
>  
>    int y; 
>  
>    if (x==0) {      y= bar1(x);      return y;    } 
>  
>    y = bar2(x); 
>  
>    return y; 
>  
> } 
>  
>  
>  
> When using WP plug-in, upwarding the callees' contracts is done for you  
> automatically. 
>  
>  
>  
> If you want to give a look to what happens ?for real?, you can try the  
> following: 
>  
> frama-c-gui foo.c 
>  
> and then right-click on the "y = bar1();" statement for instance, 
>  
> and then select "insert callees contract (all calls)" contextual menu item. 
>  
> This should insert automatically the callees' contracts with due  
> substitutions. 
>  
>  
>  
> HTH, 
>  
> D. 
>