Skip to content
Snippets Groups Projects
Commit 5d461160 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Fixes abstract_memory with respect to the new hptmap signature.

parent 3c15d950
No related branches found
No related tags found
No related merge requests found
...@@ -167,16 +167,19 @@ struct ...@@ -167,16 +167,19 @@ struct
module Prototype ( module Prototype (
FieldMap : FieldMap :
sig sig
type t type 'a map
type v = t memory
and t = v map
include Hptmap_sig.S include Hptmap_sig.S
with type t := t with type 'a map := 'a map
and type key = Cil_types.fieldinfo and type key = Cil_types.fieldinfo
and type v = t memory and type v := v
and type t := v map
end) = end) =
struct struct
type t = FieldMap.t memory type t = FieldMap.t memory
let rec pretty fmt = let rec pretty fmt : t -> 'a =
let rec leading_indexes acc = function let rec leading_indexes acc = function
| Array a -> leading_indexes (a.array_range :: acc) a.array_value | Array a -> leading_indexes (a.array_range :: acc) a.array_value
| (Raw _ | Scalar _ | Struct _ | Union _) as m -> List.rev acc, m | (Raw _ | Scalar _ | Struct _ | Union _) as m -> List.rev acc, m
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment