[aorai] fixes oracle for metavariable test

src/plugins/aorai/tests/ya/metavariables-right.i

@@ -25,4 +25,3 @@ void main(int t)
     x++;
   }
 }
-

src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle

 [kernel] Parsing tests/aorai/metavariables-right.i (no preprocessing)
-[kernel] tests/aorai/metavariables-right.i:10: 
-  syntax error:
-  Location: between lines 10 and 12, before or at token: void
-  8     void i() {}
-  9     
-  
-  10    volatile int v,
-  11    
-  12    void main(void)
-  
-  13    {
-  14      if (v) {
-[kernel] Frama-C aborted: invalid user input.
+[aorai] Welcome to the Aorai plugin
+[kernel] Parsing /tmp/aorai_metavariables-right_0.i (no preprocessing)
+/* Generated by Frama-C */
+enum aorai_States {
+    aorai_reject_state = -2,
+    a = 0,
+    b = 1,
+    c = 2,
+    d = 3,
+    e = 4,
+    f_0 = 5,
+    g_0 = 6,
+    h_0 = 7,
+    i_0 = 8
+};
+enum aorai_ListOper {
+    op_f = 4,
+    op_g = 3,
+    op_h = 2,
+    op_i = 1,
+    op_main = 0
+};
+enum aorai_OpStatusList {
+    aorai_Terminated = 1,
+    aorai_Called = 0
+};
+/*@ lemma i_0_deterministic_trans{L}: \true;
+ */
+/*@ lemma h_0_deterministic_trans{L}: \true;
+ */
+/*@ lemma g_0_deterministic_trans{L}: \true;
+ */
+/*@ lemma f_0_deterministic_trans{L}: \true;
+ */
+/*@ lemma d_deterministic_trans{L}: \true;
+ */
+/*@ lemma c_deterministic_trans{L}: \true;
+ */
+/*@ lemma a_deterministic_trans{L}: \true;
+ */
+/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@
+lemma b_deterministic_trans{L}:
+  ¬(\at(aorai_CurOperation,L) ≡ op_g ∧
+     \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧
+     \at(aorai_CurOperation,L) ≡ op_f ∧
+     \at(aorai_CurOpStatus,L) ≡ aorai_Called);
+ */
+/*@ ghost int aorai_CurStates = a; */
+/*@ ghost int aorai_x = 0; */
+/*@
+lemma e_deterministic_trans{L}:
+  ¬(\at(aorai_CurOperation,L) ≡ op_main ∧
+     \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
+     \at(aorai_CurOperation,L) ≡ op_h ∧
+     \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ \at(aorai_x,L) > 0);
+ */
+/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
+    ensures aorai_CurOperation ≡ op_f;
+    assigns aorai_x, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_a_out:
+      ensures aorai_CurStates ≢ a;
+    
+    behavior buch_state_b_out:
+      ensures aorai_CurStates ≢ b;
+    
+    behavior buch_state_c_in_0:
+      assumes aorai_CurStates ≡ b;
+      ensures aorai_CurStates ≡ c;
+      ensures aorai_x ≡ \old(x);
+    
+    behavior buch_state_c_out:
+      assumes aorai_CurStates ≢ b;
+      ensures aorai_CurStates ≢ c;
+      ensures aorai_x ≡ \old(aorai_x);
+    
+    behavior buch_state_d_out:
+      ensures aorai_CurStates ≢ d;
+    
+    behavior buch_state_e_out:
+      ensures aorai_CurStates ≢ e;
+    
+    behavior buch_state_f_0_out:
+      ensures aorai_CurStates ≢ f_0;
+    
+    behavior buch_state_g_0_out:
+      ensures aorai_CurStates ≢ g_0;
+    
+    behavior buch_state_h_0_out:
+      ensures aorai_CurStates ≢ h_0;
+    
+    behavior buch_state_i_0_out:
+      ensures aorai_CurStates ≢ i_0;
+ */
+void f_pre_func(int x)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Called;
+  aorai_CurOperation = op_f;
+  aorai_CurStates_tmp = aorai_CurStates;
+  if (1 == aorai_CurStates) {
+    aorai_CurStates_tmp = c;
+    aorai_x = x;
+  }
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires aorai_CurStates ≡ c;
+    ensures aorai_CurOpStatus ≡ aorai_Terminated;
+    ensures aorai_CurOperation ≡ op_f;
+    assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_a_out:
+      ensures aorai_CurStates ≢ a;
+    
+    behavior buch_state_b_out:
+      ensures aorai_CurStates ≢ b;
+    
+    behavior buch_state_c_out:
+      ensures aorai_CurStates ≢ c;
+    
+    behavior buch_state_d_out:
+      ensures aorai_CurStates ≢ d;
+    
+    behavior buch_state_e_in:
+      assumes aorai_CurStates ≡ c;
+      ensures aorai_CurStates ≡ e;
+    
+    behavior buch_state_e_out:
+      assumes aorai_CurStates ≢ c;
+      ensures aorai_CurStates ≢ e;
+    
+    behavior buch_state_f_0_out:
+      ensures aorai_CurStates ≢ f_0;
+    
+    behavior buch_state_g_0_out:
+      ensures aorai_CurStates ≢ g_0;
+    
+    behavior buch_state_h_0_out:
+      ensures aorai_CurStates ≢ h_0;
+    
+    behavior buch_state_i_0_out:
+      ensures aorai_CurStates ≢ i_0;
+ */
+void f_post_func(void)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Terminated;
+  aorai_CurOperation = op_f;
+  aorai_CurStates_tmp = aorai_CurStates;
+  if (2 == aorai_CurStates) aorai_CurStates_tmp = e;
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires aorai_CurStates ≡ b;
+    
+    behavior Buchi_property_behavior:
+      ensures aorai_CurStates ≡ e;
+      ensures
+        \at(aorai_CurStates ≡ b,Pre) ∧ aorai_CurStates ≡ e ⇒
+        aorai_x ≡ \at(x,Pre) + 0;
+ */
+void f(int x)
+{
+  f_pre_func(x);
+  f_post_func();
+  return;
+}
+
+/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
+    ensures aorai_CurOperation ≡ op_g;
+    assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_a_out:
+      ensures aorai_CurStates ≢ a;
+    
+    behavior buch_state_b_out:
+      ensures aorai_CurStates ≢ b;
+    
+    behavior buch_state_c_out:
+      ensures aorai_CurStates ≢ c;
+    
+    behavior buch_state_d_in:
+      assumes aorai_CurStates ≡ b;
+      ensures aorai_CurStates ≡ d;
+    
+    behavior buch_state_d_out:
+      assumes aorai_CurStates ≢ b;
+      ensures aorai_CurStates ≢ d;
+    
+    behavior buch_state_e_out:
+      ensures aorai_CurStates ≢ e;
+    
+    behavior buch_state_f_0_out:
+      ensures aorai_CurStates ≢ f_0;
+    
+    behavior buch_state_g_0_out:
+      ensures aorai_CurStates ≢ g_0;
+    
+    behavior buch_state_h_0_out:
+      ensures aorai_CurStates ≢ h_0;
+    
+    behavior buch_state_i_0_out:
+      ensures aorai_CurStates ≢ i_0;
+ */
+void g_pre_func(void)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Called;
+  aorai_CurOperation = op_g;
+  aorai_CurStates_tmp = aorai_CurStates;
+  if (1 == aorai_CurStates) aorai_CurStates_tmp = d;
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires aorai_CurStates ≡ d;
+    ensures aorai_CurOpStatus ≡ aorai_Terminated;
+    ensures aorai_CurOperation ≡ op_g;
+    assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_a_out:
+      ensures aorai_CurStates ≢ a;
+    
+    behavior buch_state_b_out:
+      ensures aorai_CurStates ≢ b;
+    
+    behavior buch_state_c_out:
+      ensures aorai_CurStates ≢ c;
+    
+    behavior buch_state_d_out:
+      ensures aorai_CurStates ≢ d;
+    
+    behavior buch_state_e_out:
+      ensures aorai_CurStates ≢ e;
+    
+    behavior buch_state_f_0_out:
+      ensures aorai_CurStates ≢ f_0;
+    
+    behavior buch_state_g_0_in:
+      assumes aorai_CurStates ≡ d;
+      ensures aorai_CurStates ≡ g_0;
+    
+    behavior buch_state_g_0_out:
+      assumes aorai_CurStates ≢ d;
+      ensures aorai_CurStates ≢ g_0;
+    
+    behavior buch_state_h_0_out:
+      ensures aorai_CurStates ≢ h_0;
+    
+    behavior buch_state_i_0_out:
+      ensures aorai_CurStates ≢ i_0;
+ */
+void g_post_func(void)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Terminated;
+  aorai_CurOperation = op_g;
+  aorai_CurStates_tmp = aorai_CurStates;
+  if (3 == aorai_CurStates) aorai_CurStates_tmp = g_0;
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires aorai_CurStates ≡ b;
+    
+    behavior Buchi_property_behavior:
+      ensures aorai_CurStates ≡ g_0;
+ */
+void g(void)
+{
+  g_pre_func();
+  g_post_func();
+  return;
+}
+
+/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
+    ensures aorai_CurOperation ≡ op_h;
+    assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_a_out:
+      ensures aorai_CurStates ≢ a;
+    
+    behavior buch_state_b_out:
+      ensures aorai_CurStates ≢ b;
+    
+    behavior buch_state_c_out:
+      ensures aorai_CurStates ≢ c;
+    
+    behavior buch_state_d_out:
+      ensures aorai_CurStates ≢ d;
+    
+    behavior buch_state_e_out:
+      ensures aorai_CurStates ≢ e;
+    
+    behavior buch_state_f_0_in:
+      assumes aorai_CurStates ≡ e ∧ aorai_x > 0;
+      ensures aorai_CurStates ≡ f_0;
+    
+    behavior buch_state_f_0_out:
+      assumes aorai_CurStates ≢ e ∨ ¬(aorai_x > 0);
+      ensures aorai_CurStates ≢ f_0;
+    
+    behavior buch_state_g_0_out:
+      ensures aorai_CurStates ≢ g_0;
+    
+    behavior buch_state_h_0_out:
+      ensures aorai_CurStates ≢ h_0;
+    
+    behavior buch_state_i_0_out:
+      ensures aorai_CurStates ≢ i_0;
+ */
+void h_pre_func(int x)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Called;
+  aorai_CurOperation = op_h;
+  aorai_CurStates_tmp = aorai_CurStates;
+  if (4 == aorai_CurStates) 
+    if (aorai_x > 0) aorai_CurStates_tmp = f_0;
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires aorai_CurStates ≡ f_0;
+    ensures aorai_CurOpStatus ≡ aorai_Terminated;
+    ensures aorai_CurOperation ≡ op_h;
+    assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_a_out:
+      ensures aorai_CurStates ≢ a;
+    
+    behavior buch_state_b_out:
+      ensures aorai_CurStates ≢ b;
+    
+    behavior buch_state_c_out:
+      ensures aorai_CurStates ≢ c;
+    
+    behavior buch_state_d_out:
+      ensures aorai_CurStates ≢ d;
+    
+    behavior buch_state_e_out:
+      ensures aorai_CurStates ≢ e;
+    
+    behavior buch_state_f_0_out:
+      ensures aorai_CurStates ≢ f_0;
+    
+    behavior buch_state_g_0_in:
+      assumes aorai_CurStates ≡ f_0;
+      ensures aorai_CurStates ≡ g_0;
+    
+    behavior buch_state_g_0_out:
+      assumes aorai_CurStates ≢ f_0;
+      ensures aorai_CurStates ≢ g_0;
+    
+    behavior buch_state_h_0_out:
+      ensures aorai_CurStates ≢ h_0;
+    
+    behavior buch_state_i_0_out:
+      ensures aorai_CurStates ≢ i_0;
+ */
+void h_post_func(void)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Terminated;
+  aorai_CurOperation = op_h;
+  aorai_CurStates_tmp = aorai_CurStates;
+  if (5 == aorai_CurStates) aorai_CurStates_tmp = g_0;
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires aorai_CurStates ≡ e;
+    requires aorai_CurStates ≡ e ⇒ aorai_x > 0;
+    
+    behavior Buchi_property_behavior:
+      ensures aorai_CurStates ≡ g_0;
+ */
+void h(int x)
+{
+  h_pre_func(x);
+  h_post_func();
+  return;
+}
+
+/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
+    ensures aorai_CurOperation ≡ op_i;
+    assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_a_out:
+      ensures aorai_CurStates ≢ a;
+    
+    behavior buch_state_b_out:
+      ensures aorai_CurStates ≢ b;
+    
+    behavior buch_state_c_out:
+      ensures aorai_CurStates ≢ c;
+    
+    behavior buch_state_d_out:
+      ensures aorai_CurStates ≢ d;
+    
+    behavior buch_state_e_out:
+      ensures aorai_CurStates ≢ e;
+    
+    behavior buch_state_f_0_out:
+      ensures aorai_CurStates ≢ f_0;
+    
+    behavior buch_state_g_0_out:
+      ensures aorai_CurStates ≢ g_0;
+    
+    behavior buch_state_h_0_in:
+      assumes aorai_CurStates ≡ g_0;
+      ensures aorai_CurStates ≡ h_0;
+    
+    behavior buch_state_h_0_out:
+      assumes aorai_CurStates ≢ g_0;
+      ensures aorai_CurStates ≢ h_0;
+    
+    behavior buch_state_i_0_out:
+      ensures aorai_CurStates ≢ i_0;
+ */
+void i_pre_func(void)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Called;
+  aorai_CurOperation = op_i;
+  aorai_CurStates_tmp = aorai_CurStates;
+  if (6 == aorai_CurStates) aorai_CurStates_tmp = h_0;
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires aorai_CurStates ≡ h_0;
+    ensures aorai_CurOpStatus ≡ aorai_Terminated;
+    ensures aorai_CurOperation ≡ op_i;
+    assigns aorai_x, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_a_out:
+      ensures aorai_CurStates ≢ a;
+    
+    behavior buch_state_b_out:
+      ensures aorai_CurStates ≢ b;
+    
+    behavior buch_state_c_out:
+      ensures aorai_CurStates ≢ c;
+    
+    behavior buch_state_d_out:
+      ensures aorai_CurStates ≢ d;
+    
+    behavior buch_state_e_in_0:
+      assumes aorai_CurStates ≡ h_0;
+      ensures aorai_CurStates ≡ e;
+      ensures aorai_x ≡ \old(1);
+    
+    behavior buch_state_e_out:
+      assumes aorai_CurStates ≢ h_0;
+      ensures aorai_CurStates ≢ e;
+      ensures aorai_x ≡ \old(aorai_x);
+    
+    behavior buch_state_f_0_out:
+      ensures aorai_CurStates ≢ f_0;
+    
+    behavior buch_state_g_0_out:
+      ensures aorai_CurStates ≢ g_0;
+    
+    behavior buch_state_h_0_out:
+      ensures aorai_CurStates ≢ h_0;
+    
+    behavior buch_state_i_0_out:
+      ensures aorai_CurStates ≢ i_0;
+ */
+void i_post_func(void)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Terminated;
+  aorai_CurOperation = op_i;
+  aorai_CurStates_tmp = aorai_CurStates;
+  if (7 == aorai_CurStates) {
+    aorai_CurStates_tmp = e;
+    aorai_x = 1;
+  }
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires aorai_CurStates ≡ g_0;
+    
+    behavior Buchi_property_behavior:
+      ensures aorai_CurStates ≡ e;
+      ensures
+        \at(aorai_CurStates ≡ g_0,Pre) ∧ aorai_CurStates ≡ e ⇒
+        aorai_x ≡ \at(1,Pre) + 0;
+ */
+void i(void)
+{
+  i_pre_func();
+  i_post_func();
+  return;
+}
+
+/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
+    ensures aorai_CurOperation ≡ op_main;
+    assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_a_out:
+      ensures aorai_CurStates ≢ a;
+    
+    behavior buch_state_b_in:
+      assumes aorai_CurStates ≡ a;
+      ensures aorai_CurStates ≡ b;
+    
+    behavior buch_state_b_out:
+      assumes aorai_CurStates ≢ a;
+      ensures aorai_CurStates ≢ b;
+    
+    behavior buch_state_c_out:
+      ensures aorai_CurStates ≢ c;
+    
+    behavior buch_state_d_out:
+      ensures aorai_CurStates ≢ d;
+    
+    behavior buch_state_e_out:
+      ensures aorai_CurStates ≢ e;
+    
+    behavior buch_state_f_0_out:
+      ensures aorai_CurStates ≢ f_0;
+    
+    behavior buch_state_g_0_out:
+      ensures aorai_CurStates ≢ g_0;
+    
+    behavior buch_state_h_0_out:
+      ensures aorai_CurStates ≢ h_0;
+    
+    behavior buch_state_i_0_out:
+      ensures aorai_CurStates ≢ i_0;
+ */
+void main_pre_func(int t)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Called;
+  aorai_CurOperation = op_main;
+  aorai_CurStates_tmp = aorai_CurStates;
+  if (0 == aorai_CurStates) aorai_CurStates_tmp = b;
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires aorai_CurStates ≡ e;
+    ensures aorai_CurOpStatus ≡ aorai_Terminated;
+    ensures aorai_CurOperation ≡ op_main;
+    assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+    
+    behavior buch_state_a_out:
+      ensures aorai_CurStates ≢ a;
+    
+    behavior buch_state_b_out:
+      ensures aorai_CurStates ≢ b;
+    
+    behavior buch_state_c_out:
+      ensures aorai_CurStates ≢ c;
+    
+    behavior buch_state_d_out:
+      ensures aorai_CurStates ≢ d;
+    
+    behavior buch_state_e_out:
+      ensures aorai_CurStates ≢ e;
+    
+    behavior buch_state_f_0_out:
+      ensures aorai_CurStates ≢ f_0;
+    
+    behavior buch_state_g_0_out:
+      ensures aorai_CurStates ≢ g_0;
+    
+    behavior buch_state_h_0_out:
+      ensures aorai_CurStates ≢ h_0;
+    
+    behavior buch_state_i_0_in:
+      assumes aorai_CurStates ≡ e;
+      ensures aorai_CurStates ≡ i_0;
+    
+    behavior buch_state_i_0_out:
+      assumes aorai_CurStates ≢ e;
+      ensures aorai_CurStates ≢ i_0;
+ */
+void main_post_func(void)
+{
+  /*@ ghost int aorai_CurStates_tmp; */
+  aorai_CurOpStatus = aorai_Terminated;
+  aorai_CurOperation = op_main;
+  aorai_CurStates_tmp = aorai_CurStates;
+  if (4 == aorai_CurStates) aorai_CurStates_tmp = i_0;
+  aorai_CurStates = aorai_CurStates_tmp;
+  return;
+}
+
+/*@ requires aorai_CurStates ≡ a;
+    
+    behavior Buchi_property_behavior:
+      ensures aorai_CurStates ≡ i_0;
+      ensures
+        \at(aorai_CurStates ≡ a,Pre) ∧ aorai_CurStates ≡ i_0 ⇒
+        aorai_x ≡ \at(1,Pre) + 0 ∨ aorai_x ≡ \at(42,Pre) + 0;
+ */
+void main(int t)
+{
+  int aorai_Loop_Init_15;
+  main_pre_func(t);
+  if (t) f(42);
+  else {
+    g();
+    goto L;
+  }
+  int x = 0;
+  /*@ ghost aorai_Loop_Init_15 = 1; */
+  aorai_loop_15:
+  /*@ loop invariant Aorai: aorai_CurStates ≢ a;
+      loop invariant Aorai: aorai_CurStates ≢ b;
+      loop invariant Aorai: aorai_CurStates ≢ c;
+      loop invariant Aorai: aorai_CurStates ≢ d;
+      loop invariant Aorai: aorai_CurStates ≡ e;
+      loop invariant Aorai: aorai_CurStates ≢ f_0;
+      loop invariant Aorai: aorai_CurStates ≢ g_0;
+      loop invariant Aorai: aorai_CurStates ≢ h_0;
+      loop invariant Aorai: aorai_CurStates ≢ i_0;
+      loop invariant
+        Aorai:
+          \at(aorai_CurStates ≡ e,aorai_loop_15) ∧ aorai_CurStates ≡ e ⇒
+          aorai_x ≡ \at(1,Pre) + 0;
+  */
+  while (x < 100) {
+    /*@ ghost aorai_Loop_Init_15 = 0; */
+    h(x);
+    L: i();
+    x ++;
+  }
+  main_post_func();
+  return;
+}
+
+