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.
|ID0001028||Frama-C||Plug-in > wp||public||2011-11-28||2012-09-19|
|Product Version||Frama-C Nitrogen-20111001||Target Version||-||Fixed in Version||Frama-C Oxygen-20120901|
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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information