--- layout: fc_discuss_archives title: Message 109 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



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
>