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