suggest to provide and document a unique warning string to grep for in value-analysis output files
ID0002259: This issue was created automatically from Mantis Issue 2259. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002259 | Frama-C | Plug-in > Eva | public | 2016-11-28 | 2017-12-17 |
| Reporter | Jochen | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | text | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Aluminium | Target Version | Frama-C 15-Phosphorus | Fixed in Version | - |
Description :
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.