From b15067dffed8b511a6b543e80225625ccdb16a37 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 25 Jan 2021 09:42:25 +0100
Subject: [PATCH] [wp] fixup constructor handling
---
src/plugins/wp/cfgCalculus.ml | 43 +++++++++++++++++++++--------------
1 file changed, 26 insertions(+), 17 deletions(-)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 6f0eb2cfe2d..1142f94be4a 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -238,27 +238,36 @@ struct
(* Compute a single instruction *)
and instr env s instr (w : W.t_prop) : W.t_prop =
- let do_call res fct args _loc =
- match Kernel_function.get_called fct with
- | Some kf -> call env s res kf args w
- | None ->
- match Dyncall.get ~bhv:env.mode.bhv.b_name s with
- | None ->
- WpLog.warning ~once:true "Missing dynamic-call infos." ;
- let ad = WpPropId.mk_stmt_assigns_any_desc s in
- W.use_assigns env.we None ad (W.merge env.we w env.wk)
- | Some(prop,kfs) ->
- let id = WpPropId.mk_property prop in
- W.call_dynamic env.we s id fct @@
- List.map (fun kf -> kf, call env s res kf args w) kfs
- in
match instr with
| Skip _ | Code_annot _ -> w
| Set(lv,e,_) -> W.assign env.we s lv e w
| Local_init(x,AssignInit i,_) -> W.init env.we x (Some i) w
- | Local_init(x,ConsInit (fct, args, kind), loc) ->
- Cil.treat_constructor_as_func do_call x fct args kind loc
- | Call(res,fct,args,loc) -> do_call res fct args loc
+ | Local_init(x,ConsInit (vf, args, kind), loc) ->
+ Cil.treat_constructor_as_func
+ begin fun r fct args _loc ->
+ match Kernel_function.get_called fct with
+ | Some kf -> call env s r kf args w
+ | None ->
+ WpLog.warning ~once:true "No function for constructor '%s'"
+ vf.vname ;
+ let any = WpPropId.mk_stmt_assigns_any_desc s in
+ W.use_assigns env.we None any (W.merge env.we w env.wk)
+ end x vf args kind loc
+ | Call(res,fct,args,_loc) ->
+ begin
+ match Kernel_function.get_called fct with
+ | Some kf -> call env s res kf args w
+ | None ->
+ match Dyncall.get ~bhv:env.mode.bhv.b_name s with
+ | None ->
+ WpLog.warning ~once:true "Missing dynamic-call infos." ;
+ let any = WpPropId.mk_stmt_assigns_any_desc s in
+ W.use_assigns env.we None any (W.merge env.we w env.wk)
+ | Some(prop,kfs) ->
+ let id = WpPropId.mk_property prop in
+ W.call_dynamic env.we s id fct @@
+ List.map (fun kf -> kf, call env s res kf args w) kfs
+ end
| Asm _ ->
W.use_assigns env.we None (WpPropId.mk_asm_assigns_desc s) w
--
GitLab