Skip to content
Snippets Groups Projects
Commit e00de35e authored by Valentin Perrelle's avatar Valentin Perrelle Committed by Virgile Prevosto
Browse files

[Aorai] Generate slevel annotations 

- Isolate all auxiliary functions registring/finding/iterating
  operations in their own module
parent f4e23690
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 158 additions and 32 deletions
src/plugins/aorai/aorai_eva_analysis.enabled.ml
+ 15
− 1
View file @ e00de35e
......@@ -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 ()
src/plugins/aorai/aorai_visitors.ml
+ 42
− 30
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
+ 8
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
+ 6
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
+ 6
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
+ 6
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
+ 6
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
+ 6
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
+ 6
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
+ 6
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
+ 6
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
+ 8
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
+ 6
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle
+ 6
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
+ 6
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
+ 6
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
+ 1
− 1
View file @ e00de35e
......@@ -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
src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
+ 4
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
+ 4
− 0
View file @ e00de35e
......@@ -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;
......
src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
+ 4
− 0
View file @ e00de35e
......@@ -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;
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment