diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml index 9bd10d0d569a91f7ff13066cfe2b001f627a16c4..aef329f81d86efb0834ba3f341870fad5c1f6202 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