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] Displaying property status for rte annotations

Hello,

On 12/02/2011 01:06 PM, Virgile Prevosto wrote:
> On 02/12/2011 12:51, Sergio Feo wrote:
>> VALID or NOT VALID. However, they are not visible when running Frama-C
>> from the command line with 'frama-c -rte -val rte_test.c'.
>>
>> The program analyzed is a minimal example with a division where rte
>> generates the assertion that the divisor is not 0. The result of issuing
>> that command is the output of the value analysis plug-in but no mention
>> of the generated assertions is made. The use of the 'report' plug-in
>> also yields no results ("No status to report" is displayed).
>
> The issue is that the order in which rte, val and report will be
> launched is not specified, as these are three independent analyses
> operating at the same stage (see Frama-C's developer manual section 5.13
> for more info about the various stages of a Frama-C run).
>
> It is possible to instruct Frama-C to perform the analyses in a
> specified order with the -then option:
>
> frama-c -rte rte_test.c -then -val -then -report

Virgile is fully right.

In addition to his answer, note that running 'frama-c-gui -rte -val 
rte_test.c' only works by chance since it is not specified than the RTE 
plug-in is launched before Value Analysis. You have to use -then to 
force the order. With your configuration, RTE is launched first in GUI 
mode, but not in the toplevel mode.

To show you how unspecified it is, the order in which plug-ins are 
launched depends on:
- whether a plug-in is dynamic;
- whether a plug-in has a GUI;
- whether you run frama-c-gui or frama-c;
- the alphabetical ordering of plug-in names;
- the order in which plug-ins are declared in the Frama-C Makefile
- the options -add-path, -load-script and -load-module put on the 
command line, and their respective ordering
- the contents of the environment variable FRAMAC_PLUGIN

So I guess that nobody, even a Frama-C expert, is able to infer quickly 
the order in which plug-ins are launched ;-)).

Best regards,
Julien