[wp] fixup constructor handling

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