71 open Hints_declaration
92 GenMem.mem -> Pointers.pointer -> Nat.nat -> ByteValues.beval List.list
94 let rec loadn m ptr = function
95 | Nat.O -> Types.Some List.Nil
97 (match GenMem.beloadv m ptr with
98 | Types.None -> Types.None
101 (Pointers.shift_pointer (Nat.S (Nat.S Nat.O)) ptr
102 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S Nat.O)) (Nat.S
104 | Types.None -> Types.None
105 | Types.Some vs -> Types.Some (List.Cons (v, vs))))
108 AST.typ -> GenMem.mem -> Pointers.pointer -> Values.val0 Types.option **)
110 match loadn m ptr (AST.typesize t) with
111 | Types.None -> Types.None
112 | Types.Some vs -> Types.Some (FrontEndVal.be_to_fe_value t vs)
115 AST.typ -> GenMem.mem -> Values.val0 -> Values.val0 Types.option **)
116 let rec loadv t m = function
117 | Values.Vundef -> Types.None
118 | Values.Vint (x, x0) -> Types.None
119 | Values.Vnull -> Types.None
120 | Values.Vptr ptr -> load t m ptr
123 GenMem.mem -> Pointers.pointer -> ByteValues.beval List.list ->
124 GenMem.mem Types.option **)
125 let rec storen m ptr = function
126 | List.Nil -> Types.Some m
127 | List.Cons (v, tl) ->
128 (match GenMem.bestorev m ptr v with
129 | Types.None -> Types.None
132 (Pointers.shift_pointer (Nat.S (Nat.S Nat.O)) ptr
133 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S Nat.O)) (Nat.S Nat.O)))
137 AST.typ -> GenMem.mem -> Pointers.pointer -> Values.val0 -> GenMem.mem
139 let store t m ptr v =
140 storen m ptr (FrontEndVal.fe_to_be_values t v)
143 AST.typ -> GenMem.mem -> Values.val0 -> Values.val0 -> GenMem.mem
145 let storev t m addr v =
147 | Values.Vundef -> Types.None
148 | Values.Vint (x, x0) -> Types.None
149 | Values.Vnull -> Types.None
150 | Values.Vptr ptr -> store t m ptr v
152 (** val valid_pointer : GenMem.mem -> Pointers.pointer -> Bool.bool **)
153 let valid_pointer m ptr =
155 BitVectorZ.z_of_unsigned_bitvector Pointers.offset_size
156 (Pointers.offv ptr.Pointers.poff)
160 (Z.zltb (Pointers.block_id ptr.Pointers.pblock) m.GenMem.nextblock)
161 (Z.zleb (GenMem.low_bound m ptr.Pointers.pblock) off))
162 (Z.zltb off (GenMem.high_bound m ptr.Pointers.pblock))