[aorai] add test for new grammar constructions

src/plugins/aorai/tests/ya/aorai_ptr_field.i

+/* run.config*
+   OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+struct S { int x; };
+
+void main(struct S* s) { return; }

src/plugins/aorai/tests/ya/aorai_ptr_field.ya

+%init: S0;
+%accept: S1;
+
+S0: { (*main().s).x >= 0 } -> S1
+  | { (main().s)->x < 0 } -> S1;
+S1: -> S1;

src/plugins/aorai/tests/ya/oracle/aorai_ptr_field.res.oracle

+[kernel] Parsing tests/ya/aorai_ptr_field.i (no preprocessing)
+[aorai] Welcome to the Aorai plugin
+[kernel] Parsing TMPDIR/aorai_aorai_ptr_field_0.i (no preprocessing)
+/* Generated by Frama-C */
+struct S {
+   int x ;
+};
+enum aorai_ListOper {
+    op_main = 0
+};
+enum aorai_OpStatusList {
+    aorai_Terminated = 1,
+    aorai_Called = 0
+};
+/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost int S0 = 1; */
+/*@ ghost int S1 = 0; */
+/*@ ghost
+  /@ requires 1 ≡ S0 ∧ 0 ≡ S1;
+     requires 1 ≡ S0 ⇒ s->x < 0 ∨ s->x ≥ 0;
+     ensures aorai_CurOpStatus ≡ aorai_Called;
+     ensures aorai_CurOperation ≡ op_main;
+     assigns aorai_CurOpStatus, aorai_CurOperation, S0, S1;
+     
+     behavior buch_state_S0_out:
+       ensures 0 ≡ S0;
+     
+     behavior buch_state_S1_in:
+       assumes 1 ≡ S0 ∧ (s->x < 0 ∨ s->x ≥ 0);
+       ensures 1 ≡ S1;
+     
+     behavior buch_state_S1_out:
+       assumes 0 ≡ S0 ∨ (¬(s->x < 0) ∧ ¬(s->x ≥ 0));
+       ensures 0 ≡ S1;
+   @/
+  void main_pre_func(struct S *s)
+  {
+    int S0_tmp;
+    int S1_tmp;
+    aorai_CurOpStatus = aorai_Called;
+    aorai_CurOperation = op_main;
+    S0_tmp = S0;
+    S1_tmp = S1;
+    if (S0 == 1 && s->x >= 0 || S0 == 1 && s->x < 0) S1_tmp = 1;
+    else S1_tmp = 0;
+    S0_tmp = 0;
+    S0 = S0_tmp;
+    S1 = S1_tmp;
+    return;
+  }
+
+*/
+
+/*@ ghost
+  /@ requires 1 ≡ S1 ∧ 0 ≡ S0;
+     ensures aorai_CurOpStatus ≡ aorai_Terminated;
+     ensures aorai_CurOperation ≡ op_main;
+     assigns aorai_CurOpStatus, aorai_CurOperation, S0, S1;
+     
+     behavior buch_state_S0_out:
+       ensures 0 ≡ S0;
+     
+     behavior buch_state_S1_in:
+       assumes 1 ≡ S1;
+       ensures 1 ≡ S1;
+     
+     behavior buch_state_S1_out:
+       assumes 0 ≡ S1;
+       ensures 0 ≡ S1;
+   @/
+  void main_post_func(void)
+  {
+    int S0_tmp;
+    int S1_tmp;
+    aorai_CurOpStatus = aorai_Terminated;
+    aorai_CurOperation = op_main;
+    S0_tmp = S0;
+    S1_tmp = S1;
+    if (S1 == 1) S1_tmp = 1; else S1_tmp = 0;
+    S0_tmp = 0;
+    S0 = S0_tmp;
+    S1 = S1_tmp;
+    return;
+  }
+
+*/
+
+/*@ requires 1 ≡ S0 ∧ 0 ≡ S1;
+    requires 1 ≡ S0 ⇒ s->x < 0 ∨ s->x ≥ 0;
+    
+    behavior Buchi_property_behavior:
+      ensures 0 ≡ S0;
+      ensures 1 ≡ S1;
+ */
+void main(struct S *s)
+{
+  /*@ ghost main_pre_func(s); */
+  /*@ ghost main_post_func(); */
+  return;
+}
+
+