suggest to report column number for warnings
ID0002268: This issue was created automatically from Mantis Issue 2268. Further discussion may take place here.
|ID0002268||Frama-C||Plug-in > Eva||public||2017-01-09||2017-03-06|
|Reporter||Jochen||Assigned To||yakobowski||Resolution||won't fix|
|Product Version||Frama-C 14-Silicon||Target Version||-||Fixed in Version||-|
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.