diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index b17dd3dae1bb60c238aeee9060a17c1373bc52dd..85aaa035683674b2ba9102556cacfb38e5d9b421 100644
--- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml
+++ b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
@@ -23,4 +23,18 @@
(* *)
(**************************************************************************)
-let setup () = ()
+let add_slevel_annotation vi kind =
+ match kind with
+ | Aorai_visitors.Aux_funcs.(Pre _ | Post _) ->
+ let kf = Globals.Functions.get vi in
+ let stmt = Kernel_function.find_first_stmt kf
+ and loc = Kernel_function.get_location kf
+ and emitter = Aorai_option.emitter in
+ Eva.Eva_annotations.(add_slevel_annot ~emitter ~loc stmt SlevelFull)
+ | _ -> ()
+
+let add_slevel_annotations () =
+ Aorai_visitors.Aux_funcs.iter add_slevel_annotation
+
+let setup () =
+ add_slevel_annotations ()
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index d5bbcfd954e886769509a08481a9420268de9ec5..7011f12d5203984c63fdb67f99868eb3036a257f 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -61,26 +61,37 @@ let get_call_name exp = match exp.enode with
not be projectified.
*)
-(* the various kinds of auxiliary functions. *)
-type func_auto_mode =
- | Not_auto_func (* original C function. *)
- | Aux_func of kernel_function
- (* Checks whether we are in the corresponding behavior of the function. *)
- | Pre_func of kernel_function
- (* Pre_func f denotes a function updating the automaton when f is called. *)
- | Post_func of kernel_function
- (* Post_func f denotes a function updating the automaton
- when returning from f. *)
-
-(* table from auxiliary functions to the corresponding original one. *)
-let func_orig_table = Cil_datatype.Varinfo.Hashtbl.create 17
-
-let add_aux_bhv orig_kf vi =
- Cil_datatype.Varinfo.Hashtbl.add func_orig_table vi (Aux_func orig_kf)
-
-let kind_of_func vi =
- try Cil_datatype.Varinfo.Hashtbl.find func_orig_table vi
- with Not_found -> Not_auto_func
+module Aux_funcs =
+struct
+ (* the various kinds of auxiliary functions. *)
+ type kind =
+ | Not_aux_func (* original C function. *)
+ | Aux of kernel_function
+ (* Checks whether we are in the corresponding behavior of the function. *)
+ | Pre of kernel_function
+ (* Pre_func f denotes a function updating the automaton when f is called. *)
+ | Post of kernel_function
+ (* Post_func f denotes a function updating the automaton
+ when returning from f. *)
+
+ module Table = Cil_datatype.Varinfo.Hashtbl
+
+ (* table from auxiliary functions to the corresponding original one. *)
+ let table = Table.create 17
+
+ let add vi kind =
+ Table.add table vi kind
+
+ let add_aux kf vi =
+ add vi (Aux kf)
+
+ let kind vi =
+ try Table.find table vi with Not_found -> Not_aux_func
+
+ let iter f =
+ Table.iter f table
+end
+
(* The following functions will be used to generate C code for pre & post
functions. *)
@@ -162,7 +173,7 @@ class visit_adding_code_for_synchronisation =
vi_pre.vname <- Data_for_aorai.get_fresh (vi_pre.vname ^ "_pre_func");
vi_pre.vdefined <- true;
vi_pre.vghost <- true;
- Cil_datatype.Varinfo.Hashtbl.add func_orig_table vi_pre (Pre_func kf);
+ Aux_funcs.(add vi_pre (Pre kf));
(* TODO:
- what about protos that have no specified args
(NB: cannot be identified here because of implem of Kernel_function).
@@ -185,7 +196,7 @@ class visit_adding_code_for_synchronisation =
(TFun(voidType,Some arg,false,[]))
in
Kernel_function.Hashtbl.add aux_post_table kf vi_post;
- Cil_datatype.Varinfo.Hashtbl.add func_orig_table vi_post (Post_func kf);
+ Aux_funcs.(add vi_post (Post kf));
let fun_dec_pre = Cil.emptyFunctionFromVI vi_pre in
let fun_dec_post = Cil.emptyFunctionFromVI vi_post in
(* For a future analysis of function arguments,
@@ -224,7 +235,7 @@ class visit_adding_code_for_synchronisation =
GFunDecl(Cil.empty_funspec(),x,loc) :: acc) aux_funcs
[ GFun(fun_dec_pre,loc); GFun(fun_dec_post,loc)]
in
- Cil_datatype.Varinfo.Set.iter (add_aux_bhv kf) aux_funcs;
+ Cil_datatype.Varinfo.Set.iter (Aux_funcs.add_aux kf) aux_funcs;
fundec.sbody.bstmts <-
Cil.mkStmtOneInstr ~ghost:true
(Call(None,Cil.evar ~loc vi_pre,
@@ -280,6 +291,7 @@ class visit_adding_code_for_synchronisation =
end
+
(*********************************************************************)
@@ -920,9 +932,9 @@ class visit_adding_pre_post_from_buch treatloops =
let vi = Kernel_function.get_vi my_kf in
let spec = Annotations.funspec my_kf in
let loc = Kernel_function.get_location my_kf in
- (match kind_of_func vi with
- | Pre_func _ | Post_func _ | Aux_func _ -> ()
- | Not_auto_func -> (* Normal C function *)
+ (match Aux_funcs.kind vi with
+ | Aux_funcs.Pre _ | Post _ | Aux _ -> ()
+ | Not_aux_func -> (* Normal C function *)
let bhvs = mk_post my_kf in
let my_state = Data_for_aorai.get_kf_init_state my_kf in
let requires = needs_zero_one_choice my_state in
@@ -953,8 +965,8 @@ class visit_adding_pre_post_from_buch treatloops =
(* don't use get_spec, as we'd generate default assigns,
while we'll fill the spec just below. *)
let vi = Kernel_function.get_vi my_kf in
- (match kind_of_func vi with
- | Pre_func kf ->
+ (match Aux_funcs.kind vi with
+ | Aux_funcs.Pre kf ->
(* must advance the automaton according to current call. *)
let bhvs = mk_pre_fct_spec kf in
let vis = new change_formals kf my_kf in
@@ -963,7 +975,7 @@ class visit_adding_pre_post_from_buch treatloops =
in
Annotations.add_behaviors Aorai_option.emitter my_kf bhvs;
SkipChildren
- | Post_func kf ->
+ | Post kf ->
(* must advance the automaton according to return event. *)
let (rt, _, _, _) =
Cil.splitFunctionTypeVI (Kernel_function.get_vi kf)
@@ -983,7 +995,7 @@ class visit_adding_pre_post_from_buch treatloops =
in
Annotations.add_behaviors Aorai_option.emitter my_kf bhvs;
SkipChildren
- | Aux_func _ | Not_auto_func ->
+ | Aux _ | Not_aux_func ->
DoChildren (* they are not considered here. *))
| _ -> DoChildren;
diff --git a/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle b/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
index 265c294b60c1352009e8cf0edac82d1896ccfa55..e06220b829a21490d9e731597629a8af15419041 100644
--- a/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
@@ -72,6 +72,7 @@ int rr = 1;
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opa;
accept_S2_tmp = accept_S2;
@@ -145,6 +146,7 @@ int rr = 1;
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opa;
accept_S2_tmp = accept_S2;
@@ -241,6 +243,7 @@ void opa(void)
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opb;
accept_S2_tmp = accept_S2;
@@ -314,6 +317,7 @@ void opa(void)
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opb;
accept_S2_tmp = accept_S2;
@@ -398,6 +402,7 @@ void opb(void)
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opc;
accept_S2_tmp = accept_S2;
@@ -463,6 +468,7 @@ void opb(void)
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opc;
accept_S2_tmp = accept_S2;
@@ -567,6 +573,7 @@ void opc(void)
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
accept_S2_tmp = accept_S2;
@@ -640,6 +647,7 @@ void opc(void)
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
accept_S2_tmp = accept_S2;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
index 844192381021eed94fa7c2989f7b24ba1f12aa01..7504f14db91b1210fc241a88b6d3aef23383d3d8 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
@@ -47,6 +47,7 @@ extern int call_to_an_undefined_function(void);
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_a;
T0_S2_tmp = T0_S2;
@@ -90,6 +91,7 @@ extern int call_to_an_undefined_function(void);
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_a;
T0_S2_tmp = T0_S2;
@@ -151,6 +153,7 @@ int a(void)
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_b;
T0_S2_tmp = T0_S2;
@@ -193,6 +196,7 @@ int a(void)
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_b;
T0_S2_tmp = T0_S2;
@@ -255,6 +259,7 @@ int b(void)
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
T0_S2_tmp = T0_S2;
@@ -297,6 +302,7 @@ int b(void)
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
T0_S2_tmp = T0_S2;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
index d48aaf2d91ec30b8856d568c26a89d02de957748..810cc3f996f1b162ac7c9e9a6b1f0d509853d2f1 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
@@ -60,6 +60,7 @@ int status = 0;
int accept_S3_tmp;
int accept_S4_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_commit_trans;
accept_S1_tmp = accept_S1;
@@ -118,6 +119,7 @@ int status = 0;
int accept_S3_tmp;
int accept_S4_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_commit_trans;
accept_S1_tmp = accept_S1;
@@ -199,6 +201,7 @@ int commit_trans(void)
int accept_S3_tmp;
int accept_S4_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_init_trans;
accept_S1_tmp = accept_S1;
@@ -263,6 +266,7 @@ int commit_trans(void)
int accept_S3_tmp;
int accept_S4_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_init_trans;
accept_S1_tmp = accept_S1;
@@ -349,6 +353,7 @@ int init_trans(void)
int accept_S3_tmp;
int accept_S4_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
accept_S1_tmp = accept_S1;
@@ -417,6 +422,7 @@ int init_trans(void)
int accept_S3_tmp;
int accept_S4_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
accept_S1_tmp = accept_S1;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
index 8491e8c23edf107114bbcc7deeb208bca688e321..bf069fb7cfce5612379c5a2c80540bb07db94e31 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
@@ -63,6 +63,7 @@ int rr = 1;
int accept_S4_tmp;
int accept_S5_tmp;
int accept_all_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opa;
T0_S2_tmp = T0_S2;
@@ -133,6 +134,7 @@ int rr = 1;
int accept_S4_tmp;
int accept_S5_tmp;
int accept_all_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opa;
T0_S2_tmp = T0_S2;
@@ -223,6 +225,7 @@ void opa(void)
int accept_S4_tmp;
int accept_S5_tmp;
int accept_all_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opb;
T0_S2_tmp = T0_S2;
@@ -288,6 +291,7 @@ void opa(void)
int accept_S4_tmp;
int accept_S5_tmp;
int accept_all_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opb;
T0_S2_tmp = T0_S2;
@@ -371,6 +375,7 @@ void opb(void)
int accept_S4_tmp;
int accept_S5_tmp;
int accept_all_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
T0_S2_tmp = T0_S2;
@@ -436,6 +441,7 @@ void opb(void)
int accept_S4_tmp;
int accept_S5_tmp;
int accept_all_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
T0_S2_tmp = T0_S2;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
index 4521080b3e1763859975e8f0d81762316305d61c..bbf09f7914af37ccd19f0eeb02e56ce59f3853e2 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
@@ -63,6 +63,7 @@ int rr = 1;
int T1_S2_tmp;
int accept_S3_tmp;
int accept_all_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opa;
T0_S4_tmp = T0_S4;
@@ -126,6 +127,7 @@ int rr = 1;
int T1_S2_tmp;
int accept_S3_tmp;
int accept_all_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opa;
T0_S4_tmp = T0_S4;
@@ -228,6 +230,7 @@ void opa(void)
int T1_S2_tmp;
int accept_S3_tmp;
int accept_all_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opb;
T0_S4_tmp = T0_S4;
@@ -286,6 +289,7 @@ void opa(void)
int T1_S2_tmp;
int accept_S3_tmp;
int accept_all_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opb;
T0_S4_tmp = T0_S4;
@@ -363,6 +367,7 @@ void opb(void)
int T1_S2_tmp;
int accept_S3_tmp;
int accept_all_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
T0_S4_tmp = T0_S4;
@@ -426,6 +431,7 @@ void opb(void)
int T1_S2_tmp;
int accept_S3_tmp;
int accept_all_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
T0_S4_tmp = T0_S4;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
index c1aac176071c4e4f44da6263665a845b67f6eb08..d434d1ddf705c3dbd33831dba0827d3c4a8ba00c 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
@@ -42,6 +42,7 @@ enum aorai_OpStatusList {
int accept_S1_tmp;
int accept_S2_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_decode_int;
accept_S1_tmp = accept_S1;
@@ -89,6 +90,7 @@ enum aorai_OpStatusList {
int accept_S1_tmp;
int accept_S2_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_decode_int;
accept_S1_tmp = accept_S1;
@@ -211,6 +213,7 @@ int decode_int(char *s)
int accept_S1_tmp;
int accept_S2_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_factorial;
accept_S1_tmp = accept_S1;
@@ -259,6 +262,7 @@ int decode_int(char *s)
int accept_S1_tmp;
int accept_S2_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_factorial;
accept_S1_tmp = accept_S1;
@@ -330,6 +334,7 @@ int factorial(int value)
int accept_S1_tmp;
int accept_S2_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
accept_S1_tmp = accept_S1;
@@ -377,6 +382,7 @@ int factorial(int value)
int accept_S1_tmp;
int accept_S2_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
accept_S1_tmp = accept_S1;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
index eaaac90fdb2269338410ce6fac7a19c5f87a50cf..28c0b50dbab69fcc8cd831e6791f43ace8439798 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
@@ -76,6 +76,7 @@ predicate valid_string{L}(char *s) =
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_countOne;
T0_S2_tmp = T0_S2;
@@ -118,6 +119,7 @@ predicate valid_string{L}(char *s) =
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_countOne;
T0_S2_tmp = T0_S2;
@@ -189,6 +191,7 @@ int countOne(char *argv)
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_count;
T0_S2_tmp = T0_S2;
@@ -231,6 +234,7 @@ int countOne(char *argv)
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_count;
T0_S2_tmp = T0_S2;
@@ -296,6 +300,7 @@ int count(int argc, char **argv)
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
T0_S2_tmp = T0_S2;
@@ -343,6 +348,7 @@ int count(int argc, char **argv)
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
T0_S2_tmp = T0_S2;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
index eb681fba1c9bb4c765e3b1b3b0c173541738b297..0c38acfaa75591b7f30ff5ef1c54ebe2446995e6 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
@@ -97,6 +97,7 @@ int global_argc = 0;
int T0_init_tmp;
int T1_tmp;
int accept_T2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_count;
S1_tmp = S1;
@@ -146,6 +147,7 @@ int global_argc = 0;
int T0_init_tmp;
int T1_tmp;
int accept_T2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_count;
S1_tmp = S1;
@@ -223,6 +225,7 @@ int count(char *argv)
int T0_init_tmp;
int T1_tmp;
int accept_T2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_sumOne;
S1_tmp = S1;
@@ -272,6 +275,7 @@ int count(char *argv)
int T0_init_tmp;
int T1_tmp;
int accept_T2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_sumOne;
S1_tmp = S1;
@@ -355,6 +359,7 @@ int sumOne(char *t, int length)
int T0_init_tmp;
int T1_tmp;
int accept_T2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S1_tmp = S1;
@@ -409,6 +414,7 @@ int sumOne(char *t, int length)
int T0_init_tmp;
int T1_tmp;
int accept_T2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S1_tmp = S1;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
index e92778bcb0cee2799033715b02f935ecf75e8d43..97d6decf1f8df3d0daf2acb49b6edd6e7cb53558 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
@@ -97,6 +97,7 @@ int global_argc = 0;
int T0_init_tmp;
int T1_tmp;
int accept_T2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_count;
S1_tmp = S1;
@@ -146,6 +147,7 @@ int global_argc = 0;
int T0_init_tmp;
int T1_tmp;
int accept_T2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_count;
S1_tmp = S1;
@@ -223,6 +225,7 @@ int count(char *argv)
int T0_init_tmp;
int T1_tmp;
int accept_T2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_sumOne;
S1_tmp = S1;
@@ -272,6 +275,7 @@ int count(char *argv)
int T0_init_tmp;
int T1_tmp;
int accept_T2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_sumOne;
S1_tmp = S1;
@@ -355,6 +359,7 @@ int sumOne(char *t, int length)
int T0_init_tmp;
int T1_tmp;
int accept_T2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S1_tmp = S1;
@@ -409,6 +414,7 @@ int sumOne(char *t, int length)
int T0_init_tmp;
int T1_tmp;
int accept_T2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S1_tmp = S1;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
index 41a59d023f0609c5b9faf6659d71d5a8afe5b8de..b3c85addc01c55afdd11746420fba2f62361f199 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
@@ -74,6 +74,7 @@ int rr = 1;
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opa;
accept_S2_tmp = accept_S2;
@@ -147,6 +148,7 @@ int rr = 1;
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opa;
accept_S2_tmp = accept_S2;
@@ -243,6 +245,7 @@ void opa(void)
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opb;
accept_S2_tmp = accept_S2;
@@ -316,6 +319,7 @@ void opa(void)
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opb;
accept_S2_tmp = accept_S2;
@@ -400,6 +404,7 @@ void opb(void)
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opc;
accept_S2_tmp = accept_S2;
@@ -465,6 +470,7 @@ void opb(void)
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opc;
accept_S2_tmp = accept_S2;
@@ -569,6 +575,7 @@ void opc(void)
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
accept_S2_tmp = accept_S2;
@@ -642,6 +649,7 @@ void opc(void)
int accept_S6_tmp;
int accept_all_tmp;
int accept_init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
accept_S2_tmp = accept_S2;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
index 4ed3b4a39a1a4b99f1c6cbe87ff005554824fd37..4d74ec69aeb2cae08b4b990cf52e83e37258604c 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
@@ -49,6 +49,7 @@ enum aorai_OpStatusList {
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_countOne;
T0_S2_tmp = T0_S2;
@@ -99,6 +100,7 @@ enum aorai_OpStatusList {
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_countOne;
T0_S2_tmp = T0_S2;
@@ -180,6 +182,7 @@ int countOne(char *argv)
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_count;
T0_S2_tmp = T0_S2;
@@ -241,6 +244,7 @@ int countOne(char *argv)
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_count;
T0_S2_tmp = T0_S2;
@@ -329,6 +333,7 @@ int count(int argc, char **argv)
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
T0_S2_tmp = T0_S2;
@@ -384,6 +389,7 @@ int count(int argc, char **argv)
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
T0_S2_tmp = T0_S2;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle
index 62566d6ad713caa507dc98dff28f8670a270d0bc..96b9dc90c1e354c849080815cb015ba467bb2397 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle
@@ -44,6 +44,7 @@ enum aorai_OpStatusList {
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_countOne;
T0_S2_tmp = T0_S2;
@@ -81,6 +82,7 @@ enum aorai_OpStatusList {
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_countOne;
T0_S2_tmp = T0_S2;
@@ -149,6 +151,7 @@ int countOne(char *argv)
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_count;
T0_S2_tmp = T0_S2;
@@ -191,6 +194,7 @@ int countOne(char *argv)
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_count;
T0_S2_tmp = T0_S2;
@@ -258,6 +262,7 @@ int count(int argc, char **argv)
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
T0_S2_tmp = T0_S2;
@@ -305,6 +310,7 @@ int count(int argc, char **argv)
int T0_S2_tmp;
int T0_init_tmp;
int accept_S1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
T0_S2_tmp = T0_S2;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
index 88b0352589bb165941afa451c1e9a37bfc82e997..23495bc09b5a1c69662a183e5eb5fddcecc16787 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
@@ -49,6 +49,7 @@ enum aorai_OpStatusList {
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_countOne;
T0_S2_tmp = T0_S2;
@@ -99,6 +100,7 @@ enum aorai_OpStatusList {
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_countOne;
T0_S2_tmp = T0_S2;
@@ -178,6 +180,7 @@ int countOne(char *argv)
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_count;
T0_S2_tmp = T0_S2;
@@ -239,6 +242,7 @@ int countOne(char *argv)
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_count;
T0_S2_tmp = T0_S2;
@@ -327,6 +331,7 @@ int count(int argc, char **argv)
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
T0_S2_tmp = T0_S2;
@@ -382,6 +387,7 @@ int count(int argc, char **argv)
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
T0_S2_tmp = T0_S2;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
index 9e0438a0e71a1f5807dfbede85a61cfd25b58cf9..1c04d032f84346569b3c9b803fdc19c3048314f3 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
@@ -49,6 +49,7 @@ enum aorai_OpStatusList {
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_countOne;
T0_S2_tmp = T0_S2;
@@ -99,6 +100,7 @@ enum aorai_OpStatusList {
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_countOne;
T0_S2_tmp = T0_S2;
@@ -185,6 +187,7 @@ int countOne(char *argv)
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_count;
T0_S2_tmp = T0_S2;
@@ -246,6 +249,7 @@ int countOne(char *argv)
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_count;
T0_S2_tmp = T0_S2;
@@ -334,6 +338,7 @@ int count(int argc, char **argv)
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
T0_S2_tmp = T0_S2;
@@ -389,6 +394,7 @@ int count(int argc, char **argv)
int T0_init_tmp;
int accept_S1_tmp;
int accept_S2_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
T0_S2_tmp = T0_S2;
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
index 0cf6aa042e89216a12267f75a00f12f7900d45ec..2d27926df0c01f67d7cd6e6aab08effa8a00c3af 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
@@ -4,5 +4,5 @@
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_boucle_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:85: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:86: Warning:
Neither code nor specification for function call_to_an_undefined_function, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
index f4acc0402458f1f853e851fdc62267159d610c1c..8c31757f7be947f639da13da388b5d61d1d18e71 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
@@ -53,6 +53,7 @@ int X;
int S_in_f_tmp;
int Sf_tmp;
int in_main_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
S1_tmp = S1;
@@ -110,6 +111,7 @@ int X;
int S_in_f_tmp;
int Sf_tmp;
int in_main_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
S1_tmp = S1;
@@ -182,6 +184,7 @@ void f(void)
int S_in_f_tmp;
int Sf_tmp;
int in_main_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S1_tmp = S1;
@@ -239,6 +242,7 @@ void f(void)
int S_in_f_tmp;
int Sf_tmp;
int in_main_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S1_tmp = S1;
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 28be1b6491e4d556fdcbc99882eb5dae9fb753cc..cdb19dd27629019910814cbdfed089f7feadc3ee 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
@@ -60,6 +60,7 @@ int X;
@/
void f_pre_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if (3 == aorai_CurStates) aorai_CurStates = S_in_f;
@@ -96,6 +97,7 @@ int X;
@/
void f_post_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if (2 == aorai_CurStates) aorai_CurStates = in_main;
@@ -145,6 +147,7 @@ void f(void)
@/
void main_pre_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if (0 == aorai_CurStates) aorai_CurStates = Sf;
@@ -181,6 +184,7 @@ void f(void)
@/
void main_post_func(int res)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if (4 == aorai_CurStates) aorai_CurStates = S2;
diff --git a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
index ded70303a39942fd04bed926f5cfb44b400fb576..d694fc99a038a4c55017d6a0dc095bbab7196059 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
@@ -26,6 +26,7 @@ enum aorai_OpStatusList {
void a_pre_func(void)
{
int S_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_a;
S_tmp = S;
@@ -48,6 +49,7 @@ enum aorai_OpStatusList {
void a_post_func(void)
{
int S_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_a;
S_tmp = S;
@@ -81,6 +83,7 @@ void a(void)
void main_pre_func(void)
{
int S_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S_tmp = S;
@@ -103,6 +106,7 @@ void a(void)
void main_post_func(void)
{
int S_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S_tmp = S;
diff --git a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
index c7ab7fc71c40604749775aee8ffd3063ab29279e..3c96ba015886f3598f2289bba6a35a46309f64e2 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
@@ -58,6 +58,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_tmp;
int aorai_intermediate_state_0_tmp;
int init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_a;
S_tmp = S;
@@ -123,6 +124,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_tmp;
int aorai_intermediate_state_0_tmp;
int init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_a;
S_tmp = S;
@@ -219,6 +221,7 @@ void a(void)
int aorai_intermediate_state_tmp;
int aorai_intermediate_state_0_tmp;
int init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S_tmp = S;
@@ -277,6 +280,7 @@ void a(void)
int aorai_intermediate_state_tmp;
int aorai_intermediate_state_0_tmp;
int init_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S_tmp = S;
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 9aac8e4561e2046e3363b3e1986e89443b6ff944..162c17c6430a0c7f9ed5cc669a949fd117ba2452 100644
--- a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
@@ -61,6 +61,7 @@ check lemma I_deterministic_trans{L}:
@/
void main_pre_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if (0 == aorai_CurStates) aorai_CurStates = I;
@@ -85,6 +86,7 @@ check lemma I_deterministic_trans{L}:
@/
void main_post_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if (0 == aorai_CurStates) aorai_CurStates = I;
diff --git a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
index eac5b5331dea0f341ab284906042b6468f412140..7d3f5aa88777d3c1fac64715ff6ac126db4cb1b5 100644
--- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
@@ -105,6 +105,7 @@ check lemma S0_deterministic_trans{L}:
@/
void g_pre_func(int x)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
if (3 == aorai_CurStates && x == 4) aorai_CurStates = S4;
@@ -157,6 +158,7 @@ check lemma S0_deterministic_trans{L}:
@/
void g_post_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
if (5 == aorai_CurStates) aorai_CurStates = S1;
@@ -224,6 +226,7 @@ void g(int x)
@/
void f_pre_func(int x)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if (1 == aorai_CurStates && x == 4) aorai_CurStates = S3;
@@ -270,6 +273,7 @@ void g(int x)
@/
void f_post_func(int res)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if (1 == aorai_CurStates && (res == 0 && X == 5)) aorai_CurStates = S2;
@@ -341,6 +345,7 @@ int f(int x)
@/
void real_main_pre_func(int c)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_real_main;
if (0 == aorai_CurStates && c != 0) aorai_CurStates = S1;
@@ -388,6 +393,7 @@ int f(int x)
@/
void real_main_post_func(int res)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_real_main;
if (2 == aorai_CurStates) aorai_CurStates = Sf;
@@ -449,6 +455,7 @@ int real_main(int c)
@/
void main_pre_func(int c)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if (7 == aorai_CurStates) aorai_CurStates = S0;
@@ -494,6 +501,7 @@ int real_main(int c)
@/
void main_post_func(int res)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if (6 == aorai_CurStates) aorai_CurStates = Sf;
diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
index 1b5982df2b99caeb671563defdd0c978475437ac..cbe2ba005bef80cd8401bcc3d5b36f696d3281b7 100644
--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -130,6 +130,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
@/
void f_pre_func(int x)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if (7 == aorai_CurStates && x == 1) {
@@ -211,6 +212,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
@/
void f_post_func(int res)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if (4 == aorai_CurStates && aorai_x_0 == 3) aorai_CurStates = OK;
@@ -343,6 +345,7 @@ int f(int x)
@/
void g_pre_func(int y)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
if (0 == aorai_CurStates) aorai_CurStates = OK;
@@ -415,6 +418,7 @@ int f(int x)
@/
void g_post_func(int res)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
if (3 == aorai_CurStates && aorai_y == 2) aorai_CurStates = OK;
@@ -502,6 +506,7 @@ int g(int y)
@/
void main_pre_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if (6 == aorai_CurStates) aorai_CurStates = main_0;
@@ -552,6 +557,7 @@ int g(int y)
@/
void main_post_func(int res)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if (0 == aorai_CurStates) aorai_CurStates = OK;
diff --git a/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
index a409f76aa7ac5194420e1825744755a472e97f68..818442d76187088f2978e417638c446b9864c827 100644
--- a/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
@@ -29,6 +29,7 @@ enum aorai_OpStatusList {
void main_pre_func(void)
{
int S_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S_tmp = S;
@@ -56,6 +57,7 @@ enum aorai_OpStatusList {
void main_post_func(void)
{
int S_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S_tmp = S;
diff --git a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
index b8271b7f3704cc26e61134cc57f31bb16d75406e..6095d7964e2c4d7526faf4862ec8ac8bfd787e35 100644
--- a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
@@ -71,6 +71,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_reject_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -153,6 +154,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_reject_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -303,6 +305,7 @@ int main_bhv_bhv(int c); */
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_reject_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S0_tmp = S0;
@@ -397,6 +400,7 @@ int main_bhv_bhv(int c); */
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_reject_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S0_tmp = S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
index bcd7dddbbf40385d8d4339e4dc6f5f884bf631d4..21a5cd9feb5329782519856617e4e888d6221448 100644
--- a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
@@ -33,6 +33,7 @@ int f(void);
@/
void main_pre_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
return;
@@ -51,6 +52,7 @@ int f(void);
@/
void main_post_func(int res)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
return;
diff --git a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
index 926ceb3efd81f583b13bdb57410e2dc8a350816c..14b24d45cddfb0f1d2d147e149127967c148440c 100644
--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -84,6 +84,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -164,6 +165,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -274,6 +276,7 @@ void f(void)
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
S0_tmp = S0;
@@ -351,6 +354,7 @@ void f(void)
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
S0_tmp = S0;
@@ -447,6 +451,7 @@ void g(void)
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S0_tmp = S0;
@@ -525,6 +530,7 @@ void g(void)
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S0_tmp = S0;
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 f9cbea2f85d0a3e5d8f936783cce082dded8059d..e753f6649c43947b761c5fa9a1eff8975e595692 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -109,6 +109,7 @@ check lemma e_deterministic_trans{L}:
@/
void f_pre_func(int x)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if (1 == aorai_CurStates) {
@@ -161,6 +162,7 @@ check lemma e_deterministic_trans{L}:
@/
void f_post_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if (2 == aorai_CurStates) aorai_CurStates = e;
@@ -227,6 +229,7 @@ void f(int x)
@/
void g_pre_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
if (1 == aorai_CurStates) aorai_CurStates = d;
@@ -275,6 +278,7 @@ void f(int x)
@/
void g_post_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
if (3 == aorai_CurStates) aorai_CurStates = g_0;
@@ -336,6 +340,7 @@ void g(void)
@/
void h_pre_func(int x)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_h;
if (4 == aorai_CurStates && aorai_x > 0) aorai_CurStates = f_0;
@@ -384,6 +389,7 @@ void g(void)
@/
void h_post_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_h;
if (5 == aorai_CurStates) aorai_CurStates = g_0;
@@ -445,6 +451,7 @@ void h(int x)
@/
void i_pre_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_i;
if (6 == aorai_CurStates) aorai_CurStates = h_0;
@@ -504,6 +511,7 @@ void h(int x)
@/
void i_post_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_i;
if (7 == aorai_CurStates) {
@@ -574,6 +582,7 @@ void i(void)
@/
void main_pre_func(int t)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if (0 == aorai_CurStates) aorai_CurStates = b;
@@ -622,6 +631,7 @@ void i(void)
@/
void main_post_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if (4 == aorai_CurStates) aorai_CurStates = i_0;
diff --git a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
index b0789f55dee4aedb27898df52aca2a53fe61924a..4b5d328fbbea498c667ace7217cc15b157eddb34 100644
--- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
@@ -64,6 +64,7 @@ check lemma Init_deterministic_trans{L}:
@/
void f_pre_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if (2 == aorai_CurStates) aorai_CurStates = aorai_reject;
@@ -96,6 +97,7 @@ check lemma Init_deterministic_trans{L}:
@/
void f_post_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if (2 == aorai_CurStates) aorai_CurStates = aorai_reject;
@@ -139,6 +141,7 @@ void f(void)
@/
void main_pre_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
return;
@@ -163,6 +166,7 @@ void f(void)
@/
void main_post_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
return;
diff --git a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
index e2b8af2f5f8c2edd8827cdbe6b9e0d81c81499ef..a1315a44ec98d6077751b08104bd3115eeb5f930 100644
--- a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
@@ -35,6 +35,7 @@ enum aorai_OpStatusList {
{
int S0_tmp;
int Sf_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -69,6 +70,7 @@ enum aorai_OpStatusList {
{
int S0_tmp;
int Sf_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
S0_tmp = S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/other.res.oracle b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
index 24195e41f5e3f2034d9deeb0369017289bf4f9bf..ea8efc3984f7b9c7adbe61320f4b9b41950efeeb 100644
--- a/src/plugins/aorai/tests/ya/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
@@ -60,6 +60,7 @@ int x = 0;
int init_tmp;
int last_tmp;
int step1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
init_tmp = init;
@@ -123,6 +124,7 @@ int x = 0;
int init_tmp;
int last_tmp;
int step1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
init_tmp = init;
@@ -250,6 +252,7 @@ void f(void)
int init_tmp;
int last_tmp;
int step1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
init_tmp = init;
@@ -313,6 +316,7 @@ void f(void)
int init_tmp;
int last_tmp;
int step1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
init_tmp = init;
@@ -427,6 +431,7 @@ void g(void)
int init_tmp;
int last_tmp;
int step1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
init_tmp = init;
@@ -486,6 +491,7 @@ void g(void)
int init_tmp;
int last_tmp;
int step1_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
init_tmp = init;
diff --git a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
index ad8e58e2c0a5251a4299d62bf2bfc419738d2f6a..8a68e3c289489ec4062c5eaf9d9234965b337bb9 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
@@ -69,6 +69,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -146,6 +147,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -269,6 +271,7 @@ void f(void)
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
S0_tmp = S0;
@@ -350,6 +353,7 @@ void f(void)
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
S0_tmp = S0;
@@ -470,6 +474,7 @@ void g(void)
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S0_tmp = S0;
@@ -548,6 +553,7 @@ void g(void)
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S0_tmp = S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
index 74c4b90d5d2ac7f17973e6170696db87575565e8..241908d1ee501a201e2240ecfb5484099cd40652 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
@@ -84,6 +84,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -164,6 +165,7 @@ enum aorai_OpStatusList {
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
S0_tmp = S0;
@@ -274,6 +276,7 @@ void f(void)
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
S0_tmp = S0;
@@ -351,6 +354,7 @@ void f(void)
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
S0_tmp = S0;
@@ -447,6 +451,7 @@ void g(void)
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S0_tmp = S0;
@@ -525,6 +530,7 @@ void g(void)
int aorai_intermediate_state_1_tmp;
int aorai_intermediate_state_2_tmp;
int aorai_intermediate_state_3_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S0_tmp = S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle b/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
index 8140ad900ee448b23e0d0ab056c90be13f42ebd8..ea9bdd5f8c44f4e60ea26e0cf2d916169aa44109 100644
--- a/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
@@ -40,6 +40,7 @@ enum aorai_OpStatusList {
int S0_tmp;
int Sf_tmp;
int aorai_intermediate_state_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S0_tmp = S0;
@@ -83,6 +84,7 @@ enum aorai_OpStatusList {
int S0_tmp;
int Sf_tmp;
int aorai_intermediate_state_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S0_tmp = S0;
diff --git a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
index 964d18945b278a6d0d8a87aca748535bb645db42..e76ec6fc3ca67bd677079f2888024f1a34b471f0 100644
--- a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
@@ -59,6 +59,7 @@ enum aorai_OpStatusList {
@/
void main_pre_func(int *x, int *y)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if (0 == aorai_CurStates) {
@@ -104,6 +105,7 @@ enum aorai_OpStatusList {
@/
void main_post_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if (1 == aorai_CurStates) {
diff --git a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
index 9ff7ca0aecdd7464bd5a26e5dabe134ca5e47e22..b20f875ba1400ef04b46722a6d248482175a1437 100644
--- a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
@@ -86,6 +86,7 @@ check lemma emptying_stack_deterministic_trans{L}:
@/
void push_pre_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_push;
if (3 == aorai_CurStates) aorai_CurStates = filling_stack;
@@ -133,6 +134,7 @@ check lemma emptying_stack_deterministic_trans{L}:
@/
void push_post_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_push;
if (4 == aorai_CurStates) {
@@ -202,6 +204,7 @@ void push(void)
@/
void pop_pre_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_pop;
if (3 == aorai_CurStates && aorai_n > 0) aorai_CurStates = emptying_stack;
@@ -255,6 +258,7 @@ void push(void)
@/
void pop_post_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_pop;
if (2 == aorai_CurStates && aorai_n == 1) {
@@ -334,6 +338,7 @@ void pop(void)
@/
void main_pre_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if (5 == aorai_CurStates) {
@@ -376,6 +381,7 @@ void pop(void)
@/
void main_post_func(void)
{
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if (1 == aorai_CurStates) aorai_CurStates = accept;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
index 20787049401870e0d034354f17271fc1c4a30eee..960ccd88bee0e98436f8b49004060cdfd70d4e36 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
@@ -64,6 +64,7 @@ int rr = 1;
int S4_tmp;
int SF_tmp;
int mainst_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opa;
S1_tmp = S1;
@@ -129,6 +130,7 @@ int rr = 1;
int S4_tmp;
int SF_tmp;
int mainst_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opa;
S1_tmp = S1;
@@ -216,6 +218,7 @@ void opa(int i, int j)
int S4_tmp;
int SF_tmp;
int mainst_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opb;
S1_tmp = S1;
@@ -282,6 +285,7 @@ void opa(int i, int j)
int S4_tmp;
int SF_tmp;
int mainst_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opb;
S1_tmp = S1;
@@ -367,6 +371,7 @@ int opb(void)
int S4_tmp;
int SF_tmp;
int mainst_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S1_tmp = S1;
@@ -432,6 +437,7 @@ int opb(void)
int S4_tmp;
int SF_tmp;
int mainst_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S1_tmp = S1;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
index c6d27622ae3da9ddb41c15b669517df025313969..0527f8f7b592cc272a2d1b250c1d61c71211b75a 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
@@ -69,6 +69,7 @@ int rr = 1;
int S5_tmp;
int S6_tmp;
int S7_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opa;
S1_tmp = S1;
@@ -142,6 +143,7 @@ int rr = 1;
int S5_tmp;
int S6_tmp;
int S7_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opa;
S1_tmp = S1;
@@ -239,6 +241,7 @@ int opa(int r)
int S5_tmp;
int S6_tmp;
int S7_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opb;
S1_tmp = S1;
@@ -311,6 +314,7 @@ int opa(int r)
int S5_tmp;
int S6_tmp;
int S7_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opb;
S1_tmp = S1;
@@ -398,6 +402,7 @@ void opb(void)
int S5_tmp;
int S6_tmp;
int S7_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_opc;
S1_tmp = S1;
@@ -463,6 +468,7 @@ void opb(void)
int S5_tmp;
int S6_tmp;
int S7_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_opc;
S1_tmp = S1;
@@ -569,6 +575,7 @@ void opc(void)
int S5_tmp;
int S6_tmp;
int S7_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S1_tmp = S1;
@@ -641,6 +648,7 @@ void opc(void)
int S5_tmp;
int S6_tmp;
int S7_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S1_tmp = S1;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
index 6bb7bed4d3159b60efac15e5c8cdd6eadf1c409c..3e9c2f9103d143b98528450a2e512548da46841e 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
@@ -45,6 +45,7 @@ enum aorai_OpStatusList {
int End_tmp;
int Idle_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_isPresent;
End_tmp = End;
@@ -92,6 +93,7 @@ enum aorai_OpStatusList {
int End_tmp;
int Idle_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_isPresent;
End_tmp = End;
@@ -189,6 +191,7 @@ int isPresent(int *t, int max, int val)
int End_tmp;
int Idle_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_foo;
End_tmp = End;
@@ -230,6 +233,7 @@ int isPresent(int *t, int max, int val)
int End_tmp;
int Idle_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_foo;
End_tmp = End;
@@ -284,6 +288,7 @@ void foo(void)
int End_tmp;
int Idle_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
End_tmp = End;
@@ -325,6 +330,7 @@ void foo(void)
int End_tmp;
int Idle_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
End_tmp = End;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
index ef459e69225d1cf2833865df30d46ea4dc7b7aed..70c686c2f89ed0d6e6a7211bb6a348fd81cae358 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
@@ -41,6 +41,7 @@ enum aorai_OpStatusList {
int S1_tmp;
int S2_tmp;
int main_0_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_decode_int;
S1_tmp = S1;
@@ -87,6 +88,7 @@ enum aorai_OpStatusList {
int S1_tmp;
int S2_tmp;
int main_0_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_decode_int;
S1_tmp = S1;
@@ -208,6 +210,7 @@ int decode_int(char *s)
int S1_tmp;
int S2_tmp;
int main_0_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_factorial;
S1_tmp = S1;
@@ -254,6 +257,7 @@ int decode_int(char *s)
int S1_tmp;
int S2_tmp;
int main_0_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_factorial;
S1_tmp = S1;
@@ -322,6 +326,7 @@ int factorial(int value)
int S1_tmp;
int S2_tmp;
int main_0_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S1_tmp = S1;
@@ -368,6 +373,7 @@ int factorial(int value)
int S1_tmp;
int S2_tmp;
int main_0_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S1_tmp = S1;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
index 9ff8daac4d006c4b2c7654824e4778e6d8869700..968521d3ad2ecef832776490a9f78c5345c5543d 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
@@ -42,6 +42,7 @@ enum aorai_OpStatusList {
int End_tmp;
int Idle_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_isPresent;
End_tmp = End;
@@ -95,6 +96,7 @@ enum aorai_OpStatusList {
int End_tmp;
int Idle_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_isPresent;
End_tmp = End;
@@ -185,6 +187,7 @@ int isPresent(int *t, int size, int val)
int End_tmp;
int Idle_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_foo;
End_tmp = End;
@@ -226,6 +229,7 @@ int isPresent(int *t, int size, int val)
int End_tmp;
int Idle_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_foo;
End_tmp = End;
@@ -280,6 +284,7 @@ void foo(void)
int End_tmp;
int Idle_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
End_tmp = End;
@@ -321,6 +326,7 @@ void foo(void)
int End_tmp;
int Idle_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
End_tmp = End;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
index 6510597aa4dbf5cca3ffa2ace04e3c9d207deedc..1a84302afcdb9689c16739c356a1c26601259dee 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
@@ -53,6 +53,7 @@ enum aorai_OpStatusList {
int Idle_tmp;
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_isPresentRec;
End_tmp = End;
@@ -117,6 +118,7 @@ enum aorai_OpStatusList {
int Idle_tmp;
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_isPresentRec;
End_tmp = End;
@@ -215,6 +217,7 @@ int isPresentRec(int *t, int i, int max, int val)
int Idle_tmp;
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_isPresent;
End_tmp = End;
@@ -272,6 +275,7 @@ int isPresentRec(int *t, int i, int max, int val)
int Idle_tmp;
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_isPresent;
End_tmp = End;
@@ -352,6 +356,7 @@ int isPresent(int *t, int max, int val)
int Idle_tmp;
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_foo;
End_tmp = End;
@@ -402,6 +407,7 @@ int isPresent(int *t, int max, int val)
int Idle_tmp;
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_foo;
End_tmp = End;
@@ -466,6 +472,7 @@ void foo(void)
int Idle_tmp;
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
End_tmp = End;
@@ -516,6 +523,7 @@ void foo(void)
int Idle_tmp;
int IgnoreFoo_tmp;
int WillDoFoo_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
End_tmp = End;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
index b73119bb7007bd98d2ff9ae0121f38547cd3bfdf..e0b06bd1c0f3829ba53195545620d8f0f478680d 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
@@ -42,6 +42,7 @@ int myAge = 0;
{
int S1_tmp;
int main_0_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_increment;
S1_tmp = S1;
@@ -77,6 +78,7 @@ int myAge = 0;
{
int S1_tmp;
int main_0_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_increment;
S1_tmp = S1;
@@ -129,6 +131,7 @@ void increment(void)
{
int S1_tmp;
int main_0_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S1_tmp = S1;
@@ -164,6 +167,7 @@ void increment(void)
{
int S1_tmp;
int main_0_tmp;
+ /@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S1_tmp = S1;
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 e5437b11cf441f0122b9d89b3ba1147984506890..16d8f0409c53ff0280dd7978f240fe94cc7edda0 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:62: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0.i:63: Warning:
Neither code nor specification for function f, generating default assigns from the prototype