suggest to report column number for warnings
ID0002268: This issue was created automatically from Mantis Issue 2268. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002268 | Frama-C | Plug-in > Eva | public | 2017-01-09 | 2017-03-06 |
| Reporter | Jochen | Assigned To | yakobowski | Resolution | won't fix |
| Priority | low | Severity | feature | Reproducibility | N/A |
| Platform | xubuntu | OS | - | OS Version | - |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
I suggest to print the column number in addition to the line number at each warning of the value analysis' batch (i.e. non-gui) version. This feature could be made on/off-switchable via a command line option. I guess it is easy to implement.
The interest in this information is motivated by an attempt to compare warning counts for (e.g.) "out of bounds read" between Frama-C and Polyspace. The latter aggregates all warnings referring to the same code location into a single one. Obtaining comparable counts from Frama-C can be done by appropriate postprocessing of its stdout stream. However, Frama-C warnings that refer to the same line, but different columns, shouldn't be joined into a single one, since Polyspace e.g. emits and counts 2 warnings for the code "a = b[i] + c[i]" when both array accesses may be out of bounds. Having both line and column number in Frama-C warnings would allow one to exactly duplicate the counting method of Polyspace.