From 5d4611602a49e907c25d1787061aa1172d3b531a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 16 Jul 2021 16:05:02 +0200
Subject: [PATCH] [Eva] Fixes abstract_memory with respect to the new hptmap
signature.
---
.../abstract_interp/abstract_memory.ml | 11 +++++++----
1 file changed, 7 insertions(+), 4 deletions(-)
diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml
index 9bd10d0d569..aef329f81d8 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.ml
+++ b/src/kernel_services/abstract_interp/abstract_memory.ml
@@ -167,16 +167,19 @@ struct
module Prototype (
FieldMap :
sig
- type t
+ type 'a map
+ type v = t memory
+ and t = v map
include Hptmap_sig.S
- with type t := t
+ with type 'a map := 'a map
and type key = Cil_types.fieldinfo
- and type v = t memory
+ and type v := v
+ and type t := v map
end) =
struct
type t = FieldMap.t memory
- let rec pretty fmt =
+ let rec pretty fmt : t -> 'a =
let rec leading_indexes acc = function
| Array a -> leading_indexes (a.array_range :: acc) a.array_value
| (Raw _ | Scalar _ | Struct _ | Union _) as m -> List.rev acc, m
--
GitLab