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

  • Subject: [Frama-c-discuss] Displaying property status for rte annotations
  • From: arenis at informatik.uni-freiburg.de (Sergio Feo)
  • Date: Fri, 2 Dec 2011 12:51:01 +0100
  • In-reply-to: <CAK2NOcX7pO+7L6a_t6fOL5xAc6HgBoX4hkCfcc5SoiFfsEDJ5w@mail.gmail.com>
  • References: <CAK2NOcX7pO+7L6a_t6fOL5xAc6HgBoX4hkCfcc5SoiFfsEDJ5w@mail.gmail.com>
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>