Frama-C Bug Tracking System - Frama-C
View Issue Details
0000424Frama-CPlug-in > jessiepublic2010-03-08 23:042010-03-22 16:58
Frama-C Beryllium-20090902 
0000424: Uncaught exception: Failure("Unexpected internal region in logic")
Jessie 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.
No tags attached.
c alloc.c (1,727) 2010-03-08 23:04
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

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;
} */
2010-03-12 10:29   
This thread on frama-c-discuss [^]

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).
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.