Frama-C Bug Tracking System - Frama-C |
| View Issue Details |
|
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0002453 | Frama-C | Plug-in > wp | public | 2019-06-14 13:20 | 2019-07-05 11:41 |
|
| Reporter | jens | |
| Assigned To | bobot | |
| Priority | normal | Severity | major | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | Frama-C GIT, precise the release id | |
| Target Version | | Fixed in Version | Frama-C 19-Potassium | |
|
| Summary | 0002453: number of generated files in Frama-C 18 vs 19. beta(2) |
| Description | This entry references issue
https://github.com/Frama-C/Frama-C-snapshot/issues/21 [^]
in order to be able to easily add files. |
| Steps To Reproduce | Run the command
frama-c -pp-annot -no-unicode -wp -wp-rte -warn-unsigned-overflow -warn-unsigned-downcast -wp-model Typed+ref -wp-out rc.wp rc.c
on the attached files.
As mentioned in the github issue, both 18.0 and 19.beta(2) report 17 VC of which 5 are discharged by Qed and the remaining 12 are verified by Alt-Ergo.
However, Frama-C 18.0 generates 12 .mlw and .out files, respectively.
Frama-C 19 beta2, on the other hand, only generates 9 .mlw and .out files, respectively.
The latter behaviour confuses our internal evaluation scripts which report that only 9 of the remaining 12 proof obligations have been discharged by Alt-Ergo. |
| Additional Information | |
| Tags | No tags attached. |
| Relationships | |
| Attached Files |  rc.c (42,718) 2019-06-14 13:20
https://bts.frama-c.com/file_download.php?file_id=1316&type=bug |
|
| Issue History |
| Date Modified | Username | Field | Change |
| 2019-06-14 13:20 | jens | New Issue | |
| 2019-06-14 13:20 | jens | Status | new => assigned |
| 2019-06-14 13:20 | jens | Assigned To | => correnson |
| 2019-06-14 13:20 | jens | File Added: rc.c | |
| 2019-06-14 14:03 | bobot | Note Added: 0006785 | |
| 2019-06-14 14:06 | correnson | Note Added: 0006786 | |
| 2019-06-14 14:10 | jens | Note Added: 0006787 | |
| 2019-06-14 15:27 | bobot | Note Added: 0006788 | |
| 2019-06-14 16:18 | jens | Note Added: 0006789 | |
| 2019-06-26 11:52 | jens | Note Added: 0006804 | |
| 2019-06-26 15:37 | bobot | Note Added: 0006805 | |
| 2019-06-26 15:38 | bobot | Status | assigned => resolved |
| 2019-06-26 15:38 | bobot | Fixed in Version | => Frama-C 19-Potassium |
| 2019-06-26 15:38 | bobot | Resolution | open => fixed |
| 2019-06-26 15:38 | bobot | Assigned To | correnson => bobot |
| 2019-07-05 11:41 | signoles | Status | resolved => closed |
|
Notes |
|
|
(0006785)
|
|
bobot
|
|
2019-06-14 14:03
|
|
|
The file names changed and they are perhaps not uniq anymore. |
|
|
|
|
The files are only generated when Qed did not solve the goals ; what happened is that v19 is much better than v18 at solving with Qed :-)
To get stable results, use the -wp-report option or, even better, the -report and -report-classify utilities. |
|
|
|
(0006787)
|
|
jens
|
|
2019-06-14 14:10
|
|
|
I don't understand the last remark as both versions claim that 5 VC were successfully handled by Qed and the remaining 12 by Alt-Ergo. In other words, for this particular example, Qed is not better. |
|
|
|
(0006788)
|
|
bobot
|
|
2019-06-14 15:27
|
|
|
Yes there is really a regression, it will be fixed. (However using -report could still be a better idea than looking at the files present ;).) |
|
|
|
(0006789)
|
|
jens
|
|
2019-06-14 16:18
|
|
|
Thanks for the clarification and the hints towards "-report" |
|
|
|
(0006804)
|
|
jens
|
|
2019-06-26 11:52
|
|
|
It looks like the issue os not present in the final release of Frama-C 19.0 |
|
|
|
(0006805)
|
|
bobot
|
|
2019-06-26 15:37
|
|
|
Yes it has been fixed, thanks to your report! |
|