From 042790d9c2780ff6dbb8ee8b5265295b89d149eb Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 7 Jan 2019 11:09:25 +0100
Subject: [PATCH] [aorai] fixes oracle for metavariable test
---
.../aorai/tests/ya/metavariables-right.i | 1 -
.../ya/oracle/metavariables-right.res.oracle | 657 +++++++++++++++++-
2 files changed, 644 insertions(+), 14 deletions(-)
diff --git a/src/plugins/aorai/tests/ya/metavariables-right.i b/src/plugins/aorai/tests/ya/metavariables-right.i
index b79672a08cd..7c0f5aedff7 100644
--- a/src/plugins/aorai/tests/ya/metavariables-right.i
+++ b/src/plugins/aorai/tests/ya/metavariables-right.i
@@ -25,4 +25,3 @@ void main(int t)
x++;
}
}
-
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
index d816c5975a4..2b5b723ec9d 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -1,14 +1,645 @@
[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;
+}
+
+
--
GitLab