Frama-C does not work with versions of Why3 newer than 0.83
ID0002067: This issue was created automatically from Mantis Issue 2067. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002067 | Frama-C | Plug-in > wp | public | 2015-01-27 | 2015-03-17 |
| Reporter | thinkmoore | Assigned To | bobot | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | Mac OS X | OS Version | Yosemite |
| Product Version | Frama-C Neon-20140301 | Target Version | Frama-C Sodium | Fixed in Version | Frama-C Sodium |
Description :
Why3 appears to have changed their command line interface with release 0.84, causing Frama-C to issue commands it no longer understands.
Steps To Reproduce :
Install Why3 >= 0.84 and attempt to discharge a wp goal using a why3 solver, i.e. -wp-prover z3