--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on December 2013 ---
[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.