--- layout: fc_discuss_archives title: Message 91 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131112/85f7d777/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screenshot from 2013-11-13 104014.png
Type: image/png
Size: 173303 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131112/85f7d777/attachment-0001.png>