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 Xiao-Lei,

> but? by right-click on the "y = bar1();" , I did not have the option
> "insert callees contract (all calls)"? in context menu.?

This feature is at least available in Frama-C v. Fluorine.

> ?? 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?

As David mentioned before, it depends on what one wants to prove as post-condition for the caller (and thus the behavior of the caller function from the given callsite to the return control point(s)).

In your example, (without any consideration to ACSL behavior feature or even assigns - side-effects - clauses) one might simply specify foo() as:

/*@
 ensures x==0 ==> \result==x;
 ensures x!=0 ==> \result==-x;
*/
int foo(int x){ 
...}

As Lo?c said, one may give a look to the Fraunhofer ACSL tutorial (which requires before to invest a bit in deductive verification theory, Hoare's logic principles, ...).

Best,
D.