--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on March 2010 ---
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