--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on December 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Displaying property status for rte annotations



Hi everyone,
I would like to ask a (hopefully) simple question for Frama-C experts:

How do you tell the command-line version of Frama-C to display the status
of the assertions generated by the RTE plug-in?. The results are visible in
the GUI when invoked with 'frama-c-gui -rte -val rte_test.c' (there are
color swatches next to the generated assertions indicating 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).

Thank you very much,
Sergio

========= SAMPLE RTE_TEST.C =======
int x = 0;
int y = 0;

void foo()
{
 if (y==0) y=1;
}

int main()
{
 int result;
 foo();
// Assertion y != 0 is inserted here by RTE, gives the result VALID
 result = x / y;
 return 0;
}
======== END SAMPLE ========
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111202/9278bb10/attachment.htm>