Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002259Frama-CPlug-in > Evapublic2016-11-28 12:572017-12-17 21:05
Assigned Toyakobowski 
PlatformOSOS Version
Product VersionFrama-C Aluminium 
Target VersionFrama-C 15-PhosphorusFixed in Version 
Summary0002259: suggest to provide and document a unique warning string to grep for in value-analysis output files
DescriptionWhen running Frama-C value analysis with parameters that cause a huge output file, it is not possible to read thourgh it line by line. (My current output file, "results.txt.gz", has the size 700 MB in gzipped format) In this case, it is only possible to use tools like "zgrep -10 -n -i 'warning:' results.txt.gz >resultsExcerpt.txt" to find relevant messages. The value analysis manual suggests (on p.41) to grep for "assert" to get all messages that relate to a proof obligation. However, warnings about non-terminating functions are not found this way, so at least another grep for "terminat" seems necessary. More important, I can't be not sure that "assert" and "terminat" will cover all relevant messages. Therefore I suggest to provide a single search string that will appear at every relevant message. It shouldn't fit into C's variable name syntax (so 'warning:' is ok, but 'warning' is not). It should be mentioned in the manual at a prominent place when discussing the batch (i.e. non-gui) version of value analysis; it is an essential part of the methodology then. If there are several such strings (e.g. for different degrees of severity, like 'error:' or 'hint:'), they should all be documented in that same place. A user who has read this documentation part should be confident about how to catch all relevant messages.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
Jochen (reporter)
2016-11-28 16:45

By the way: I wonder why nothing is said in the manual about warnings for unreachable code, except on p.52-53 that valuae analysis can't be used for termination proofs. Isn't there any message printed when Frama-C detects that some statements within a function body cannot be reached (except for possibly "NON TERMINATING FUNCTION" at the very end of the function)? Apparently, the program "int main(int a) { if (a) { while (1) ; return 2; } else { return 3; } }" doesn't cause any warning, although Frama-C recognizes that the "return 2" isn't reachable.
maroneze (administrator)
2016-11-29 18:54

The lack of feedback concerning non-termination has indeed been noticed by some users, and the upcoming release (Silicon) already incorporates a plug-in (called Nonterm) that runs after Value and emits messages such as the one you described, although not necessarily in the format you suggested. For instance, in your example program, it reports: filep.c:1:[nonterm] warning: non-terminating loop stack: main It is a very young plug-in and thus it has some rough edges, but it should help with the methodology. It reports cases of definitive non-termination. In a simple test, it can be run with `frama-c file.c -val -then -nonterm`, but in a more complex setting its output could be copied to a specific file, using `-nonterm-log :nonterm.log` for instance. The upcoming Value analysis manual mentions this plug-in in a section called "Non-termination". The manual is not available yet, but the Silicon-rc1 version is already available on GitHub (
yakobowski (manager)
2017-03-06 11:09

Hi Jochen, We have improved things in Silicon, and will improve them further in Phosphorus: - in Phosphorus, option -val-show-progress will be unset by default. This will shrink down the logs considerably - all _alarms_ are now emitted as ACSL assertions, so it is always possible to use the 'Properties' tab of the GUI to find them. The log is no longer needed. - alarms can be emitted as standard messages using the option -no-val-warn-on-alarms. This way, the other warnings of Value become much more visible. I'm leaving this issue open so that we document this properly in the Phosphorus manual.
yakobowski (manager)
2017-12-17 21:05

Fixed in the last versions. The log should always be of a reasonable size.

- Issue History
Date Modified Username Field Change
2016-11-28 12:57 Jochen New Issue
2016-11-28 12:57 Jochen Status new => assigned
2016-11-28 12:57 Jochen Assigned To => yakobowski
2016-11-28 16:45 Jochen Note Added: 0006290
2016-11-29 18:54 maroneze Note Added: 0006294
2017-03-06 11:09 yakobowski Note Added: 0006371
2017-03-06 11:36 yakobowski Target Version => Frama-C 15-Phosphorus
2017-12-17 21:05 yakobowski Note Added: 0006489
2017-12-17 21:05 yakobowski Status assigned => closed
2017-12-17 21:05 yakobowski Resolution open => fixed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker