Commit 32202fd3 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

prettier oracles

parent 96362936
(* Small script to test that the code generated by aorai can be parsed again
* by frama-c.
*)
*)
open Kernel
module P = Plugin.Register
(struct
let name = "aorai testing module"
let shortname = "aorai-test"
let help = "utility script for aorai regtests"
end)
(struct
let name = "aorai testing module"
let shortname = "aorai-test"
let help = "utility script for aorai regtests"
end)
module TestNumber =
P.Zero
......@@ -17,25 +17,25 @@ module TestNumber =
let option_name = "-aorai-test-number"
let help = "test number when multiple tests are run over the same file"
let arg_name = "n"
end)
end)
module InternalWpShare =
P.Filepath(
struct
let option_name = "-aorai-test-wp-share"
let help = "use custom wp share dir (when in internal plugin mode)"
let arg_name = "dir"
let existence = Filepath.Must_exist
let file_kind = "wp share directory"
end)
struct
let option_name = "-aorai-test-wp-share"
let help = "use custom wp share dir (when in internal plugin mode)"
let arg_name = "dir"
let existence = Filepath.Must_exist
let file_kind = "wp share directory"
end)
module ProveAuxSpec =
P.False(
struct
let option_name = "-aorai-test-prove-aux-spec"
let help = "use WP + alt-ergo to prove that generated spec and body \
of auxiliary automata functions match"
end)
struct
let option_name = "-aorai-test-prove-aux-spec"
let help = "use WP + alt-ergo to prove that generated spec and body \
of auxiliary automata functions match"
end)
let ok = ref false
......@@ -95,6 +95,7 @@ let extend () =
Project.set_current my_project;
Kernel.SymbolicPath.add ("TMPDIR:"^Filename.get_temp_dir_name());
Files.append_after [ Filepath.Normalized.of_string tmpfile ];
Kernel.LogicalOperators.on ();
Constfold.off ();
Ast.compute();
if ProveAuxSpec.get () then begin
......
......@@ -52,9 +52,8 @@ extern int call_to_an_undefined_function(void);
T0_S2_tmp = T0_S2;
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
if (T0_S2 == 1) accept_S1_tmp = 1;
else
if (accept_S1 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
if (T0_S2 == 1 || accept_S1 == 1) accept_S1_tmp = 1;
else accept_S1_tmp = 0;
T0_init_tmp = 0;
T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
......@@ -159,9 +158,7 @@ int a(void)
accept_S1_tmp = accept_S1;
accept_S1_tmp = 0;
T0_init_tmp = 0;
if (T0_S2 == 1) T0_S2_tmp = 1;
else
if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
if (T0_S2 == 1 || accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
......
......@@ -271,12 +271,10 @@ int commit_trans(void)
accept_S4_tmp = accept_S4;
accept_init_tmp = accept_init;
accept_init_tmp = 0;
if (accept_S2 == 1)
if (status != 0) accept_S4_tmp = 1; else accept_S4_tmp = 0;
if (accept_S2 == 1 && status != 0) accept_S4_tmp = 1;
else accept_S4_tmp = 0;
accept_S3_tmp = 0;
if (accept_S2 == 1)
if (status == 0) accept_S2_tmp = 1; else accept_S2_tmp = 0;
if (accept_S2 == 1 && status == 0) accept_S2_tmp = 1;
else accept_S2_tmp = 0;
accept_S1_tmp = 0;
accept_S1 = accept_S1_tmp;
......
......@@ -144,9 +144,7 @@ int rr = 1;
accept_all_tmp = 0;
accept_S5_tmp = 0;
accept_S4_tmp = 0;
if (T0_S2 == 1)
if (rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
else accept_S3_tmp = 0;
if (T0_S2 == 1 && rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
T0_init_tmp = 0;
if (T0_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
......
......@@ -236,9 +236,7 @@ void opa(void)
accept_S3_tmp = accept_S3;
accept_all_tmp = accept_all;
accept_all_tmp = 0;
if (T1_S2 == 1)
if (rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
else accept_S3_tmp = 0;
if (T1_S2 == 1 && rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
T1_S2_tmp = 0;
T0_init_tmp = 0;
T0_S4_tmp = 0;
......
......@@ -217,9 +217,8 @@ int decode_int(char *s)
accept_S2_tmp = accept_S2;
accept_init_tmp = accept_init;
accept_init_tmp = 0;
if (accept_S1 == 1) accept_S2_tmp = 1;
else
if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
if (accept_S1 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
else accept_S2_tmp = 0;
accept_S1_tmp = 0;
accept_S1 = accept_S1_tmp;
accept_S2 = accept_S2_tmp;
......@@ -266,12 +265,10 @@ int decode_int(char *s)
accept_S2_tmp = accept_S2;
accept_init_tmp = accept_init;
accept_init_tmp = 0;
if (accept_S1 == 1) accept_S2_tmp = 1;
else
if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
if (accept_S1 == 1) accept_S1_tmp = 1;
else
if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
if (accept_S1 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
else accept_S2_tmp = 0;
if (accept_S1 == 1 || accept_S2 == 1) accept_S1_tmp = 1;
else accept_S1_tmp = 0;
accept_S1 = accept_S1_tmp;
accept_S2 = accept_S2_tmp;
accept_init = accept_init_tmp;
......
......@@ -106,11 +106,7 @@ int global_argc = 0;
accept_T2_tmp = 0;
T1_tmp = 0;
T0_init_tmp = 0;
if (S1 == 1) S1_tmp = 1;
else
if (T1 == 1)
if (global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
else S1_tmp = 0;
if (S1 == 1 || T1 == 1 && global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
T0_init = T0_init_tmp;
T1 = T1_tmp;
......
......@@ -106,11 +106,7 @@ int global_argc = 0;
accept_T2_tmp = 0;
T1_tmp = 0;
T0_init_tmp = 0;
if (S1 == 1) S1_tmp = 1;
else
if (T1 == 1)
if (global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
else S1_tmp = 0;
if (S1 == 1 || T1 == 1 && global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
T0_init = T0_init_tmp;
T1 = T1_tmp;
......@@ -419,9 +415,7 @@ int sumOne(char *t, int length)
T0_init_tmp = T0_init;
T1_tmp = T1;
accept_T2_tmp = accept_T2;
if (T1 == 1)
if (res == 1) accept_T2_tmp = 1; else accept_T2_tmp = 0;
else accept_T2_tmp = 0;
if (T1 == 1 && res == 1) accept_T2_tmp = 1; else accept_T2_tmp = 0;
if (T1 == 1) T1_tmp = 1; else T1_tmp = 0;
T0_init_tmp = 0;
S1_tmp = 0;
......
......@@ -58,9 +58,7 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
if (T0_S2 == 1) T0_S2_tmp = 1;
else
if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
......@@ -249,14 +247,10 @@ int countOne(char *argv)
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
accept_S2_tmp = accept_S2;
if (T0_S2 == 1) accept_S2_tmp = 1;
else
if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
if (T0_S2 == 1) accept_S1_tmp = 1;
else
if (accept_S1 == 1) accept_S1_tmp = 1;
else
if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
else accept_S2_tmp = 0;
if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
else accept_S1_tmp = 0;
T0_init_tmp = 0;
if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
......
......@@ -58,9 +58,7 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
if (T0_S2 == 1) T0_S2_tmp = 1;
else
if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
......@@ -247,14 +245,10 @@ int countOne(char *argv)
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
accept_S2_tmp = accept_S2;
if (T0_S2 == 1) accept_S2_tmp = 1;
else
if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
if (T0_S2 == 1) accept_S1_tmp = 1;
else
if (accept_S1 == 1) accept_S1_tmp = 1;
else
if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
else accept_S2_tmp = 0;
if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
else accept_S1_tmp = 0;
T0_init_tmp = 0;
if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
......
......@@ -58,9 +58,7 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
if (T0_S2 == 1) T0_S2_tmp = 1;
else
if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
......@@ -254,14 +252,10 @@ int countOne(char *argv)
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
accept_S2_tmp = accept_S2;
if (T0_S2 == 1) accept_S2_tmp = 1;
else
if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
if (T0_S2 == 1) accept_S1_tmp = 1;
else
if (accept_S1 == 1) accept_S1_tmp = 1;
else
if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
else accept_S2_tmp = 0;
if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
else accept_S1_tmp = 0;
T0_init_tmp = 0;
if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
......
......@@ -107,14 +107,9 @@ check lemma S0_deterministic_trans{L}:
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
if (3 == aorai_CurStates) {
if (x == 4) aorai_CurStates = S4; else goto _LAND;
}
else {
_LAND: ;
if (3 == aorai_CurStates)
if (x == 5) aorai_CurStates = S5;
}
if (3 == aorai_CurStates && x == 4) aorai_CurStates = S4;
else
if (3 == aorai_CurStates && x == 5) aorai_CurStates = S5;
return;
}
......@@ -231,8 +226,7 @@ void g(int x)
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if (1 == aorai_CurStates)
if (x == 4) aorai_CurStates = S3;
if (1 == aorai_CurStates && x == 4) aorai_CurStates = S3;
return;
}
......@@ -278,9 +272,7 @@ void g(int x)
{
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if (1 == aorai_CurStates)
if (res == 0)
if (X == 5) aorai_CurStates = S2;
if (1 == aorai_CurStates && (res == 0 && X == 5)) aorai_CurStates = S2;
return;
}
......@@ -351,14 +343,9 @@ int f(int x)
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_real_main;
if (0 == aorai_CurStates) {
if (c != 0) aorai_CurStates = S1; else goto _LAND;
}
else {
_LAND: ;
if (0 == aorai_CurStates)
if (c == 0) aorai_CurStates = S2;
}
if (0 == aorai_CurStates && c != 0) aorai_CurStates = S1;
else
if (0 == aorai_CurStates && c == 0) aorai_CurStates = S2;
return;
}
......
......@@ -132,21 +132,15 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if (7 == aorai_CurStates) {
if (x == 1) {
aorai_CurStates = aorai_intermediate_state;
aorai_x = x;
}
else goto _LAND;
}
else {
_LAND: ;
if (7 == aorai_CurStates)
if (x == 3) {
aorai_CurStates = aorai_intermediate_state_2;
aorai_x_0 = x;
}
if (7 == aorai_CurStates && x == 1) {
aorai_CurStates = aorai_intermediate_state;
aorai_x = x;
}
else
if (7 == aorai_CurStates && x == 3) {
aorai_CurStates = aorai_intermediate_state_2;
aorai_x_0 = x;
}
return;
}
......@@ -219,28 +213,13 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
{
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if (4 == aorai_CurStates) {
if (aorai_x_0 == 3) aorai_CurStates = OK; else goto _LAND_1;
}
else {
_LAND_1: ;
if (1 == aorai_CurStates) {
if (aorai_x == 1) aorai_CurStates = aorai_intermediate_state_0;
else goto _LAND_0;
}
else {
_LAND_0: ;
if (4 == aorai_CurStates) {
if (aorai_x_0 != 3) aorai_CurStates = aorai_reject;
else goto _LAND;
}
else {
_LAND: ;
if (1 == aorai_CurStates)
if (aorai_x != 1) aorai_CurStates = aorai_reject;
}
}
}
if (4 == aorai_CurStates && aorai_x_0 == 3) aorai_CurStates = OK;
else
if (1 == aorai_CurStates && aorai_x == 1) aorai_CurStates = aorai_intermediate_state_0;
else
if (4 == aorai_CurStates && aorai_x_0 != 3) aorai_CurStates = aorai_reject;
else
if (1 == aorai_CurStates && aorai_x != 1) aorai_CurStates = aorai_reject;
return;
}
......@@ -438,18 +417,13 @@ int f(int x)
{
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
if (3 == aorai_CurStates) {
if (aorai_y == 2) aorai_CurStates = OK; else goto _LAND;
}
else {
_LAND: ;
if (3 == aorai_CurStates && aorai_y == 2) aorai_CurStates = OK;
else
if (0 == aorai_CurStates) aorai_CurStates = OK;
else
if (5 == aorai_CurStates) aorai_CurStates = aorai_reject;
else
if (3 == aorai_CurStates)
if (aorai_y != 2) aorai_CurStates = aorai_reject;
}
if (3 == aorai_CurStates && aorai_y != 2) aorai_CurStates = aorai_reject;
return;
}
......
......@@ -315,14 +315,10 @@ int main_bhv_bhv(int c); */
aorai_reject_tmp = 0;
aorai_intermediate_state_2_tmp = 0;
aorai_intermediate_state_1_tmp = 0;
if (S0 == 1)
if (c <= 0) aorai_intermediate_state_0_tmp = 1;
else aorai_intermediate_state_0_tmp = 0;
if (S0 == 1 && c <= 0) aorai_intermediate_state_0_tmp = 1;
else aorai_intermediate_state_0_tmp = 0;
bhv_aux = main_bhv_bhv(c);
if (S0 == 1)
if (bhv_aux) aorai_intermediate_state_tmp = 1;
else aorai_intermediate_state_tmp = 0;
if (S0 == 1 && bhv_aux) aorai_intermediate_state_tmp = 1;
else aorai_intermediate_state_tmp = 0;
Sf_tmp = 0;
S0_tmp = 0;
......@@ -410,25 +406,17 @@ int main_bhv_bhv(int c); */
aorai_intermediate_state_1_tmp = aorai_intermediate_state_1;
aorai_intermediate_state_2_tmp = aorai_intermediate_state_2;
aorai_reject_tmp = aorai_reject;
if (aorai_intermediate_state_0 == 1) aorai_reject_tmp = 1;
else
if (aorai_intermediate_state_2 == 1) {
if (res != 0) aorai_reject_tmp = 1; else goto _LAND;
}
else {
_LAND: ;
if (aorai_reject == 1) aorai_reject_tmp = 1;
else aorai_reject_tmp = 0;
}
if ((aorai_intermediate_state_0 == 1 || aorai_intermediate_state_2 == 1 &&
res != 0) || aorai_reject == 1)
aorai_reject_tmp = 1;
else aorai_reject_tmp = 0;
aorai_intermediate_state_2_tmp = 0;
aorai_intermediate_state_1_tmp = 0;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
if (aorai_intermediate_state == 1) Sf_tmp = 1;
else
if (aorai_intermediate_state_2 == 1)
if (res == 0) Sf_tmp = 1; else Sf_tmp = 0;
else Sf_tmp = 0;
if (aorai_intermediate_state == 1 || aorai_intermediate_state_2 == 1 &&
res == 0) Sf_tmp = 1;
else Sf_tmp = 0;
S0_tmp = 0;
S0 = S0_tmp;
Sf = Sf_tmp;
......
......@@ -95,14 +95,10 @@ enum aorai_OpStatusList {
aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
aorai_intermediate_state_3_tmp = 0;
aorai_intermediate_state_2_tmp = 0;
if (aorai_intermediate_state == 1) aorai_intermediate_state_1_tmp = 1;
else
if (aorai_intermediate_state_0 == 1)
if (aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
else aorai_intermediate_state_1_tmp = 0;
else aorai_intermediate_state_1_tmp = 0;
if (aorai_intermediate_state_0 == 1)
if (aorai_counter < 5) aorai_counter ++;
if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1 &&
aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
else aorai_intermediate_state_1_tmp = 0;
if (aorai_intermediate_state_0 == 1 && aorai_counter < 5) aorai_counter ++;
if (aorai_intermediate_state == 1) aorai_counter = 1;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
......@@ -543,9 +539,9 @@ void g(void)
aorai_intermediate_state_1_tmp = 0;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
if (aorai_intermediate_state == 1) Sf_tmp = 1;
else
if (aorai_intermediate_state_0 == 1) Sf_tmp = 1; else Sf_tmp = 0;
if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1)
Sf_tmp = 1;
else Sf_tmp = 0;
S0_tmp = 0;
S0 = S0_tmp;
Sf = Sf_tmp;
......
......@@ -338,8 +338,7 @@ void g(void)
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_h;
if (4 == aorai_CurStates)
if (aorai_x > 0) aorai_CurStates = f_0;
if (4 == aorai_CurStates && aorai_x > 0) aorai_CurStates = f_0;
return;
}
......
......@@ -39,9 +39,7 @@ enum aorai_OpStatusList {
aorai_CurOperation = op_f;
S0_tmp = S0;
Sf_tmp = Sf;
if (S0 == 1)
if (x >= 4) Sf_tmp = 1; else Sf_tmp = 0;
else Sf_tmp = 0;
if (S0 == 1 && x >= 4) Sf_tmp = 1; else Sf_tmp = 0;
S0_tmp = 0;
S0 = S0_tmp;
Sf = Sf_tmp;
......
......@@ -65,42 +65,13 @@ int x = 0;
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
if (init == 1) {
if (x == 3) step1_tmp = 1; else goto _LAND_0;
}
else {
_LAND_0: ;
if (last == 1) {
if (x == 3) step1_tmp = 1; else goto _LAND;
}
else {
_LAND: ;
if (step1 == 1)
if (x != 4) step1_tmp = 1; else step1_tmp = 0;
else step1_tmp = 0;
}
}
if (last == 1) {
if (x != 4) {
if (x != 3) last_tmp = 1; else goto _LAND_1;
}
else goto _LAND_1;
}
else {
_LAND_1: ;
if (step1 == 1)
if (x == 4) last_tmp = 1; else last_tmp = 0;
else last_tmp = 0;
}
if (init == 1) {
if (x != 3) init_tmp = 1; else goto _LAND_2;
}
else {
_LAND_2: ;
if (last == 1)
if (x == 4) init_tmp = 1; else init_tmp = 0;
else init_tmp = 0;
}
if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4)
step1_tmp = 1;
else step1_tmp = 0;
if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
else last_tmp = 0;
if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
else init_tmp = 0;
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
......@@ -157,42 +128,13 @@ int x = 0;
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
if (init == 1) {
if (x == 3) step1_tmp = 1; else goto _LAND_0;
}
else {
_LAND_0: ;
if (last == 1) {
if (x == 3) step1_tmp = 1; else goto _LAND;
}
else {
_LAND: ;
if (step1 == 1)
if (x != 4) step1_tmp = 1; else step1_tmp = 0;
else step1_tmp = 0;
}
}
if (last == 1) {
if (x != 4) {
if (x != 3) last_tmp = 1; else goto _LAND_1;
}
else goto _LAND_1;
}
else {
_LAND_1: ;
if (step1 == 1)
if (x == 4) last_tmp = 1; else last_tmp = 0;
else last_tmp = 0;
}
if (init == 1) {
if (x != 3) init_tmp = 1; else goto _LAND_2;
}
else {