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] arbitrary buffers in analysis

On Fri, Aug 28, 2015 at 6:46 AM, Tim Newsham <tim.newsham at gmail.com> wrote:

> I looked into this and to my surprise frama-c's textual output
> doesnt include a warning for this unverified assertion, but when
> I loaded it up in the gui, it was clearly marked as yellow.  I had
> previously assumed that no warnings in the output meant that
> everything was good. Is there a way to force warnings in the
> output for all unverified assertions?
>
>
Not at the current time.

There are four competing semantics for plugin "warnings", and only two
possibilities in Frama-C API (warning/error). This explains some of the
inconsistencies one may encounter. The four semantics are:
(1) the plugin loses precision, which may impact the results; for Value,
this is typically the family of messages "too many locations to enumerate"
(2) the plugin has found something suspicious in the code; for Value,
typically an alarm or an unknown assertion
(3) the plugin makes an hypothesis on the code (for example "no aliasing")
and proceeds under this hypothesis ; I don't think Value has those, except
perhaps the generation of assigns clauses for functions without
specifications
(3) the plugin does something completely unsound to avoid stopping (for
Value, mostly recursive calls)

It may be argued that type (2) information should not be reported by the
plugin as warnings, because there is nothing to warn about: this is the
normal behavior of the plugin to find such information. Value is a bit
schizophrenic on this point, because alarms are reported as warnings, and
unknown statuses on existing ACSL assertions are reported as information.

The recommended way to find whether something is not proven at the end of
the analysis is
- using the Properties tab of the GUI, with appropriate filters to remove
"Valid", "Untried", "Dead", "Considered Valid" statuses, plus
Reachable/Generated/Not generated properties.
- using the report plugin ; some options are also available to remove
uninteresting properties

Currently, a few alarms cannot be reported in ACSL, so you also need to
grep the analysis log. Hopefully, this won't be necessary in Aluminium.

(It seems that all the good stuff will be in Aluminium and none in
Magnesium. Rest assured it is not the case :-) )

HTH,

-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150828/30891dae/attachment.html>