Option -wp-qed-checks generates invalid At-Ergo files
ID0002031: This issue was created automatically from Mantis Issue 2031. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002031 | Frama-C | Plug-in > wp | public | 2014-12-15 | 2014-12-16 |
| Reporter | dmentre | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
When running Frama-C / WP with -wp-qed-checks option, most of generated ALt-Ergo files are truncated and thus invalid.
For example, on following file: """ /*@ requires 0 <= x <= 10; ensures 1 <= \result <= 11; */ int f(int x) { return x + 1; } """
and calling Frama-C with: frama-c -wp-out out -wp -wp-qed-checks f_wp.c
Here is one of generated files: """ $ cat out/typed/Qed_19_20.ergo (* ---------------------------------------------------------- ) ( --- Qed-19-20 --- ) ( ---------------------------------------------------------- *)
goal Qed_19_20: (0 < """
Best regards, david
Steps To Reproduce :
$ cat > f_wp.c /*@ requires 0 <= x <= 10; ensures 1 <= \result <= 11; */ int f(int x) { return x + 1; } ^D
$ frama-c -wp-out out -wp -wp-qed-checks f_wp.c
$ cat out/typed/Qed_19_20.ergo