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