--- layout: fc_discuss_archives title: Message 121 from Frama-C-discuss on November 2013 ---
Hi, Thanks for the hints. I will try to move ACSL annotations to the header files. However, I have another question for annotating function calls. for instance, extern void g(void); extern int h(void); int f(void){ //@ asserts pre-condition-of (g) ? g(); //@ asserts post-condition-of (g) ? return (h()); /*how to specify the return value here?*/ } Thanks :) cheers, xiaolei -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131127/980e10a0/attachment.html>