diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 44ef64c7d1d270711e4959275da491627760735a..7fd1b0b683a4ac3977630c865213dce7aefe0bf6 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -453,14 +453,113 @@ and tlval_to_lval (tlhost, toffset) res =
should not see \result. *)
| None -> Aorai_option.fatal "Unexpected \\result")
-(* Translate the cross condition of an automaton edge to an expression.
- Used in mk_stmt. *)
-let crosscond_to_exp curr_f curr_status loc (cond,_) res =
+module Kf_bhv_cache =
+ Datatype.Pair_with_collections(Cil_datatype.Kf)(Datatype.String)
+ (struct let module_name = "Aorai_utils.Kf_bhv_cache" end)
+
+let bhv_aux_functions_table = Kf_bhv_cache.Hashtbl.create 7
+
+let get_bhv_aux_fct kf bhv =
+ match
+ Kf_bhv_cache.Hashtbl.find_opt bhv_aux_functions_table (kf,bhv.b_name)
+ with
+ | Some vi -> vi, false
+ | None ->
+ let loc = Cil_datatype.Location.unknown in
+ let ovi = Kernel_function.get_vi kf in
+ let vi = Cil_const.copy_with_new_vid ovi in
+ vi.vname <- Data_for_aorai.get_fresh (ovi.vname ^ "_bhv_" ^ bhv.b_name);
+ vi.vdefined <- false;
+ vi.vghost <- true;
+ let (_,args,varargs,_) = Cil.splitFunctionTypeVI ovi in
+ let typ = TFun(Cil.intType, args, varargs,[]) in
+ Cil.update_var_type vi typ;
+ Cil.setFormalsDecl vi typ;
+ vi.vattr <- [];
+ let assoc =
+ List.combine (Kernel_function.get_formals kf) (Cil.getFormalsDecl vi)
+ in
+ let vis = object
+ inherit Visitor.frama_c_copy (Project.current())
+ method! vlogic_var_use lv =
+ match lv.lv_origin with
+ | None -> JustCopy
+ | Some vi ->
+ (match
+ List.find_opt (fun (x,_) -> Cil_datatype.Varinfo.equal vi x) assoc
+ with
+ | None -> JustCopy
+ | Some (_,nvi) -> ChangeTo (Cil.cvar_to_lvar nvi))
+ end
+ in
+ let assumes = Visitor.visitFramacPredicates vis bhv.b_assumes in
+ let assumes = List.map Logic_const.refresh_predicate assumes in
+ let assigns = Writes [] in
+ let post_cond =
+ [Normal,
+ Logic_const.(
+ new_predicate
+ (prel (Req,tlogic_coerce (tresult Cil.intType) Linteger,lone())))]
+ in
+ let bhv_in =
+ Cil.mk_behavior ~name:bhv.b_name ~assumes ~assigns ~post_cond ()
+ in
+ let name = bhv.b_name ^ "_out" in
+ let assumes =
+ [ Logic_const.(
+ new_predicate (pnot (pands (List.map pred_of_id_pred assumes))))]
+ in
+ let assigns = Writes [] in
+ let post_cond =
+ [ Normal,
+ Logic_const.(
+ new_predicate
+ (prel
+ (Req, tlogic_coerce (tresult Cil.intType) Linteger, lzero())))]
+ in
+ let bhv_out = Cil.mk_behavior ~name ~assumes ~assigns ~post_cond () in
+ Globals.Functions.replace_by_declaration (Cil.empty_funspec()) vi loc;
+ let my_kf = Globals.Functions.get vi in
+ Annotations.add_behaviors
+ ~register_children:true Aorai_option.emitter my_kf [bhv_in; bhv_out];
+ Annotations.add_assigns
+ ~keep_empty:false Aorai_option.emitter my_kf (Writes []);
+ Annotations.add_complete Aorai_option.emitter my_kf
+ [bhv_in.b_name; bhv_out.b_name];
+ Annotations.add_disjoint Aorai_option.emitter my_kf
+ [bhv_in.b_name; bhv_out.b_name];
+ vi, true
+
+(** create a new abstract function call to decide whether we are in the
+ corresponding behavior or not. *)
+let mk_behavior_call generated_kf kf bhv =
+ let aux,generated = get_bhv_aux_fct kf bhv in
+ let res =
+ Cil.makeLocalVar
+ (Kernel_function.get_definition generated_kf)
+ ~ghost:true ~referenced:true ~insert:false
+ (get_fresh "bhv_aux") Cil.intType
+ in
+ let stmt =
+ Cil.mkStmtOneInstr
+ ~ghost:true
+ ~valid_sid:true
+ (Cil_types.Call (
+ Some (Var res, NoOffset),
+ Cil.evar aux,
+ List.map (fun x -> Cil.evar x) (Kernel_function.get_formals kf),
+ Cil_datatype.Location.unknown))
+ in
+ (res, stmt,
+ if generated then Cil_datatype.Varinfo.Set.singleton aux
+ else Cil_datatype.Varinfo.Set.empty)
+(* Translate the cross condition of an automaton edge to an expression.
+ Used in mk_stmt. This might generate calls to auxiliary functions, to
+ take into account a guard that uses a function behavior. *)
+let crosscond_to_exp generated_kf curr_f curr_status loc (cond,_) res =
let check_current_event f status =
- if Kernel_function.equal curr_f f && curr_status = status then
- Cil.one loc
- else Cil.zero loc
+ Kernel_function.equal curr_f f && curr_status = status
in
let rel_convert = function
| Rlt -> Lt
@@ -473,28 +572,54 @@ let crosscond_to_exp curr_f curr_status loc (cond,_) res =
let rec expnode_convert =
function
| TOr (c1, c2) ->
- let e1 = expnode_convert c1 in
+ let stmts1, vars1, defs1, e1 = expnode_convert c1 in
(match Cil.isInteger e1 with
- | None -> Cil.mkBinOp loc LOr e1 (expnode_convert c2)
+ | None ->
+ let stmts2, vars2, defs2, e2 = expnode_convert c2 in
+ stmts1 @ stmts2, vars1 @ vars2,
+ Cil_datatype.Varinfo.Set.union defs1 defs2,
+ Cil.mkBinOp loc LOr e1 e2
| Some i when Integer.is_zero i -> expnode_convert c2
- | Some _ -> e1)
+ | Some _ -> [], [], Cil_datatype.Varinfo.Set.empty,e1)
| TAnd (c1, c2) ->
- let e1 = expnode_convert c1 in
+ let stmts1, vars1, defs1, e1 = expnode_convert c1 in
(match Cil.isInteger e1 with
- | None -> Cil.mkBinOp loc LAnd e1 (expnode_convert c2)
- | Some i when Integer.is_zero i -> e1
+ | None ->
+ let stmts2, vars2, defs2, e2 = expnode_convert c2 in
+ stmts1 @ stmts2, vars1 @vars2,
+ Cil_datatype.Varinfo.Set.union defs1 defs2,
+ Cil.mkBinOp loc LAnd e1 e2
+ | Some i when Integer.is_zero i ->
+ [], [], Cil_datatype.Varinfo.Set.empty, e1
| Some _ -> expnode_convert c2)
| TNot (c1) ->
- let e1 = expnode_convert c1 in
+ let stmts1, vars1, defs1, e1 = expnode_convert c1 in
(match Cil.isInteger e1 with
- | None -> Cil.new_exp loc (UnOp(LNot, e1,Cil.intType))
- | Some i when Integer.is_zero i -> Cil.one loc
- | Some _ -> Cil.zero loc)
- | TCall (f,_) -> check_current_event f Promelaast.Call
- | TReturn f -> check_current_event f Promelaast.Return
- | TTrue -> (Cil.one loc)
- | TFalse -> (Cil.zero loc)
+ | None ->
+ stmts1, vars1, defs1, Cil.new_exp loc (UnOp(LNot, e1,Cil.intType))
+ | Some i when Integer.is_zero i ->
+ [], [], Cil_datatype.Varinfo.Set.empty, Cil.one loc
+ | Some _ -> [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero loc)
+ | TCall (f,None) ->
+ if check_current_event f Promelaast.Call then
+ [], [], Cil_datatype.Varinfo.Set.empty, Cil.one loc
+ else
+ [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero loc
+ | TCall (f, Some bhv) ->
+ if check_current_event f Promelaast.Call then begin
+ let res, stmt, new_kf = mk_behavior_call generated_kf f bhv in
+ [ stmt ], [res], new_kf, Cil.evar res
+ end else
+ [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero loc
+ | TReturn f ->
+ if check_current_event f Promelaast.Return then
+ [], [], Cil_datatype.Varinfo.Set.empty, Cil.one loc
+ else
+ [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero loc
+ | TTrue -> [], [], Cil_datatype.Varinfo.Set.empty, Cil.one loc
+ | TFalse -> [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero loc
| TRel(rel,t1,t2) ->
+ [], [], Cil_datatype.Varinfo.Set.empty,
Cil.mkBinOp
loc (rel_convert rel) (term_to_exp t1 res) (term_to_exp t2 res)
in
@@ -1782,22 +1907,24 @@ let copy_stmt s =
If state is reachable, generates a "If then else" statement, else it is
just an assignment.
Used in auto_func_block. *)
-let mk_stmt loc (states, tr) f fst status ((st,_) as state) res =
+let mk_stmt generated_kf loc (states, tr) f fst status ((st,_) as state) res =
if is_reachable st status then begin
let useful_trans = get_accessible_transitions (states,tr) st status in
- let exp_from_trans,stmt_from_action =
- List.split
- (List.map
- (function trans ->
- (Cil.mkBinOp
- loc
- LAnd
- (is_state_exp trans.start loc)
- (crosscond_to_exp f fst loc trans.cross res)),
- (act_convert loc trans.cross res)
- )
- useful_trans
- )
+ let aux_stmts, new_vars, new_funcs, exp_from_trans,stmt_from_action =
+ List.fold_right
+ (fun trans
+ (aux_stmts, aux_vars, new_funcs, exp_from_trans, stmt_from_action) ->
+ let (tr_stmts, tr_vars, tr_funcs, exp) =
+ crosscond_to_exp generated_kf f fst loc trans.cross res
+ in
+ (tr_stmts @ aux_stmts,
+ tr_vars @ aux_vars,
+ Cil_datatype.Varinfo.Set.union tr_funcs new_funcs,
+ Cil.mkBinOp loc LAnd (is_state_exp trans.start loc) exp
+ ::exp_from_trans,
+ act_convert loc trans.cross res :: stmt_from_action))
+ useful_trans
+ ([],[],Cil_datatype.Varinfo.Set.empty, [], [])
in
let mkIfStmt exp1 block1 block2 =
Cil.mkStmt ~ghost:true (If (exp1, block1, block2, loc))
@@ -1813,31 +1940,35 @@ let mk_stmt loc (states, tr) f fst status ((st,_) as state) res =
if Aorai_option.Deterministic.get () then []
else [is_out_of_state_stmt state loc]
in
- if Aorai_option.Deterministic.get () then
- List.fold_left2
- (fun acc cond stmt_act ->
- [mkIfStmt cond
- (mkBlock (copy_stmt then_stmt :: stmt_act)) (mkBlock acc)])
- else_stmt
- (List.rev exp_from_trans)
- (List.rev stmt_from_action)
- else
- let actions =
+ let trans_stmts =
+ if Aorai_option.Deterministic.get () then
List.fold_left2
(fun acc cond stmt_act ->
- if stmt_act = [] then acc
- else
- (mkIfStmt cond (mkBlock stmt_act) (mkBlock []))::acc)
- []
+ [mkIfStmt cond
+ (mkBlock (copy_stmt then_stmt :: stmt_act)) (mkBlock acc)])
+ else_stmt
(List.rev exp_from_trans)
(List.rev stmt_from_action)
- in
- mkIfStmt if_cond (mkBlock [then_stmt]) (mkBlock else_stmt) :: actions
+ else
+ let actions =
+ List.fold_left2
+ (fun acc cond stmt_act ->
+ if stmt_act = [] then acc
+ else
+ (mkIfStmt cond (mkBlock stmt_act) (mkBlock []))::acc)
+ []
+ (List.rev exp_from_trans)
+ (List.rev stmt_from_action)
+ in
+ mkIfStmt if_cond (mkBlock [then_stmt]) (mkBlock else_stmt) :: actions
+ in
+ new_funcs, new_vars, aux_stmts @ trans_stmts
end else
- if Aorai_option.Deterministic.get () then []
- else [is_out_of_state_stmt state loc]
+ if Aorai_option.Deterministic.get () then
+ Cil_datatype.Varinfo.Set.empty, [], []
+ else Cil_datatype.Varinfo.Set.empty, [], [is_out_of_state_stmt state loc]
-let auto_func_block loc f st status res =
+let auto_func_block generated_kf loc f st status res =
let dkey = func_body_dkey in
let call_or_ret =
match st with
@@ -1901,15 +2032,21 @@ let auto_func_block loc f st status res =
copies
in
(* For each state, we have to generate the statement that will update its copy. *)
- let main_stmt =
+ let new_funcs, local_var, main_stmt =
List.fold_left
- (fun acc state -> (mk_stmt loc auto f st status state res)@acc )
- []
+ (fun (new_funcs, aux_vars, stmts) state ->
+ let my_funcs, my_vars, my_stmts =
+ mk_stmt generated_kf loc auto f st status state res
+ in
+ Cil_datatype.Varinfo.Set.union my_funcs new_funcs,
+ my_vars @ aux_vars,
+ my_stmts@stmts )
+ (Cil_datatype.Varinfo.Set.empty, local_var, [])
copies
in
-
+
(* Finally, we replace the state var values by the ones computed in copies. *)
let stvar_update =
if Aorai_option.Deterministic.get () then
@@ -1931,7 +2068,7 @@ let auto_func_block loc f st status res =
res_block.blocals <- local_var;
Aorai_option.debug ~dkey "Generated body is:@\n%a"
Printer.pp_block res_block;
- res_block,local_var
+ new_funcs,res_block,local_var
let get_preds_wrt_params_reachable_states state f status =
let auto = Data_for_aorai.getAutomata () in
diff --git a/src/plugins/aorai/aorai_utils.mli b/src/plugins/aorai/aorai_utils.mli
index 7ea1ff1b0a7917185b727521275ab0c720c433d7..ec9bf4837c1d313a0eca64ec4caa36cc1ddbd37a 100644
--- a/src/plugins/aorai/aorai_utils.mli
+++ b/src/plugins/aorai/aorai_utils.mli
@@ -126,16 +126,24 @@ val auto_func_behaviors:
Cil_types.location -> kernel_function -> Promelaast.funcStatus ->
Data_for_aorai.state -> Cil_types.funbehavior list
-(** [auto_func_block loc f status st res]
+(** [auto_func_block current_kf loc f status st res]
generates the body of pre & post functions.
- res must be [None] for a pre-function and [Some v] for a post-func where
+ - [current_kf] is the auxiliary function currently being defined.
+ - [res] must be [None] for a pre-function and [Some v] for a post-func where
[v] is the formal corresponding to the value returned by the original
function. If the original function returns [Void], [res] must be [None].
- It also returns the local variables list declared in the body. *)
+
+ @returns [funcs, block, locals], where
+ - funcs is the set of auxiliary functions that are used to determine
+ whether a particular behavior of original callee is taken
+ - block is the sequence of instructions that perform the transition
+ - locals is the list of local variables.
+*)
val auto_func_block:
+ Kernel_function.t ->
Cil_types.location -> kernel_function -> Promelaast.funcStatus ->
Data_for_aorai.state -> Cil_types.varinfo option ->
- Cil_types.block * Cil_types.varinfo list
+ Cil_datatype.Varinfo.Set.t * Cil_types.block * Cil_types.varinfo list
val get_preds_pre_wrt_params : kernel_function -> predicate
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 2b7c52b53ecfa135f351fee114293ad84e50b706..ba4095ac168cf360822acb156a17720d5b3518b4 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -62,15 +62,21 @@ let get_call_name exp = match exp.enode with
(* the various kinds of auxiliary functions. *)
type func_auto_mode =
- Not_auto_func (* original C 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. *)
+ | 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
@@ -78,19 +84,21 @@ let kind_of_func vi =
(* The following functions will be used to generate C code for pre & post
functions. *)
-let mk_auto_fct_block kf status auto_state res =
+let mk_auto_fct_block kf_aux kf status auto_state res =
let loc = Kernel_function.get_location kf in
- Aorai_utils.auto_func_block loc kf status auto_state res
+ Aorai_utils.auto_func_block kf_aux loc kf status auto_state res
-let mk_pre_fct_block kf =
+let mk_pre_fct_block kf_pre kf =
mk_auto_fct_block
+ kf_pre
kf
Promelaast.Call
(Data_for_aorai.get_kf_init_state kf)
None
-let mk_post_fct_block kf res =
+let mk_post_fct_block kf_post kf res =
mk_auto_fct_block
+ kf_post
kf
Promelaast.Return
(Data_for_aorai.get_kf_return_state kf)
@@ -153,9 +161,16 @@ class visit_adding_code_for_synchronisation =
fun_dec_post (TFun(voidType,Some arg,false,[]));
(* We will now fill the function with the result
of the automaton's analysis. *)
- let pre_block,pre_locals = mk_pre_fct_block kf in
- let post_block,post_locals =
- mk_post_fct_block kf (Extlib.opt_of_list fun_dec_post.sformals)
+ Globals.Functions.replace_by_definition
+ (Cil.empty_funspec()) fun_dec_pre loc;
+ Globals.Functions.replace_by_definition
+ (Cil.empty_funspec()) fun_dec_post loc;
+ let kf_pre = Globals.Functions.get vi_pre in
+ let kf_post = Globals.Functions.get vi_post in
+ let aux_func_pre, pre_block,pre_locals = mk_pre_fct_block kf_pre kf in
+ let aux_func_post, post_block,post_locals =
+ mk_post_fct_block
+ kf_post kf (Extlib.opt_of_list fun_dec_post.sformals)
in
fun_dec_pre.slocals <- pre_locals;
fun_dec_pre.sbody <- pre_block;
@@ -163,7 +178,16 @@ class visit_adding_code_for_synchronisation =
fun_dec_post.slocals <- post_locals;
fun_dec_post.sbody <- post_block;
fun_dec_post.svar.vdefined <- true;
- let globs = [ GFun(fun_dec_pre,loc); GFun(fun_dec_post,loc);] in
+ let aux_funcs =
+ Cil_datatype.Varinfo.Set.union aux_func_pre aux_func_post
+ in
+ let globs =
+ Cil_datatype.Varinfo.Set.fold
+ (fun x acc ->
+ 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;
fundec.sbody.bstmts <-
Cil.mkStmtOneInstr ~ghost:true
(Call(None,Cil.evar ~loc vi_pre,
@@ -171,11 +195,7 @@ class visit_adding_code_for_synchronisation =
(Kernel_function.get_formals kf),
loc))
:: fundec.sbody.bstmts;
- Globals.Functions.replace_by_definition
- (Cil.empty_funspec()) fun_dec_pre loc;
- Globals.Functions.replace_by_definition
- (Cil.empty_funspec()) fun_dec_post loc;
- (* Finally, we update the CFG for the new fundec *)
+ (* Finally, we update the CFG for the new fundec *)
let keepSwitch = Kernel.KeepSwitch.get() in
Cfg.prepareCFG ~keepSwitch fun_dec_pre;
Cfg.cfgFun fun_dec_pre;
@@ -891,7 +911,7 @@ class visit_adding_pre_post_from_buch treatloops =
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 _ -> ()
+ | Pre_func _ | Post_func _ | Aux_func _ -> ()
| Not_auto_func -> (* Normal C function *)
let bhvs = mk_post my_kf in
let my_state = Data_for_aorai.get_kf_init_state my_kf in
@@ -954,7 +974,8 @@ class visit_adding_pre_post_from_buch treatloops =
in
Annotations.add_behaviors Aorai_option.emitter my_kf bhvs;
SkipChildren
- | Not_auto_func -> DoChildren (* they are not considered here. *))
+ | Aux_func _ | Not_auto_func ->
+ DoChildren (* they are not considered here. *))
| _ -> DoChildren;
diff --git a/src/plugins/aorai/tests/aorai/oracle/hoare_seq.res.oracle b/src/plugins/aorai/tests/aorai/oracle/hoare_seq.res.oracle
index 18c655cce2c59fd9064f89f6ed6b63c72c9d744e..c420dac4bde2f7fb559303c95568f7bd79685dae 100644
--- a/src/plugins/aorai/tests/aorai/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/hoare_seq.res.oracle
@@ -230,6 +230,24 @@ void f(void)
return;
}
+/*@ ghost
+/@ assigns \nothing;
+
+ behavior bhv:
+ assumes c > 0;
+ ensures \result ≡ 1;
+ assigns \nothing;
+
+ behavior bhv_out:
+ assumes ¬(c > 0);
+ ensures \result ≡ 0;
+ assigns \nothing;
+
+ complete behaviors bhv, bhv_out;
+ disjoint behaviors bhv, bhv_out;
+ @/
+int main_bhv_bhv(int c); */
+
/*@ ghost
/@ requires
1 ≡ S0 ∧ 0 ≡ Sf ∧ 0 ≡ aorai_intermediate_state ∧
@@ -277,6 +295,7 @@ void f(void)
@/
void main_pre_func(int c)
{
+ int bhv_aux;
int S0_tmp;
int Sf_tmp;
int aorai_intermediate_state_tmp;
@@ -300,7 +319,10 @@ void f(void)
if (c <= 0) aorai_intermediate_state_0_tmp = 1;
else aorai_intermediate_state_0_tmp = 0;
else aorai_intermediate_state_0_tmp = 0;
- if (S0 == 1) aorai_intermediate_state_tmp = 1;
+ bhv_aux = main_bhv_bhv(c);
+ if (S0 == 1)
+ if (bhv_aux) aorai_intermediate_state_tmp = 1;
+ else aorai_intermediate_state_tmp = 0;
else aorai_intermediate_state_tmp = 0;
Sf_tmp = 0;
S0_tmp = 0;
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/hoare_seq.res.oracle b/src/plugins/aorai/tests/aorai/oracle_prove/hoare_seq.res.oracle
index e10a469f4eb782349a83d67248eea95c87de1ce1..2270c4bc39855f932441fed24b4032d593122f67 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle_prove/hoare_seq.res.oracle
@@ -2,5 +2,3 @@
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_hoare_seq_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[aorai-test] Warning: Could not prove ensures
- 0 ≡ aorai_intermediate_state in automaton function main_pre_func