Frama-C Bug Tracking System - Frama-C
View Issue Details
0002259Frama-CPlug-in > Evapublic2016-11-28 12:572017-12-17 21:05
Jochen 
yakobowski 
normaltextN/A
closedfixed 
Frama-C Aluminium 
Frama-C 15-Phosphorus 
0002259: suggest to provide and document a unique warning string to grep for in value-analysis output files
When 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.
No tags attached.
Issue History
2016-11-28 12:57JochenNew Issue
2016-11-28 12:57JochenStatusnew => assigned
2016-11-28 12:57JochenAssigned To => yakobowski
2016-11-28 16:45JochenNote Added: 0006290
2016-11-29 18:54maronezeNote Added: 0006294
2017-03-06 11:09yakobowskiNote Added: 0006371
2017-03-06 11:36yakobowskiTarget Version => Frama-C 15-Phosphorus
2017-12-17 21:05yakobowskiNote Added: 0006489
2017-12-17 21:05yakobowskiStatusassigned => closed
2017-12-17 21:05yakobowskiResolutionopen => fixed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0006290)
Jochen   
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.
(0006294)
maroneze   
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 (https://github.com/Frama-C/Frama-C-snapshot/tree/release-candidates).
(0006371)
yakobowski   
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.
(0006489)
yakobowski   
2017-12-17 21:05   
Fixed in the last versions. The log should always be of a reasonable size.