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