--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on December 2013 ---
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>