Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002423Frama-CPlug-in > reportpublic2019-01-22 16:092019-01-24 10:33
Reporterpmo 
Assigned Tomaroneze 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionno change required 
Platformlinux OSubuntuOS Version4.18
Product VersionFrama-C 18-Argon 
Target VersionFrama-C 19-PotassiumFixed in Version 
Summary0002423: option -report-csv doesn't work anymore ?
Descriptionthis 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 ?
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006737)
maroneze (developer)
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.
(0006738)
pmo (reporter)
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
(0006739)
maroneze (developer)
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.
(0006740)
pmo (reporter)
2019-01-23 17:14

indeed it works ! thanks for your return

- Issue History
Date Modified Username Field Change
2019-01-22 16:09 pmo New Issue
2019-01-22 16:09 pmo Status new => assigned
2019-01-22 16:09 pmo Assigned To => correnson
2019-01-23 10:15 pmo Note Added: 0006735
2019-01-23 10:43 pmo Note Deleted: 0006735
2019-01-23 10:46 signoles Assigned To correnson => maroneze
2019-01-23 10:49 signoles Target Version => Frama-C 19-Potassium
2019-01-23 11:26 maroneze Note Added: 0006737
2019-01-23 11:32 maroneze Note Edited: 0006737 View Revisions
2019-01-23 14:16 pmo Note Added: 0006738
2019-01-23 16:41 maroneze Note Added: 0006739
2019-01-23 16:42 maroneze Note Edited: 0006739 View Revisions
2019-01-23 16:42 maroneze Note Edited: 0006739 View Revisions
2019-01-23 16:44 maroneze Note Edited: 0006739 View Revisions
2019-01-23 16:44 maroneze Note Edited: 0006739 View Revisions
2019-01-23 17:14 pmo Note Added: 0006740
2019-01-24 10:33 maroneze Status assigned => closed
2019-01-24 10:33 maroneze Resolution open => no change required


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker