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

-- Boris Yakobowski (2015-08-28)
> On Fri, Aug 28, 2015 at 6:46 AM, Tim Newsham <tim.newsham at gmail.com <mailto: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.

FWIW, I find this behavior too surprising to be good for an analyzer. We've thought a lot about it in our work on SPARK, and we've come up with a quite satisfying separation between 
- info messages (displayed in green in the IDE): information about the analysis that is useful to understand the results (for example, proved "checks" as described below can be displayed as info messages)
- warning messages (displayed in yellow in the IDE): possible problems in the program, where the decision to display them may be heuristic driven, and the messages may be incomplete (for example for dead code)
- check messages (displayed in red in the IDE): failure to prove with certainty that the property of interest (the "check", be it run-time check or assertion) always holds, which are all issued

Of course, you may want to add levels to check and warning messages, and that's what we do (low / medium / high).

> 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"

That's what I'd call an info message. Something you can ignore if you're only interested in a sound analysis of the properties of interest to you, and nothing else.

> (2) the plugin has found something suspicious in the code; for Value, typically an alarm or an unknown assertion

That's what I'd call a check message.

> (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

We issue some of those as warnings when they have a local impact (say, assuming that an external function has no effect on global variables), but our general solution is to list separately all those assumptions, so that they can be reviewed or justified separately (say, by testing). For example, an assumption is generated for every pragma Assume in the code (it would be an assume annotation in E-ACSL I guess).

> (3) the plugin does something completely unsound to avoid stopping (for Value, mostly recursive calls)

I agree you should issue a warning here (maybe even IN CAPITAL LETTERS IN THAT CASE).

> 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.

Hard to follow if you ask me! :)
--
Yannick Moy, Senior Software Engineer, AdaCore




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