Frama-C Bug Tracking System - Frama-C
View Issue Details
0002423Frama-CPlug-in > reportpublic2019-01-22 16:092019-01-24 10:33
closedno change required 
linux ubuntu4.18
Frama-C 18-Argon 
Frama-C 19-Potassium 
0002423: option -report-csv doesn't work anymore ?
this option seems to be deprecated now ...
I know there is a new option to make report with Eva but only for red alarms and only with eva - I want a complete report as before with -report-csv
There is no indication at all in the changelog or maybe I've missed something ?
Is there a new way to use this option or another option to have the same result ?
No tags attached.
Issue History
2019-01-22 16:09pmoNew Issue
2019-01-22 16:09pmoStatusnew => assigned
2019-01-22 16:09pmoAssigned To => correnson
2019-01-23 10:15pmoNote Added: 0006735
2019-01-23 10:43pmoNote Deleted: 0006735
2019-01-23 10:46signolesAssigned Tocorrenson => maroneze
2019-01-23 10:49signolesTarget Version => Frama-C 19-Potassium
2019-01-23 11:26maronezeNote Added: 0006737
2019-01-23 11:32maronezeNote Edited: 0006737bug_revision_view_page.php?bugnote_id=6737#r383
2019-01-23 14:16pmoNote Added: 0006738
2019-01-23 16:41maronezeNote Added: 0006739
2019-01-23 16:42maronezeNote Edited: 0006739bug_revision_view_page.php?bugnote_id=6739#r385
2019-01-23 16:42maronezeNote Edited: 0006739bug_revision_view_page.php?bugnote_id=6739#r386
2019-01-23 16:44maronezeNote Edited: 0006739bug_revision_view_page.php?bugnote_id=6739#r387
2019-01-23 16:44maronezeNote Edited: 0006739bug_revision_view_page.php?bugnote_id=6739#r388
2019-01-23 17:14pmoNote Added: 0006740
2019-01-24 10:33maronezeStatusassigned => closed
2019-01-24 10:33maronezeResolutionopen => no change required

2019-01-23 11:26   
(edited on: 2019-01-23 11:32)
The option has not been deprecated (-report-h shows it normally), and there is one test in which it is used, and also as part of the template for analysis-scripts. So, unless something untested stopped working, it should work as before.

Is there a specific configuration that stopped working? The Report plug-in had some new classification features added recently, but they should not affect previously existing options.

2019-01-23 14:16   
Sorry, this was due to an error in my script ... and indeed, this option is not obsolete.
However, I'm a little surprised that this plug-in only reports with EVA (or value for older versions) but nothing with WP. I know there is the -wp-print option (or something like that), but a full report in CSV format would be very useful with results of EVA and WP as I would expect by calling Report.
This is more surprising with the last version of FC (Argon) since eva has a dedicated options for the analysis report on red-alarms in a csv file
2019-01-23 16:41   
(edited on: 2019-01-23 16:44)
Report lists the properties consolidated by the kernel, independently of which plug-in produced them. However, the Report plug-in must be run after WP (with a '-then' before '-report-csv'), otherwise it will not list its properties.

What usually happens is that, by happenstance, writing "frama-c -eva -report-csv file.csv" seems to work as expected, while "frama-c -wp -report-csv file.csv" does not. But some arbitrary changes in Frama-C could invert that, and since the order of execution in the Frama-C command line is unspecified between two '-then', both are valid executions.

Ideally, one should always write "frama-c -eva/-wp -then -report-csv file.csv", to enforce Eva/WP to run before Report, ensuring that Report will contain all the statuses generated by them.

The new red-alarms option for Eva is a special case due to the fact that these red alarms do not correspond to the consolidated properties in the kernel (e.g., in one iteration, they were Invalid, but in another they might have been Valid or Unknown, which results in the kernel consolidating them as Unknown, making the red "disappear" in the standard CSV report), hence why there is a specific Eva option to add them. WP does not have such cases, so it does not need a specific option.

If there is already a '-then' after '-wp' and before '-report-csv' in your script, then it might be another issue. Testing locally produced the results I indicated, so I'm assuming that was the cause, but it could be something else.

2019-01-23 17:14   
indeed it works !
thanks for your return