View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000073 | Frama-C | Plug-in > jessie | public | 2009-04-30 14:46 | 2009-06-23 18:03 | ||||
Reporter | bobot | ||||||||
Assigned To | cmarche | ||||||||
Priority | normal | Severity | crash | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C GIT, precise the release id | ||||||||
Target Version | Fixed in Version | Frama-C Beryllium-20090601-beta1 | |||||||
Summary | 0000073: A pure predicate in an axiomatic with some "unpure" axioms have some strange results | ||||||||
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 | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2009-04-30 14:46 | bobot | New Issue | |
2009-04-30 16:49 | monate | Status | new => assigned |
2009-04-30 16:49 | monate | Assigned To | => cmarche |
2009-06-18 13:49 | cmarche | Status | assigned => resolved |
2009-06-18 13:49 | cmarche | Resolution | open => fixed |
2009-06-23 18:02 | signoles | Status | resolved => closed |
2009-06-23 18:03 | signoles | Fixed in Version | => Frama-C Beryllium beta-1 |