Frama-C Bug Tracking System - Frama-C
View Issue Details
0000424Frama-CPlug-in > jessiepublic2010-03-08 23:042010-03-22 16:58
Jochen 
cmarche 
normalminoralways
assignedopen 
Frama-C Beryllium-20090902 
 
0000424: Uncaught exception: Failure("Unexpected internal region in logic")
Jessie exits with the message <> when trying to translate the attached program. "Uncaught" and "Unexpected" sounds like a bug. I couldn't find a work-around for it yet.
No tags attached.
c alloc.c (1,727) 2010-03-08 23:04
https://bts.frama-c.com/file_download.php?file_id=64&type=bug
Issue History
2010-03-08 23:04JochenNew Issue
2010-03-08 23:04JochenStatusnew => assigned
2010-03-08 23:04JochenAssigned To => cmarche
2010-03-08 23:04JochenFile Added: alloc.c
2010-03-11 16:08JochenNote Added: 0000727
2010-03-12 10:29virgileNote Added: 0000728
2010-03-12 10:59signolesRelationship addedrelated to 0000426
2010-03-12 11:46signolesRelationship deletedrelated to 0000426
2010-03-22 16:58JochenNote Added: 0000733

Notes
(0000727)
Jochen   
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   
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   
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.