Anonymous | Login | Signup for a new account | 2019-12-09 01:54 CET | ![]() |
Main | My View | View Issues | Change Log | Roadmap | Repositories |
View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
0000424 | Frama-C | Plug-in > jessie | public | 2010-03-08 23:04 | 2010-03-22 16:58 | ||||||||
Reporter | Jochen | ||||||||||||
Assigned To | cmarche | ||||||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||||||
Status | assigned | Resolution | open | ||||||||||
Platform | OS | OS Version | |||||||||||
Product Version | Frama-C Beryllium-20090902 | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0000424: Uncaught exception: Failure("Unexpected internal region in logic") | ||||||||||||
Description | Jessie exits with the message < | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files | ![]() | ||||||||||||
![]() |
|
(0000727) Jochen (reporter) 2010-03-11 16:08 |
I could boil down the example causing the "Uncaught" message to the following: /*@ axiomatic a1 { logic boolean isList{L}(int *b, integer f); logic integer jLgth{L}(int *b); axiom a2{L}: \forall int *b; isList(b,b[5]); axiom a3{L}: \forall int *b; jLgth(b) == 0; } */ |
(0000728) virgile (developer) 2010-03-12 10:29 |
This thread on frama-c-discuss http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-March/001844.html suggests that the issue lies in the two functions/predicates declared in the axiomatic block. A workaround until this is fixed would be to declare separately isList and jLgth (putting the axioms in the latter). Note that it might imply to write some reads clauses for isList (while they'd be inferred from the axioms in the case of only one axiomatic). |
(0000733) Jochen (reporter) 2010-03-22 16:58 |
I'm fine with the work-around Virgile suggested in his above note 728. As far as I'm concerned, the issue may be closed. |
![]() |
|||
Date Modified | Username | Field | Change |
2010-03-08 23:04 | Jochen | New Issue | |
2010-03-08 23:04 | Jochen | Status | new => assigned |
2010-03-08 23:04 | Jochen | Assigned To | => cmarche |
2010-03-08 23:04 | Jochen | File Added: alloc.c | |
2010-03-11 16:08 | Jochen | Note Added: 0000727 | |
2010-03-12 10:29 | virgile | Note Added: 0000728 | |
2010-03-12 10:59 | signoles | Relationship added | related to 0000426 |
2010-03-12 11:46 | signoles | Relationship deleted | related to 0000426 |
2010-03-22 16:58 | Jochen | Note Added: 0000733 |
Copyright © 2000 - 2019 MantisBT Team |