diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index c192b4c348ec4da230f4942f290f2a3d8f78f25c..1a270032c6bd862f3f7e72a62e0f2f4573925039 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -835,12 +835,14 @@ let is_state_pred state =
(Req,one_term(),
Logic_const.tvar (Data_for_aorai.get_state_logic_var state))
-let is_state_stmt (state,copy) loc =
- if Aorai_option.Deterministic.get ()
- then
- mkStmtOneInstr
- ~ghost:true (Set (Cil.var copy, int2enumstate_exp loc state.nums, loc))
- else mkStmtOneInstr ~ghost:true (Set (Cil.var copy, Cil.one loc, loc))
+let is_state_non_det_stmt (_,copy) loc =
+ mkStmtOneInstr ~ghost:true (Set (Cil.var copy, Cil.one loc, loc))
+
+let is_state_det_stmt state loc =
+ let var = Data_for_aorai.get_varinfo curState in
+ mkStmtOneInstr
+ ~ghost:true (Set (Cil.var var, int2enumstate_exp loc state.nums, loc))
+
let is_state_exp state loc =
if Aorai_option.Deterministic.get ()
@@ -1901,173 +1903,173 @@ let act_convert loc act res =
in
List.map treat_one_act act
-let copy_stmt s =
- let vis = new Visitor.frama_c_refresh (Project.current()) in
- Visitor.visitFramacStmt vis s
+let mk_transitions_stmt generated_kf loc f st res trans =
+ List.fold_right
+ (fun trans
+ (aux_stmts, aux_vars, new_funcs, exp_from_trans, stmt_from_action) ->
+ let (tr_stmts, tr_vars, tr_funcs, exp) =
+ crosscond_to_exp generated_kf f st loc trans.cross res
+ in
+ let cond = Cil.mkBinOp loc LAnd (is_state_exp trans.start loc) exp in
+ (tr_stmts @ aux_stmts,
+ tr_vars @ aux_vars,
+ Cil_datatype.Varinfo.Set.union tr_funcs new_funcs,
+ Cil.mkBinOp loc LOr exp_from_trans cond,
+ (Cil.copy_exp cond, act_convert loc trans.actions res)
+ :: stmt_from_action))
+ trans
+ ([],[],Cil_datatype.Varinfo.Set.empty, Cil.zero ~loc, [])
+
+let mkIfStmt loc exp1 block1 block2 =
+ Cil.mkStmt ~ghost:true (If (exp1, block1, block2, loc))
+
+let mk_deterministic_stmt
+ generated_kf loc auto f fst status ret state
+ (other_stmts, other_funcs, other_vars, trans_stmts as res) =
+ if is_reachable state status then begin
+ let trans = get_accessible_transitions auto state status in
+ let aux_stmts, aux_vars, aux_funcs, _, stmt_from_action =
+ mk_transitions_stmt generated_kf loc f fst ret trans
+ in
+ let stmts =
+ List.fold_left
+ (fun acc (cond, stmt_act) ->
+ [mkIfStmt loc cond
+ (mkBlock (is_state_det_stmt state loc :: stmt_act))
+ (mkBlock acc)])
+ trans_stmts
+ (List.rev stmt_from_action)
+ in
+ aux_stmts @ other_stmts,
+ Cil_datatype.Varinfo.Set.union aux_funcs other_funcs,
+ aux_vars @ other_vars,
+ stmts
+ end else res
-(* mk_stmt loc (states, tr) f fst status state
+(* mk_non_deterministic_stmt loc (states, tr) f fst status state
Generates the statement updating the variable representing
the state argument.
If state is reachable, generates a "If then else" statement, else it is
just an assignment.
Used in auto_func_block. *)
-let mk_stmt generated_kf loc (states, tr) f fst status ((st,_) as state) res =
+let mk_non_deterministic_stmt
+ generated_kf loc (states, tr) f fst status ((st,_) as state) res =
if is_reachable st status then begin
let useful_trans = get_accessible_transitions (states,tr) st status in
- let aux_stmts, new_vars, new_funcs, exp_from_trans,stmt_from_action =
- List.fold_right
- (fun trans
- (aux_stmts, aux_vars, new_funcs, exp_from_trans, stmt_from_action) ->
- let (tr_stmts, tr_vars, tr_funcs, exp) =
- crosscond_to_exp generated_kf f fst loc trans.cross res
- in
- (tr_stmts @ aux_stmts,
- tr_vars @ aux_vars,
- Cil_datatype.Varinfo.Set.union tr_funcs new_funcs,
- Cil.mkBinOp loc LAnd (is_state_exp trans.start loc) exp
- ::exp_from_trans,
- act_convert loc trans.actions res :: stmt_from_action))
- useful_trans
- ([],[],Cil_datatype.Varinfo.Set.empty, [], [])
- in
- let mkIfStmt exp1 block1 block2 =
- Cil.mkStmt ~ghost:true (If (exp1, block1, block2, loc))
- in
- let if_cond =
- List.fold_left
- (fun acc exp -> Cil.mkBinOp loc LOr exp acc)
- (List.hd exp_from_trans)
- (List.tl exp_from_trans)
- in
- let then_stmt = is_state_stmt state loc in
- let else_stmt =
- if Aorai_option.Deterministic.get () then []
- else [is_out_of_state_stmt state loc]
+ let aux_stmts, new_vars, new_funcs, cond,stmt_from_action =
+ mk_transitions_stmt generated_kf loc f fst res useful_trans
in
+ let then_stmt = is_state_non_det_stmt state loc in
+ let else_stmt = [is_out_of_state_stmt state loc] in
let trans_stmts =
- if Aorai_option.Deterministic.get () then
- List.fold_left2
- (fun acc cond stmt_act ->
- [mkIfStmt cond
- (mkBlock (copy_stmt then_stmt :: stmt_act)) (mkBlock acc)])
- else_stmt
- (List.rev exp_from_trans)
+ let actions =
+ List.fold_left
+ (fun acc (cond, stmt_act) ->
+ if stmt_act = [] then acc
+ else
+ (mkIfStmt loc cond (mkBlock stmt_act) (mkBlock []))::acc)
+ []
(List.rev stmt_from_action)
- else
- let actions =
- List.fold_left2
- (fun acc cond stmt_act ->
- if stmt_act = [] then acc
- else
- (mkIfStmt cond (mkBlock stmt_act) (mkBlock []))::acc)
- []
- (List.rev exp_from_trans)
- (List.rev stmt_from_action)
- in
- mkIfStmt if_cond (mkBlock [then_stmt]) (mkBlock else_stmt) :: actions
+ in
+ mkIfStmt loc cond (mkBlock [then_stmt]) (mkBlock else_stmt) :: actions
in
new_funcs, new_vars, aux_stmts @ trans_stmts
end else
- if Aorai_option.Deterministic.get () then
- Cil_datatype.Varinfo.Set.empty, [], []
- else Cil_datatype.Varinfo.Set.empty, [], [is_out_of_state_stmt state loc]
+ Cil_datatype.Varinfo.Set.empty, [], [is_out_of_state_stmt state loc]
-let auto_func_block generated_kf loc f st status res =
- let dkey = func_body_dkey in
- let call_or_ret =
- match st with
- | Promelaast.Call -> "call"
- | Promelaast.Return -> "return"
+let equalsStmt lval exp loc = (* assignment *)
+ Cil.mkStmtOneInstr ~ghost:true (Set (lval, exp, loc))
+
+let mk_deterministic_body generated_kf loc f st status res =
+ let (states, _ as auto) = Data_for_aorai.getGraph() in
+ let aux_stmts, aux_funcs, aux_vars, trans_stmts =
+ List.fold_right
+ (mk_deterministic_stmt generated_kf loc auto f st status res)
+ states
+ ([], Cil_datatype.Varinfo.Set.empty, [],[])
in
- Aorai_option.debug
- ~dkey "func code for %a (%s)" Kernel_function.pretty f call_or_ret;
- let (states, _) as auto = Data_for_aorai.getGraph() in
+ aux_funcs, aux_vars, aux_stmts @ trans_stmts
+let mk_non_deterministic_body generated_kf loc f st status res =
(* For the following tests, we need a copy of every state. *)
-
+ let (states, _) as auto = Data_for_aorai.getGraph() in
let copies, local_var =
- if Aorai_option.Deterministic.get () then begin
- let orig = Data_for_aorai.get_varinfo curState in
- let copy = Cil.copyVarinfo orig (orig.vname ^ "_tmp") in
- copy.vglob <- false;
- List.map (fun st -> (st, copy)) states, [copy]
- end else begin
- let bindings =
- List.map
- (fun st ->
- let state_var = Data_for_aorai.get_state_var st in
- let copy = Cil.copyVarinfo state_var (state_var.vname ^ "_tmp") in
- copy.vglob <- false;
- (st,copy))
- states
- in bindings, snd (List.split bindings)
- end
- in
- let equalsStmt lval exp = (* assignment *)
- Cil.mkStmtOneInstr ~ghost:true (Set (lval, exp, loc))
- in
- let stmt_begin_list =
-
- [
- (* First statement : what is the current status : called or return ? *)
- equalsStmt
- (Cil.var (Data_for_aorai.get_varinfo Data_for_aorai.curOpStatus)) (* current status... *)
- (Cil.new_exp loc (Const (Data_for_aorai.op_status_to_cenum st))); (* ... equals to what it is *)
-
- (* Second statement : what is the current operation, i.e. which function ? *)
- equalsStmt
- (Cil.var (Data_for_aorai.get_varinfo Data_for_aorai.curOp)) (* current operation ... *)
- (Cil.new_exp loc (Const (Data_for_aorai.func_to_cenum (Kernel_function.get_name f)))) (* ...equals to what it is *)
- ]
-
+ let bindings =
+ List.map
+ (fun st ->
+ let state_var = Data_for_aorai.get_state_var st in
+ let copy = Cil.copyVarinfo state_var (state_var.vname ^ "_tmp") in
+ copy.vglob <- false;
+ (st,copy))
+ states
+ in bindings, snd (List.split bindings)
in
-
- (* As we work on copies, they need to be set to their actual values *)
-
let copies_update =
- if Aorai_option.Deterministic.get () then
- let orig = Data_for_aorai.get_varinfo curState in
- [ equalsStmt (Cil.var (List.hd local_var)) (Cil.evar ~loc orig) ]
- else
- List.map
- (fun (st,copy) ->
- equalsStmt (Cil.var copy)
- (Cil.evar ~loc (Data_for_aorai.get_state_var st)))
- copies
+ List.map
+ (fun (st,copy) ->
+ equalsStmt (Cil.var copy)
+ (Cil.evar ~loc (Data_for_aorai.get_state_var st)) loc)
+ copies
in
- (* For each state, we have to generate the statement that will update its copy. *)
let new_funcs, local_var, main_stmt =
-
List.fold_left
(fun (new_funcs, aux_vars, stmts) state ->
let my_funcs, my_vars, my_stmts =
- mk_stmt generated_kf loc auto f st status state res
+ mk_non_deterministic_stmt generated_kf loc auto f st status state res
in
Cil_datatype.Varinfo.Set.union my_funcs new_funcs,
my_vars @ aux_vars,
my_stmts@stmts )
(Cil_datatype.Varinfo.Set.empty, local_var, [])
copies
-
in
(* Finally, we replace the state var values by the ones computed in copies. *)
let stvar_update =
- if Aorai_option.Deterministic.get () then
- let orig = Data_for_aorai.get_varinfo curState in
- [ equalsStmt (Cil.var orig) (Cil.evar (List.hd local_var))]
+ List.map
+ (fun (state,copy) ->
+ equalsStmt
+ (Cil.var (Data_for_aorai.get_state_var state))
+ (Cil.evar ~loc copy) loc)
+ copies
+ in
+ new_funcs, local_var, copies_update @ main_stmt @ stvar_update
+
+let auto_func_block generated_kf loc f st status res =
+ let dkey = func_body_dkey in
+ let call_or_ret =
+ match st with
+ | Promelaast.Call -> "call"
+ | Promelaast.Return -> "return"
+ in
+ Aorai_option.debug
+ ~dkey "func code for %a (%s)" Kernel_function.pretty f call_or_ret;
+
+ let stmt_begin_list =
+ [
+ (* First statement : what is the current status : called or return ? *)
+ equalsStmt
+ (Cil.var (Data_for_aorai.get_varinfo Data_for_aorai.curOpStatus))
+ (Cil.new_exp loc (Const (Data_for_aorai.op_status_to_cenum st))) loc;
+ (* Second statement : what is the current operation,
+ i.e. which function ? *)
+ equalsStmt
+ (Cil.var (Data_for_aorai.get_varinfo Data_for_aorai.curOp))
+ (Cil.new_exp loc
+ (Const (Data_for_aorai.func_to_cenum (Kernel_function.get_name f))))
+ loc
+ ]
+ in
+ let new_funcs, local_var, main_stmt =
+ if Aorai_option.Deterministic.get() then
+ mk_deterministic_body generated_kf loc f st status res
else
- List.map
- (fun (state,copy) ->
- equalsStmt
- (Cil.var (Data_for_aorai.get_state_var state))
- (Cil.evar ~loc copy))
- copies
+ mk_non_deterministic_body generated_kf loc f st status res
in
let ret = [ Cil.mkStmt ~ghost:true (Cil_types.Return(None,loc)) ] in
let res_block =
(Cil.mkBlock
- ( stmt_begin_list @ copies_update @ main_stmt @ stvar_update @ ret))
+ ( stmt_begin_list @ main_stmt @ ret))
in
res_block.blocals <- local_var;
Aorai_option.debug ~dkey "Generated body is:@\n%a"
diff --git a/src/plugins/aorai/aorai_utils.mli b/src/plugins/aorai/aorai_utils.mli
index 0bc659364f45321b358bd845405c89e5d06020d8..efb8b12df79c276e22688cf01d55f06fe5e1e61a 100644
--- a/src/plugins/aorai/aorai_utils.mli
+++ b/src/plugins/aorai/aorai_utils.mli
@@ -71,9 +71,6 @@ val host_state_term: unit -> Cil_types.term_lval
corresponding state. *)
val is_state_pred: state -> predicate
-(** Returns the statement saying the state is affected *)
-val is_state_stmt: state * Cil_types.varinfo -> location -> Cil_types.stmt
-
(** Returns the boolean expression saying the state is affected *)
val is_state_exp: state -> location -> Cil_types.exp
diff --git a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
index 7b3833fb8c530be00f93100df610e7986540081f..fd7526444df55abd2c128af76809b32c0a411955 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
@@ -60,12 +60,9 @@ int X;
@/
void f_pre_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
- aorai_CurStates_tmp = aorai_CurStates;
- if (3 == aorai_CurStates) aorai_CurStates_tmp = S_in_f;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (3 == aorai_CurStates) aorai_CurStates = S_in_f;
return;
}
@@ -99,12 +96,9 @@ int X;
@/
void f_post_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
- aorai_CurStates_tmp = aorai_CurStates;
- if (2 == aorai_CurStates) aorai_CurStates_tmp = in_main;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (2 == aorai_CurStates) aorai_CurStates = in_main;
return;
}
@@ -151,12 +145,9 @@ void f(void)
@/
void main_pre_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
- aorai_CurStates_tmp = aorai_CurStates;
- if (0 == aorai_CurStates) aorai_CurStates_tmp = Sf;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (0 == aorai_CurStates) aorai_CurStates = Sf;
return;
}
@@ -190,12 +181,9 @@ void f(void)
@/
void main_post_func(int res)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
- aorai_CurStates_tmp = aorai_CurStates;
- if (4 == aorai_CurStates) aorai_CurStates_tmp = S2;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (4 == aorai_CurStates) aorai_CurStates = S2;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
index ab55916b9af828248a4309cdc6424442f8027441..7141a6e19585342e2f1f9571efaa71e68c2ba704 100644
--- a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
@@ -61,12 +61,9 @@ check lemma I_deterministic_trans{L}:
@/
void main_pre_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
- aorai_CurStates_tmp = aorai_CurStates;
- if (0 == aorai_CurStates) aorai_CurStates_tmp = I;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (0 == aorai_CurStates) aorai_CurStates = I;
return;
}
@@ -88,12 +85,9 @@ check lemma I_deterministic_trans{L}:
@/
void main_post_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
- aorai_CurStates_tmp = aorai_CurStates;
- if (0 == aorai_CurStates) aorai_CurStates_tmp = I;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (0 == aorai_CurStates) aorai_CurStates = I;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
index 5a30e59e7d5e51dd0849a5f48c908fbe5493e073..8e648b2ea61129f84dbd19578c474b63943ede22 100644
--- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
@@ -105,15 +105,16 @@ check lemma S0_deterministic_trans{L}:
@/
void g_pre_func(int x)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
- aorai_CurStates_tmp = aorai_CurStates;
- if (3 == aorai_CurStates)
- if (x == 5) aorai_CurStates_tmp = S5;
- if (3 == aorai_CurStates)
- if (x == 4) aorai_CurStates_tmp = S4;
- aorai_CurStates = aorai_CurStates_tmp;
+ 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;
+ }
return;
}
@@ -161,13 +162,11 @@ check lemma S0_deterministic_trans{L}:
@/
void g_post_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
- aorai_CurStates_tmp = aorai_CurStates;
- if (4 == aorai_CurStates) aorai_CurStates_tmp = S3;
- if (5 == aorai_CurStates) aorai_CurStates_tmp = S1;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (5 == aorai_CurStates) aorai_CurStates = S1;
+ else
+ if (4 == aorai_CurStates) aorai_CurStates = S3;
return;
}
@@ -230,13 +229,10 @@ void g(int x)
@/
void f_pre_func(int x)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
- aorai_CurStates_tmp = aorai_CurStates;
if (1 == aorai_CurStates)
- if (x == 4) aorai_CurStates_tmp = S3;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (x == 4) aorai_CurStates = S3;
return;
}
@@ -280,14 +276,11 @@ void g(int x)
@/
void f_post_func(int res)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
- aorai_CurStates_tmp = aorai_CurStates;
if (1 == aorai_CurStates)
if (res == 0)
- if (X == 5) aorai_CurStates_tmp = S2;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (X == 5) aorai_CurStates = S2;
return;
}
@@ -356,15 +349,16 @@ int f(int x)
@/
void real_main_pre_func(int c)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_real_main;
- aorai_CurStates_tmp = aorai_CurStates;
- if (0 == aorai_CurStates)
- if (c == 0) aorai_CurStates_tmp = S2;
- if (0 == aorai_CurStates)
- if (c != 0) aorai_CurStates_tmp = S1;
- aorai_CurStates = aorai_CurStates_tmp;
+ 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;
+ }
return;
}
@@ -407,12 +401,9 @@ int f(int x)
@/
void real_main_post_func(int res)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_real_main;
- aorai_CurStates_tmp = aorai_CurStates;
- if (2 == aorai_CurStates) aorai_CurStates_tmp = Sf;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (2 == aorai_CurStates) aorai_CurStates = Sf;
return;
}
@@ -471,12 +462,9 @@ int real_main(int c)
@/
void main_pre_func(int c)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
- aorai_CurStates_tmp = aorai_CurStates;
- if (7 == aorai_CurStates) aorai_CurStates_tmp = S0;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (7 == aorai_CurStates) aorai_CurStates = S0;
return;
}
@@ -519,12 +507,9 @@ int real_main(int c)
@/
void main_post_func(int res)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
- aorai_CurStates_tmp = aorai_CurStates;
- if (6 == aorai_CurStates) aorai_CurStates_tmp = Sf;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (6 == aorai_CurStates) aorai_CurStates = Sf;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
index 3fa9613a782d0cd189af5fb61fae70e89db84d9f..4e41dd7f696e65d3b5b363d4a952c1560a6d5b9f 100644
--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -124,21 +124,23 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
@/
void f_pre_func(int x)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
- aorai_CurStates_tmp = aorai_CurStates;
- if (7 == aorai_CurStates)
- if (x == 3) {
- aorai_CurStates_tmp = aorai_intermediate_state_2;
- aorai_x_0 = x;
- }
- if (7 == aorai_CurStates)
+ if (7 == aorai_CurStates) {
if (x == 1) {
- aorai_CurStates_tmp = aorai_intermediate_state;
+ aorai_CurStates = aorai_intermediate_state;
aorai_x = x;
}
- aorai_CurStates = aorai_CurStates_tmp;
+ else goto _LAND;
+ }
+ else {
+ _LAND: ;
+ if (7 == aorai_CurStates)
+ if (x == 3) {
+ aorai_CurStates = aorai_intermediate_state_2;
+ aorai_x_0 = x;
+ }
+ }
return;
}
@@ -209,24 +211,30 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
@/
void f_post_func(int res)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
- aorai_CurStates_tmp = aorai_CurStates;
if (4 == aorai_CurStates) {
- if (aorai_x_0 != 3) aorai_CurStates_tmp = aorai_reject;
- else goto _LAND;
+ if (aorai_x_0 == 3) aorai_CurStates = OK; else goto _LAND_1;
}
else {
- _LAND: ;
- if (1 == aorai_CurStates)
- if (aorai_x != 1) aorai_CurStates_tmp = aorai_reject;
+ _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 (1 == aorai_CurStates)
- if (aorai_x == 1) aorai_CurStates_tmp = aorai_intermediate_state_0;
- if (4 == aorai_CurStates)
- if (aorai_x_0 == 3) aorai_CurStates_tmp = OK;
- aorai_CurStates = aorai_CurStates_tmp;
return;
}
@@ -347,17 +355,16 @@ int f(int x)
@/
void g_pre_func(int y)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
- aorai_CurStates_tmp = aorai_CurStates;
- if (5 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject;
- if (2 == aorai_CurStates) {
- aorai_CurStates_tmp = aorai_intermediate_state_1;
- aorai_y = y;
- }
- if (0 == aorai_CurStates) aorai_CurStates_tmp = OK;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (0 == aorai_CurStates) aorai_CurStates = OK;
+ else
+ if (2 == aorai_CurStates) {
+ aorai_CurStates = aorai_intermediate_state_1;
+ aorai_y = y;
+ }
+ else
+ if (5 == aorai_CurStates) aorai_CurStates = aorai_reject;
return;
}
@@ -420,22 +427,20 @@ int f(int x)
@/
void g_post_func(int res)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
- aorai_CurStates_tmp = aorai_CurStates;
- if (5 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject;
- else
- if (3 == aorai_CurStates)
- if (aorai_y != 2) aorai_CurStates_tmp = aorai_reject;
if (3 == aorai_CurStates) {
- if (aorai_y == 2) aorai_CurStates_tmp = OK; else goto _LAND;
+ if (aorai_y == 2) aorai_CurStates = OK; else goto _LAND;
}
else {
_LAND: ;
- if (0 == aorai_CurStates) aorai_CurStates_tmp = OK;
+ 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;
}
- aorai_CurStates = aorai_CurStates_tmp;
return;
}
@@ -514,12 +519,9 @@ int g(int y)
@/
void main_pre_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
- aorai_CurStates_tmp = aorai_CurStates;
- if (6 == aorai_CurStates) aorai_CurStates_tmp = main_0;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (6 == aorai_CurStates) aorai_CurStates = main_0;
return;
}
@@ -567,13 +569,11 @@ int g(int y)
@/
void main_post_func(int res)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
- aorai_CurStates_tmp = aorai_CurStates;
- if (5 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject;
- if (0 == aorai_CurStates) aorai_CurStates_tmp = OK;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (0 == aorai_CurStates) aorai_CurStates = OK;
+ else
+ if (5 == aorai_CurStates) aorai_CurStates = aorai_reject;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
index 3913f00e2f485fad13453eb892e7fcc28f412f75..ccfb249eba5eb4f3b759bba09f44a869117caa21 100644
--- a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
@@ -33,11 +33,8 @@ int f(void);
@/
void main_pre_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
- aorai_CurStates_tmp = aorai_CurStates;
- aorai_CurStates = aorai_CurStates_tmp;
return;
}
@@ -54,11 +51,8 @@ int f(void);
@/
void main_post_func(int res)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
- aorai_CurStates_tmp = aorai_CurStates;
- aorai_CurStates = aorai_CurStates_tmp;
return;
}
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 0b3bcf3d45f628b37e1d9a3290724d593ededdce..2f740e907d67b768924e4ecbe361e49c581f4c00 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -103,16 +103,13 @@ check lemma e_deterministic_trans{L}:
@/
void f_pre_func(int x)
{
- 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_CurStates = c;
aorai_y = aorai_x;
aorai_x = x;
}
- aorai_CurStates = aorai_CurStates_tmp;
return;
}
@@ -158,12 +155,9 @@ check lemma e_deterministic_trans{L}:
@/
void f_post_func(void)
{
- 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;
+ if (2 == aorai_CurStates) aorai_CurStates = e;
return;
}
@@ -227,12 +221,9 @@ void f(int x)
@/
void g_pre_func(void)
{
- 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;
+ if (1 == aorai_CurStates) aorai_CurStates = d;
return;
}
@@ -278,12 +269,9 @@ void f(int x)
@/
void g_post_func(void)
{
- 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;
+ if (3 == aorai_CurStates) aorai_CurStates = g_0;
return;
}
@@ -342,13 +330,10 @@ void g(void)
@/
void h_pre_func(int x)
{
- 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;
+ if (aorai_x > 0) aorai_CurStates = f_0;
return;
}
@@ -394,12 +379,9 @@ void g(void)
@/
void h_post_func(void)
{
- 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;
+ if (5 == aorai_CurStates) aorai_CurStates = g_0;
return;
}
@@ -458,12 +440,9 @@ void h(int x)
@/
void i_pre_func(void)
{
- 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;
+ if (6 == aorai_CurStates) aorai_CurStates = h_0;
return;
}
@@ -514,16 +493,13 @@ void h(int x)
@/
void i_post_func(void)
{
- 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_CurStates = e;
aorai_y = 0;
aorai_x = 1;
}
- aorai_CurStates = aorai_CurStates_tmp;
return;
}
@@ -587,12 +563,9 @@ void i(void)
@/
void main_pre_func(int t)
{
- 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;
+ if (0 == aorai_CurStates) aorai_CurStates = b;
return;
}
@@ -638,12 +611,9 @@ void i(void)
@/
void main_post_func(void)
{
- 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;
+ if (4 == aorai_CurStates) aorai_CurStates = i_0;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
index 5df73b9c95c31edffe2319c7c773b93acfa13b23..86ceb3e991278c964faf62706c167f6710087817 100644
--- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
@@ -64,14 +64,11 @@ check lemma Init_deterministic_trans{L}:
@/
void f_pre_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
- aorai_CurStates_tmp = aorai_CurStates;
- if (2 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject;
+ if (2 == aorai_CurStates) aorai_CurStates = aorai_reject;
else
- if (1 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (1 == aorai_CurStates) aorai_CurStates = aorai_reject;
return;
}
@@ -99,12 +96,9 @@ check lemma Init_deterministic_trans{L}:
@/
void f_post_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
- aorai_CurStates_tmp = aorai_CurStates;
- if (2 == aorai_CurStates) aorai_CurStates_tmp = aorai_reject;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (2 == aorai_CurStates) aorai_CurStates = aorai_reject;
return;
}
@@ -145,11 +139,8 @@ void f(void)
@/
void main_pre_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
- aorai_CurStates_tmp = aorai_CurStates;
- aorai_CurStates = aorai_CurStates_tmp;
return;
}
@@ -172,11 +163,8 @@ void f(void)
@/
void main_post_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
- aorai_CurStates_tmp = aorai_CurStates;
- aorai_CurStates = aorai_CurStates_tmp;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
index 61c74befdb48b9cefe767cb5d067e8b3b9437886..d036e4e44939b3d91ffec9da6606f8670f5c7463 100644
--- a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
@@ -86,14 +86,11 @@ check lemma emptying_stack_deterministic_trans{L}:
@/
void push_pre_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_push;
- aorai_CurStates_tmp = aorai_CurStates;
- if (3 == aorai_CurStates) aorai_CurStates_tmp = filling_stack;
+ if (3 == aorai_CurStates) aorai_CurStates = filling_stack;
else
- if (1 == aorai_CurStates) aorai_CurStates_tmp = filling_stack;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (1 == aorai_CurStates) aorai_CurStates = filling_stack;
return;
}
@@ -132,15 +129,12 @@ check lemma emptying_stack_deterministic_trans{L}:
@/
void push_post_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_push;
- aorai_CurStates_tmp = aorai_CurStates;
if (4 == aorai_CurStates) {
- aorai_CurStates_tmp = filled_stack;
+ aorai_CurStates = filled_stack;
aorai_n ++;
}
- aorai_CurStates = aorai_CurStates_tmp;
return;
}
@@ -204,13 +198,10 @@ void push(void)
@/
void pop_pre_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_pop;
- aorai_CurStates_tmp = aorai_CurStates;
if (3 == aorai_CurStates)
- if (aorai_n > 0) aorai_CurStates_tmp = emptying_stack;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (aorai_n > 0) aorai_CurStates = emptying_stack;
return;
}
@@ -258,21 +249,23 @@ void push(void)
@/
void pop_post_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_pop;
- aorai_CurStates_tmp = aorai_CurStates;
- if (2 == aorai_CurStates)
- if (aorai_n > 1) {
- aorai_CurStates_tmp = filled_stack;
- aorai_n --;
- }
- if (2 == aorai_CurStates)
+ if (2 == aorai_CurStates) {
if (aorai_n == 1) {
- aorai_CurStates_tmp = empty_stack;
+ aorai_CurStates = empty_stack;
aorai_n --;
}
- aorai_CurStates = aorai_CurStates_tmp;
+ else goto _LAND;
+ }
+ else {
+ _LAND: ;
+ if (2 == aorai_CurStates)
+ if (aorai_n > 1) {
+ aorai_CurStates = filled_stack;
+ aorai_n --;
+ }
+ }
return;
}
@@ -338,15 +331,12 @@ void pop(void)
@/
void main_pre_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
- aorai_CurStates_tmp = aorai_CurStates;
if (5 == aorai_CurStates) {
- aorai_CurStates_tmp = empty_stack;
+ aorai_CurStates = empty_stack;
aorai_n = 0;
}
- aorai_CurStates = aorai_CurStates_tmp;
return;
}
@@ -383,12 +373,9 @@ void pop(void)
@/
void main_post_func(void)
{
- int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
- aorai_CurStates_tmp = aorai_CurStates;
- if (1 == aorai_CurStates) aorai_CurStates_tmp = accept;
- aorai_CurStates = aorai_CurStates_tmp;
+ if (1 == aorai_CurStates) aorai_CurStates = accept;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
index 7655e180602256ff7618173c8a157ec9f4bc2b63..e5437b11cf441f0122b9d89b3ba1147984506890 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
@@ -3,5 +3,5 @@
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing TMPDIR/aorai_incorrect_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0.i:65: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0.i:62: Warning:
Neither code nor specification for function f, generating default assigns from the prototype