Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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
>