Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Jessie failure: "Unexpected internal region in logic"
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Fri, 12 Mar 2010 10:20:10 +0100
  • In-reply-to: <30805_1268379953_4B99F131_30805_43_1_1268379937.14079.57.camel@ossiriand>
  • References: <30805_1268379953_4B99F131_30805_43_1_1268379937.14079.57.camel@ossiriand>
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