--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on December 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



All hints provided below are highly valuables.
Two additional pennies:
 - you can double-click into the proof obligation to show pretty-printed logic formulae to be discharged
 - in those formulae, you can figure out traces of the Pre- and Post- conditions of callers.

Regarding how to write ACSL contracts, may I suggest you to have a look at Fraunhofer ACSL tutorial:
http://www.dcc.fc.up.pt/~nam/aulas/0910/vfs/teoricas/acsl-by-example-4_2_1.pdf

Regards, L.




________________________________
De : frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] de la part de Pariente Dillon [Dillon.Pariente at dassault-aviation.com]
Date d'envoi : jeudi 12 d?cembre 2013 09:11
? : Frama-C public discussion
Objet : 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.

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/8c8d5d58/attachment.html>