From cdde6e8c2188c2bd80ed0ffa01fc7142772af129 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 10 Jul 2020 15:04:06 +0200
Subject: [PATCH] [Kernel] Status_by_call changes node after visit for
replacement
---
.../ast_data/statuses_by_call.ml | 41 ++++++++++---------
1 file changed, 22 insertions(+), 19 deletions(-)
diff --git a/src/kernel_services/ast_data/statuses_by_call.ml b/src/kernel_services/ast_data/statuses_by_call.ml
index 2487ade6c49..24779c45007 100644
--- a/src/kernel_services/ast_data/statuses_by_call.ml
+++ b/src/kernel_services/ast_data/statuses_by_call.ml
@@ -111,23 +111,27 @@ let replacement_visitor ~arguments = object (self)
| TVar { lv_origin = Some vinfo } when vinfo.vformal ->
if under_label then raise Non_Transposable;
begin
- let new_term = replace_formal_by_concrete vinfo arguments in
- let add_offset lv = TLval (Logic_const.addTermOffsetLval t_offset lv) in
- match new_term.term_node with
- | TLval lv -> Cil.ChangeDoChildrenPost (add_offset lv, fun x -> x)
- | _ ->
- if t_offset = TNoOffset
- then Cil.ChangeTo new_term.term_node
- else
- let ltyp = new_term.term_type in
- let tmp_lvar = Cil.make_temp_logic_var ltyp in
- let tmp_linfo =
- { l_var_info = tmp_lvar; l_body = LBterm new_term;
- l_type = None; l_tparams = []; l_labels = []; l_profile = []; }
- in
- let lval_node = TLval (TVar tmp_lvar, t_offset) in
- let lval_term = Tlet (tmp_linfo, Logic_const.term lval_node ltyp) in
- Cil.ChangeDoChildrenPost (lval_term, fun x -> x)
+ let post_replace _ =
+ let new_term = replace_formal_by_concrete vinfo arguments in
+ let add_offset lv =
+ TLval (Logic_const.addTermOffsetLval t_offset lv)
+ in
+ match new_term.term_node with
+ | TLval lv -> add_offset lv
+ | node ->
+ if t_offset = TNoOffset then node
+ else
+ let ltyp = new_term.term_type in
+ let tmp_lvar = Cil.make_temp_logic_var ltyp in
+ let tmp_linfo =
+ { l_var_info = tmp_lvar; l_body = LBterm new_term;
+ l_type = None; l_tparams = []; l_labels = [];
+ l_profile = []; }
+ in
+ let lval_node = TLval (TVar tmp_lvar, t_offset) in
+ Tlet (tmp_linfo, Logic_const.term lval_node ltyp)
+ in
+ Cil.DoChildrenPost post_replace
end
| _ -> Cil.DoChildren
@@ -149,8 +153,7 @@ let replacement_visitor ~arguments = object (self)
| _ -> Cil.DoChildren
method! vlogic_label = function
- | BuiltinLabel Pre ->
- Cil.ChangeDoChildrenPost (Logic_const.here_label, fun x -> x)
+ | BuiltinLabel Pre -> Cil.DoChildrenPost (fun _ -> Logic_const.here_label)
| _ -> Cil.DoChildren
end
--
GitLab