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