From e00de35e282943bf3fd8b07f23daa21f72281390 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 18 Dec 2018 16:08:32 +0100
Subject: [PATCH] [Aorai] Generate slevel annotations
- Isolate all auxiliary functions registring/finding/iterating
operations in their own module
---
.../aorai/aorai_eva_analysis.enabled.ml | 16 ++++-
src/plugins/aorai/aorai_visitors.ml | 72 +++++++++++--------
.../aorai/tests/ltl/oracle/goto.res.oracle | 8 +++
.../tests/ltl/oracle/test_boucle.res.oracle | 6 ++
.../tests/ltl/oracle/test_boucle1.res.oracle | 6 ++
.../tests/ltl/oracle/test_boucle2.res.oracle | 6 ++
.../tests/ltl/oracle/test_boucle3.res.oracle | 6 ++
.../ltl/oracle/test_factorial.res.oracle | 6 ++
.../ltl/oracle/test_recursion1.res.oracle | 6 ++
.../ltl/oracle/test_recursion2.0.res.oracle | 6 ++
.../ltl/oracle/test_recursion2.1.res.oracle | 6 ++
.../tests/ltl/oracle/test_switch2.res.oracle | 8 +++
.../tests/ltl/oracle/test_switch3.res.oracle | 6 ++
.../test_switch3_et_recursion.res.oracle | 6 ++
.../ltl/oracle/test_switch3_if.res.oracle | 6 ++
.../ltl/oracle/test_switch3_return.res.oracle | 6 ++
.../ltl/oracle_prove/test_boucle.res.oracle | 2 +-
.../tests/ya/oracle/assigns.0.res.oracle | 4 ++
.../tests/ya/oracle/assigns.1.res.oracle | 4 ++
.../tests/ya/oracle/bts1289.0.res.oracle | 4 ++
.../tests/ya/oracle/bts1289.1.res.oracle | 4 ++
.../ya/oracle/declared_function.res.oracle | 2 +
.../tests/ya/oracle/deterministic.res.oracle | 8 +++
.../aorai/tests/ya/oracle/formals.res.oracle | 6 ++
.../generate_assigns_bts1290.res.oracle | 2 +
.../tests/ya/oracle/hoare_seq.res.oracle | 4 ++
.../tests/ya/oracle/incorrect.res.oracle | 2 +
.../tests/ya/oracle/loop_bts1050.res.oracle | 6 ++
.../ya/oracle/metavariables-right.res.oracle | 10 +++
.../tests/ya/oracle/monostate.res.oracle | 4 ++
.../aorai/tests/ya/oracle/not_prm.res.oracle | 2 +
.../aorai/tests/ya/oracle/other.res.oracle | 6 ++
.../aorai/tests/ya/oracle/seq.res.oracle | 6 ++
.../aorai/tests/ya/oracle/seq_loop.res.oracle | 6 ++
.../tests/ya/oracle/single_call.res.oracle | 2 +
.../oracle/singleassignment-right.res.oracle | 2 +
.../aorai/tests/ya/oracle/stack.res.oracle | 6 ++
.../ya/oracle/test_acces_params.res.oracle | 6 ++
.../ya/oracle/test_acces_params2.res.oracle | 8 +++
.../test_boucle_rechercheTableau.res.oracle | 6 ++
.../tests/ya/oracle/test_factorial.res.oracle | 6 ++
.../ya/oracle/test_recursion4.res.oracle | 6 ++
.../ya/oracle/test_recursion5.res.oracle | 8 +++
.../tests/ya/oracle/test_struct.res.oracle | 4 ++
.../ya/oracle_prove/incorrect.res.oracle | 2 +-
45 files changed, 281 insertions(+), 33 deletions(-)
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index b17dd3dae1b..85aaa035683 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 d5bbcfd954e..7011f12d520 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 265c294b60c..e06220b829a 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 84419238102..7504f14db91 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 d48aaf2d91e..810cc3f996f 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 8491e8c23ed..bf069fb7cfc 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 4521080b3e1..bbf09f7914a 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 c1aac176071..d434d1ddf70 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 eaaac90fdb2..28c0b50dbab 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 eb681fba1c9..0c38acfaa75 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 e92778bcb0c..97d6decf1f8 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 41a59d023f0..b3c85addc01 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 4ed3b4a39a1..4d74ec69aeb 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 62566d6ad71..96b9dc90c1e 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 88b0352589b..23495bc09b5 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 9e0438a0e71..1c04d032f84 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 0cf6aa042e8..2d27926df0c 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 f4acc040245..8c31757f7be 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 28be1b6491e..cdb19dd2762 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 ded70303a39..d694fc99a03 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 c7ab7fc71c4..3c96ba01588 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 9aac8e4561e..162c17c6430 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 eac5b5331de..7d3f5aa8877 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 1b5982df2b9..cbe2ba005be 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 a409f76aa7a..818442d7618 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 b8271b7f370..6095d7964e2 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 bcd7dddbbf4..21a5cd9feb5 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 926ceb3efd8..14b24d45cdd 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 f9cbea2f85d..e753f6649c4 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 b0789f55dee..4b5d328fbbe 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 e2b8af2f5f8..a1315a44ec9 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 24195e41f5e..ea8efc3984f 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 ad8e58e2c0a..8a68e3c2894 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 74c4b90d5d2..241908d1ee5 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 8140ad900ee..ea9bdd5f8c4 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 964d18945b2..e76ec6fc3ca 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 9ff7ca0aecd..b20f875ba14 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 20787049401..960ccd88bee 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 c6d27622ae3..0527f8f7b59 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 6bb7bed4d31..3e9c2f9103d 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 ef459e69225..70c686c2f89 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 9ff8daac4d0..968521d3ad2 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 6510597aa4d..1a84302afcd 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 b73119bb700..e0b06bd1c0f 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 e5437b11cf4..16d8f0409c5 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
--
GitLab