--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on December 2013 ---
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/42e36b97/attachment.html>