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

should do what you want. Note that rte_test.c must be placed before the 
first -then (otherwise, your initial project would not have any source 
file. See user manual section 3.3.1 for more information about -then and 
its project-aware sibling -then-on)

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile