Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

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 
PlatformOSOS Version
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 Filesc file icon ftest.c [^] (134 bytes) 2011-11-28 17:55 [Show Content]
? file icon ite.why [^] (336 bytes) 2011-12-01 16:04

- 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

- 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

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker