--- layout: fc_discuss_archives title: Message 92 from Frama-C-discuss on November 2013 ---
As a follow-up to the post below, I find that why3IDE pops up without throwing any proof obligations, only when the header(.h) file folders are being processed, not for .c source files. And no header file contains any ACSL annotation. cheers, xiaolei From: x_cui at hotmail.com To: frama-c-discuss at lists.gforge.inria.fr Date: Tue, 12 Nov 2013 22:31:11 -0500 Subject: [Frama-c-discuss] why3IDE interactive proof session popup 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131113/9a6bd620/attachment.html>