assert false (* TODO *)
ID0000406: This issue was created automatically from Mantis Issue 406. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000406 | Frama-C | Plug-in > jessie | public | 2010-02-16 | 2014-02-12 |
| Reporter | sboldo | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Boron-20100401 |
Description :
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