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



In fact my advice is not good, sorry. The good practice should be to 
deal with each .c file one at a time, provided that the contracts for 
all functions are put in the header files .h. This would a true modular 
approach.

- Claude

On 11/16/2013 09:39 AM, Claude Marche wrote:
>
> 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
>>
>
> _______________________________________________
> 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