A pure predicate in an axiomatic with some "unpure" axioms have some strange results
ID0000073: This issue was created automatically from Mantis Issue 73. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0000073 | Frama-C | Plug-in > jessie | public | 2009-04-30 | 2009-06-23 |
Reporter | bobot | Assigned To | cmarche | Resolution | fixed |
Priority | normal | Severity | crash | Reproducibility | always |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Beryllium-20090601-beta1 |
Description :
A pure predicate in an axiomatic with some "unpure" axioms have some strange results. In this case an assertion failed :
myc.c
/*@ axiomatic myaxioms{
predicate myrelation(int p,int q);
logic int mylogic{L}(int * p);
axiom myaxiom{L} :
\forall int * p, q; \at(myrelation(mylogic(p),q),L);
} @*/
frama-c -jessie-analysis unwanted_label.c.assertion_failed.c :
Calling Jessie tool in subdir unwanted_label.c.assertion_failed.jessie File "jc/jc_typing.ml", line 2687, characters 20-20: Uncaught exception: File "jc/jc_typing.ml", line 2687, characters 20-26: Assertion failed
Additional Information :
frama-c : 5186