--- layout: fc_discuss_archives title: Message 116 from Frama-C-discuss on November 2013 ---
Hi, > In fact my advice is not good, sorry. The good practice should be to > deal with each .c file one at a time, provided that the contracts for > all functions are put in the header files .h. This would a true modular > approach. What you advised is certainly more structured way to annotate C code. Just be certain I get the idea: in each folder that contains C code, I shall call frama-c for each C file like frama-c -jessie -pp-annot file1.c frama-c -jessie -pp-annot file2.c ... ... And for contracts for each function, I have only seen examples that shows how to embed them along with the function body. are you suggesting put the contract along with the function prototype in some header file(.h), rather than put them in the .c file? Thank you cheers xiaolei > Date: Sat, 16 Nov 2013 09:44:09 +0100 > From: Claude.Marche at inria.fr > To: frama-c-discuss at lists.gforge.inria.fr > Subject: Re: [Frama-c-discuss] why3IDE interactive proof session popup > > > In fact my advice is not good, sorry. The good practice should be to > deal with each .c file one at a time, provided that the contracts for > all functions are put in the header files .h. This would a true modular > approach. > > - Claude > > On 11/16/2013 09:39 AM, Claude Marche wrote: > > > > I'm not sure I understand what you are trying to do. But I think you > > should pass all your sources within a single invocation of frama-c, for > > example > > > > frama-c -jessie *.c */*.c > > > > (or better, list precisely the directories where the sources are) > > > > Moreover, passing included files like .h ones is probably useless > > > > - Claude > > > > On 11/13/2013 04:31 AM, Xiao-lei Cui wrote: > >> Hi All, > >> I wrote a script to process, using frama-c/jessie, a folder that > >> contains sub-folders recursively, as follows: > >> #-------------------------------------------------------- > >> trav() > >> { > >> for x in $(ls) > >> do > >> if [ -f "$x" ];then > >> echo "$x"; > >> elif [ -L "$x" ];then > >> echo "this is a link"; > >> else > >> cd "$x"; > >> pwd; > >> frama-c -jessie -pp-annot *.h; > >> frama-c -jessie -pp-annot *.c; > >> trav; > >> cd .. > >> fi > >> done > >> } > >> trav > >> #---------------------------------------------------------- > >> As the script runs through the entire folder, why3IDE pops up > >> after each sub-folder being processed. In many cases, the proof session > >> coming up contains no proof obligation. It shows the .mlw file > >> processed, plus jessie model and jessie program (as in the attached > >> screen capture ). To continue with the processing, I simply use ctrl+q > >> to quit the session. This isn't strange because I disabled most of the > >> ACSL annotation for now. However, I just want to be certain I did it in > >> a reasonable way and not miss anything important. Also, is there some > >> short-cut way to work around the pop-ups, instead of quitting manually:) > >> Thanks.. > >> > >> cheers, > >> xiaolei > >> > >> > >> _______________________________________________ > >> Frama-c-discuss mailing list > >> Frama-c-discuss at lists.gforge.inria.fr > >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > >> > > > > _______________________________________________ > > Frama-c-discuss mailing list > > Frama-c-discuss at lists.gforge.inria.fr > > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131119/a3b0b39b/attachment.html>