2021-02-27 10:35 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001028Frama-CPlug-in > wppublic2011-11-28 17:552012-09-19 17:16
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001028: unable to prove that comparison-result is 0 or 1: insufficient axiomatization of eq_int_bool?
DescriptionThe 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.

TagsNo tags attached.
Attached Files
  • c file icon ftest.c (134 bytes) 2011-11-28 17:55 - 
    /*@ requires 2000000000 < 2147483647 < 2147483648;
    ensures \result == 0 || \result == 1;
*/
int eq9(int a) {
    return a == 9;
}
    c file icon ftest.c (134 bytes) 2011-11-28 17:55 +
  • ? file icon ite.why (336 bytes) 2011-12-01 16:04

-Relationships
+Relationships

-Notes

~0002521

correnson (manager)

2011-12-01 16:04

 The problem does not appear in SVN version, ite is no more used.
Actually, the problem is from Alt-Ergo, which does not split over c=true or c=false with ite.
A better definition of ite for alt-ergo is :

axiom ite_split:
   forall c:bool.
   forall x,y:'a [ite(c,x,y)].
   (c=true and ite(c,x,y)=x) or (c=false and ite(c,x,y)=y)

Before the next release, you can patch the *.why in share/wp and replace ite_true and ite_false axioms by ite_split. See also uploaded ite.why file.

~0002522

correnson (manager)

2011-12-01 16:05

 No more appear in SVN version.

~0002523

correnson (manager)

2011-12-01 16:11

 PS : ite axioms are generated by Why 2, not WP.

~0003121

correnson (manager)

2012-06-14 13:44

 Fixed in Qed
+Notes

-Issue History
Date Modified Username Field Change
2011-11-28 17:55 Jochen New Issue
2011-11-28 17:55 Jochen Status new => assigned
2011-11-28 17:55 Jochen Assigned To => correnson
2011-11-28 17:55 Jochen File Added: ftest.c
2011-12-01 16:04 correnson Note Added: 0002521
2011-12-01 16:04 correnson File Added: ite.why
2011-12-01 16:05 correnson Note Added: 0002522
2011-12-01 16:05 correnson Status assigned => acknowledged
2011-12-01 16:11 correnson Note Added: 0002523
2012-06-14 13:44 correnson Note Added: 0003121
2012-06-14 13:44 correnson Status acknowledged => closed
2012-06-14 13:44 correnson Resolution open => fixed
2012-06-14 14:22 signoles Status closed => resolved
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
+Issue History