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