Frama-C Bug Tracking System - Frama-C
View Issue Details
0000406Frama-CPlug-in > jessiepublic2010-02-16 10:162014-02-12 16:56
sboldo 
cmarche 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Boron-20100401 
0000406: assert false (* TODO *)
Hello, I have run into an "assert false" in the code of jessie. It prevents me from describing an axiomatic. The assert false is here: File "jc/jc_typing.ml", line 2820, characters 29-29: that is to say: | JCTreal_cast (_, _) -> assert false (* TODO *) And I was unable to understand what this function is about in order to correct it. :-/ Here is a simplified axiomatization example that fails: # pragma JessieFloatModel(strict) /*@ axiomatic FP { @ @ axiom toto : @ \forall double f; 0x1p-1022 <= \abs(f) || \abs(f) < 0x1p-1022; @ } */ Reagrds, Sylvie Boldo
No tags attached.
Issue History
2010-02-16 10:16sboldoNew Issue
2010-02-16 10:16sboldoStatusnew => assigned
2010-02-16 10:16sboldoAssigned To => cmarche
2010-02-16 10:19cmarcheNote Added: 0000681
2010-02-16 10:39cmarcheNote Added: 0000682
2010-02-16 10:39cmarcheStatusassigned => resolved
2010-02-16 10:39cmarcheResolutionopen => fixed
2010-04-19 16:13signolesStatusresolved => closed
2010-04-19 16:13signolesFixed in Version => Frama-C Boron
2010-04-19 16:14signolesNote Added: 0000776

Notes
(0000681)
cmarche   
2010-02-16 10:19   
Ouaip, c'est bien sur un bug. Neanmoins, meme si ce bug est corrigé, ce sera rejeté plus loin. Seul un lemma sera accepté.
(0000682)
cmarche   
2010-02-16 10:39   
Fixed in why CVS
(0000776)
signoles   
2010-04-19 16:14   
Fix in Why 2.24 (require Frama-C Boron-20100401).