--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on December 2011 ---
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>