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

  • Subject: [Frama-c-discuss] ACSL annotation for making function calls
  • From: x_cui at hotmail.com (Xiao-lei Cui)
  • Date: Thu, 12 Dec 2013 01:25:29 -0500
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/82473010/attachment.html>