From f0c7ae25787cc4ca3e02c51b79394322c501cbbf Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 2 Feb 2024 10:17:35 +0100
Subject: [PATCH] Give a expr loc in plain_array_to_ptr
---
src/kernel_services/ast_queries/logic_utils.ml | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 976d4f69902..a16e6432ea8 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -96,12 +96,14 @@ let logicCType t =
in plain_or_set logicCType t
let plain_array_to_ptr ty =
+ let open Cil_const.CurrentLoc.Operators in
match unroll_type ty with
| Ctype(TArray(ty,lo,attr) as tarr) ->
let length_attr =
match lo with
| None -> []
- | Some _ ->
+ | Some e ->
+ let* CurrentLocUpdated = e.eloc in
try
let len = Cil.bitsSizeOf tarr in
let len = try len / (Cil.bitsSizeOf ty)
--
GitLab