--- layout: fc_discuss_archives title: Message 60 from Frama-C-discuss on August 2015 ---
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>