--- layout: fc_discuss_archives title: Message 32 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,

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.

De : frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la part de Xiao-lei Cui
Envoy? : jeudi 12 d?cembre 2013 07:25
? : frama-c-discuss at lists.gforge.inria.fr
Objet : [Frama-c-discuss] ACSL annotation for making function calls

Hi all,
   I often struggle with annotating function calls in ACSL, due to my inexperience.  I am not sure if it is necessary to reference the pre and post conditions of the callee(e.g. bar1, bar2 in the code below) in the annotation for the caller.
   For instance , given the code below, what is the proper way to annotate function foo()?
   Thanks!
cheers,
xiao-lei
-----------------------------
/*@ contract for bar1*/
extern int bar1(int);

/*@ contract for bar2*/
extern int bar2(int);

/*@ how to deal with bar1 and bar2 ??*/
int foo(int x){
  int y;
  if x==0 {
     y= bar1(x);
     return y;
   }
  y = bar2(x);
  return y;
}

Theory is when you know all and nothing works.
Practice is when all works and nobody knows why.
In this case, we have put together theory and practice: nothing works... and nobody knows why!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131212/42e36b97/attachment.html>