Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000424Frama-CPlug-in > jessiepublic2010-03-08 23:042010-03-22 16:58
ReporterJochen 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in Version 
Summary0000424: Uncaught exception: Failure("Unexpected internal region in logic")
DescriptionJessie exits with the message <<Uncaught exception: Failure("Unexpected internal region in logic")>> when trying to translate the attached program.
"Uncaught" and "Unexpected" sounds like a bug.
I couldn't find a work-around for it yet.
TagsNo tags attached.
Attached Filesc file icon alloc.c [^] (1,727 bytes) 2010-03-08 23:04 [Show Content]

- Relationships

-  Notes
(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.

- Issue History
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
Powered by Mantis Bugtracker