unable to prove that comparison-result is 0 or 1: insufficient axiomatization of eq_int_bool?
ID0001028: This issue was created automatically from Mantis Issue 1028. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001028 | Frama-C | Plug-in > wp | public | 2011-11-28 | 2012-09-19 |
| Reporter | Jochen | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
The attached program is verified under Jessie (why 2.30), but not under Wp.
Jessie generates two obligations: one for the case a==9 (and \result==1), and another for a!=9 (and \result==0); both are trivial to verify.
In contrast, Wp generates something like ite(eq_int_bool(a,9),1,0)==0 || ite(eq_int_bool(a,9),1,0)==1. I found axioms like ite(true,x,y)==x and ite(false,x,y)==y, however, an axiom about eq_int_bool always returning either true or false seems to be missing.