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] use of frama-c GUI

On Thu, Apr 7, 2011 at 3:15 PM, SENE, Sali <sali.sene at airbus.com> wrote:

> I used the Frama-C command line to analyse my C code, everything was ok.
> Now I try to use the Frama-C gui to make value analysis and run time errors
> analysis, but I get something like this I don?t understand why.
>

The statements displayed in red have been found to be unreachable by the
value analysis.

The two reasons why a statement may be found to be unreachable by the value
analysis are:
- it really is not intended to be reached in a normal execution, or
- it occurs after an unintended systematic undefined behavior, which, in the
value analysis, stops the execution (in a real execution, undefined
behaviors do not always stop execution; this is the biggest problem with
undefined behaviors).

If you are following the tutorial, you are in the first case: the function
you have selected is not reachable. Start your observations from main() and
only descend into functions that are actually called.

Besides, you are invoking the Rte and value analysis plug-in at the same
time. This does not make sense : Rte emits alarms for all dangerous
constructions (that it knows of) found syntactically in the program. The
value analysis emits alarms only for the dangerous constructions (that it
knows of) that appear to be reachable with dangerous arguments. Either
choose Rte and check the emitted alarms with the method of your choice, or
choose the value analysis and then, absence of undefined behaviors has been
checked when the value analysis does not emit any alarm.

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110407/17303c80/attachment.htm>