Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000406Frama-CPlug-in > jessiepublic2010-02-16 10:162014-02-12 16:56
Reportersboldo 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000406: assert false (* TODO *)
DescriptionHello,

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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000681)
cmarche (developer)
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 (developer)
2010-02-16 10:39


Fixed in why CVS
(0000776)
signoles (manager)
2010-04-19 16:14

Fix in Why 2.24 (require Frama-C Boron-20100401).

- Issue History
Date Modified Username Field Change
2010-02-16 10:16 sboldo New Issue
2010-02-16 10:16 sboldo Status new => assigned
2010-02-16 10:16 sboldo Assigned To => cmarche
2010-02-16 10:19 cmarche Note Added: 0000681
2010-02-16 10:39 cmarche Note Added: 0000682
2010-02-16 10:39 cmarche Status assigned => resolved
2010-02-16 10:39 cmarche Resolution open => fixed
2010-04-19 16:13 signoles Status resolved => closed
2010-04-19 16:13 signoles Fixed in Version => Frama-C Boron
2010-04-19 16:14 signoles Note Added: 0000776


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker