--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on March 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie failure: "Unexpected internal region in logic"



Hello David,

Le ven. 12 mars 2010 08:45:37 CET,
David Delmas <david.delmas at airbus.com> a ?crit :

> 
>         //@ predicate P0{L}(int t[], int i) = t[i]==1;
>         
>         /*@ axiomatic Failure_Unexpected_internal_region_in_logic {
>         
>         predicate P1{L}(int t[], int i);
>         predicate P2{L}(int t[], int i);
>         
>         axiom aP1{L} :
>             \forall int t[], int i;
>                 i==0 && P0{L}(t,i) ==> P1{L}(t,i);
>         
>         axiom aP2{L} :
>             \forall int t[], int i;
>                 i!=1 && !P0{L}(t,i) ==> P2{L}(t,i);
>         }*/
> 
> 
> If I then run "frama-c -jessie failure.c", I get the below error :
> Uncaught exception: Failure("Unexpected internal region in logic")
> 

This is a bug. I'll let Jessie experts comment further on the exact
causes, but it seems that jessie (the tool, not the plugin) has some
troubles with axiomatisations in presence of two declarations that use
logic labels (in particular, if you change P2 into P1 in aP2 the issue
disappear). A seemingly related bug has already been reported (bug 424
http://bts.frama-c.com/view.php?id=424). A workaround might be to
split axiomatics so that each of them declares only one predicate/logic
function.

-- 
E tutto per oggi, a la prossima volta.
Virgile