diff --git a/Makefile b/Makefile index 9598162d13dd7f6cdadbfa2006dc3e4a47cb4917..fc57451b0098a4e6a322ba70a38a37da3ba5a4a5 100644 --- a/Makefile +++ b/Makefile @@ -598,7 +598,7 @@ KERNEL_CMO=\ src/kernel_services/abstract_interp/lmap_bitwise.cmo \ src/kernel_services/abstract_interp/multidim.cmo \ src/kernel_services/abstract_interp/abstract_offset.cmo \ - src/kernel_services/abstract_interp/memory_map.cmo \ + src/kernel_services/abstract_interp/abstract_memory.cmo \ src/kernel_services/visitors/visitor.cmo \ src/kernel_services/ast_data/statuses_by_call.cmo \ src/kernel_services/ast_printing/printer_tag.cmo \ diff --git a/headers/header_spec.txt b/headers/header_spec.txt index 8c1613bca1f4f69960a04531efbf9468d687fefd..c62c5c099a76660fec06a6564f5e8d89e710add8 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -437,6 +437,8 @@ src/kernel_services/README.md: .ignore src/kernel_services/abstract_interp/README.md: .ignore src/kernel_services/abstract_interp/abstract_interp.ml: CEA_LGPL src/kernel_services/abstract_interp/abstract_interp.mli: CEA_LGPL +src/kernel_services/abstract_interp/abstract_memory.ml: CEA_LGPL +src/kernel_services/abstract_interp/abstract_memory.mli: CEA_LGPL src/kernel_services/abstract_interp/abstract_offset.ml: CEA_LGPL src/kernel_services/abstract_interp/abstract_offset.mli: CEA_LGPL src/kernel_services/abstract_interp/base.ml: CEA_LGPL @@ -477,8 +479,6 @@ src/kernel_services/abstract_interp/locations.ml: CEA_LGPL src/kernel_services/abstract_interp/locations.mli: CEA_LGPL src/kernel_services/abstract_interp/map_lattice.ml: CEA_LGPL src/kernel_services/abstract_interp/map_lattice.mli: CEA_LGPL -src/kernel_services/abstract_interp/memory_map.ml: CEA_LGPL -src/kernel_services/abstract_interp/memory_map.mli: CEA_LGPL src/kernel_services/abstract_interp/multidim.ml: CEA_LGPL src/kernel_services/abstract_interp/multidim.mli: CEA_LGPL src/kernel_services/abstract_interp/offsetmap.ml: CEA_LGPL diff --git a/src/kernel_services/abstract_interp/memory_map.ml b/src/kernel_services/abstract_interp/abstract_memory.ml similarity index 100% rename from src/kernel_services/abstract_interp/memory_map.ml rename to src/kernel_services/abstract_interp/abstract_memory.ml diff --git a/src/kernel_services/abstract_interp/memory_map.mli b/src/kernel_services/abstract_interp/abstract_memory.mli similarity index 100% rename from src/kernel_services/abstract_interp/memory_map.mli rename to src/kernel_services/abstract_interp/abstract_memory.mli diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml index cec335a9e4c7a96063332bd06ae6be4d80846bf3..319d866f25a248c80ff758f4b6ac9d9b0a86b3d4 100644 --- a/src/plugins/value/domains/multidim_domain.ml +++ b/src/plugins/value/domains/multidim_domain.ml @@ -43,14 +43,14 @@ struct let of_integer = inject_int let of_bit = function - | Memory_map.Zero -> inject_int Integer.zero + | Abstract_memory.Zero -> inject_int Integer.zero | Any (Set s) -> inject_top_origin Origin.top s | Any (Top) -> top_with_origin Origin.top let to_bit v = if is_zero v - then Memory_map.Zero - else Memory_map.Any (get_bases v) + then Abstract_memory.Zero + else Abstract_memory.Any (get_bases v) let backward_is_finite positive fkind v = let prec = Fval.kind fkind in @@ -163,7 +163,7 @@ end module Memory = struct module Config = struct let deps = [Ast.self] end - module Memory = Memory_map.Make (Config) (Value) + module Memory = Abstract_memory.Make (Config) (Value) module Prototype = (* Datatype *) @@ -349,7 +349,7 @@ struct | `Value value -> write (fun m off -> Memory.overwrite ~weak m off value) state dst - let erase (state : state) (dst : mdlocation) (b : Memory_map.bit): state = + let erase (state : state) (dst : mdlocation) (b : Abstract_memory.bit): state = let weak = not (Location.is_singleton dst) in write (fun m off -> Memory.erase ~weak m off b) state dst @@ -430,7 +430,7 @@ struct let src = Location.of_lval oracle right.lval in `Value (overwrite state dst src) with Abstract_interp.Error_Top | Abstract_interp.Error_Bottom -> - `Value (erase state dst Memory_map.Bit.top) + `Value (erase state dst Abstract_memory.Bit.top) with Abstract_interp.Error_Top | Abstract_interp.Error_Bottom -> (* Failed to evaluate the left location *) `Value top @@ -492,7 +492,7 @@ struct match sources with | [] -> let dst = Location.of_precise_loc location in - erase state dst Memory_map.Bit.numerical + erase state dst Abstract_memory.Bit.numerical | _ -> remove state location @@ -530,15 +530,15 @@ struct let initialize_variable lval _loc ~initialized:_ init_value state = let dst = Location.of_lval no_oracle lval in let d = match init_value with - | Abstract_domain.Top -> Memory_map.Bit.numerical - | Abstract_domain.Zero -> Memory_map.Bit.zero + | Abstract_domain.Top -> Abstract_memory.Bit.numerical + | Abstract_domain.Zero -> Abstract_memory.Bit.zero in erase state dst d let initialize_variable_using_type _kind vi state = let lval = Cil.var vi in let dst = Location.of_lval no_oracle lval in - erase state dst Memory_map.Bit.top + erase state dst Abstract_memory.Bit.top let relate _kf _bases _state = Base.SetLattice.empty