Feedback on using Colibri2 on the WP tests
In the following branch of Frama-C:
- https://git.frama-c.com/frama-c/frama-c/-/commits/colibri2
I have added a few commits that updates Oracles for tests that behaves differently:
- Unknown errors: tests that fail with Why3 Unknown error
- Valid -> Unsuccess: tests that fail with Colibri but not with Alt-Ergo
- Unsuccess -> Failed: tests where status changed from Unsuccess to Failed
- Valid -> Failed: tests where status changed from Valid to Failed
- Unsuccess -> Valid (float/real): tests related to float where there are more successful proofs, however, since some of them are name KO, a closer look may be useful
- Suspect test results: tests where some proofs succeeds while I suspect it should not
The last commit provides the changes required to run Colibri2 instead of Alt-Ergo in the tests.