From 1fcf62eafbdea90b30619646142dcf8b6d546297 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 2 Feb 2024 11:00:03 +0100
Subject: [PATCH] Add locs for Ctypes.constant and cfgInfos.compute
---
src/plugins/wp/cfgInfos.ml | 2 ++
src/plugins/wp/ctypes.ml | 2 ++
2 files changed, 4 insertions(+)
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 653c64c01e7..031337e2cc9 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -423,6 +423,8 @@ let loop_contract_pids kf stmt =
| _ -> []
let compile Key.{ kf ; smoking ; bhv ; prop } =
+ let open Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = Kernel_function.get_location kf in
let body, checkpath, reachability =
if Kernel_function.has_definition kf then
let cfg = Cfg.get_automaton kf in
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index ed8d44bafa9..00b1c4c922c 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -236,6 +236,8 @@ let f_name = f_memo (Pretty_utils.to_string pp_float)
let char c = Integer.to_int64_exn (Cil.charConstToInt c)
let constant e =
+ let open Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = e.eloc in
match (Cil.constFold true e).enode with
| Const(CInt64(k,_,_)) ->
begin
--
GitLab