diff --git a/src/kernel_services/abstract_interp/abstract_offset.ml b/src/kernel_services/abstract_interp/abstract_offset.ml
index 2184c2c297c5f0fa2c902b61fd3220fb1215a5c5..5a573091cbc7881db853f9c68bba15a9384908cb 100644
--- a/src/kernel_services/abstract_interp/abstract_offset.ml
+++ b/src/kernel_services/abstract_interp/abstract_offset.ml
@@ -56,7 +56,7 @@ sig
val append : t -> t -> t (* Does not check that the appened offset fits *)
val join : t -> t -> t
val of_cil_offset : (Cil_types.exp -> Ival.t) -> Cil_types.typ -> Cil_types.offset -> t
- val of_ival : Cil_types.typ -> Cil_types.typ -> Ival.t -> t
+ val of_ival : base_typ:Cil_types.typ -> typ:Cil_types.typ -> Ival.t -> t
val of_term_offset : Cil_types.typ -> Cil_types.term_offset -> t
val is_singleton : t -> bool
end
@@ -97,7 +97,8 @@ struct
match array_size with
| None -> None, None
| Some size_exp ->
- Some Integer.zero, Cil.constFoldToInt size_exp
+ Some Integer.zero,
+ Option.map Integer.pred (Cil.constFoldToInt size_exp)
let array_range array_size =
let l,u = array_bounds array_size in
@@ -119,34 +120,34 @@ struct
Index (idx, elem_typ, of_cil_offset oracle elem_typ sub)
| _ -> assert false
- let rec of_ival base_typ typ ival =
+ let rec of_ival ~base_typ ~typ ival =
if Ival.is_zero ival && type_compatible base_typ typ then
NoOffset typ
else
match Cil.unrollType base_typ with
| TArray (elem_typ, array_size, _, _) ->
- begin try
+ let range, rem =
+ try
let elem_size = Integer.of_int (Cil.bitsSizeOf elem_typ) in
if Integer.is_zero elem_size then (* array of elements of size 0 *)
if Ival.is_zero ival then (* the whole range is valid *)
- let sub = of_ival elem_typ typ ival in
- Index (array_range array_size, elem_typ, sub)
+ array_range array_size, ival
else (* Non-zero offset cannot represent anything here *)
raise Abstract_interp.Error_Top
else
- let range = Ival.scale_div ~pos:true elem_size ival
- and range_rem = Ival.scale_rem ~pos:true elem_size ival in
- let sub = of_ival elem_typ typ range_rem in
- Index (range, elem_typ, sub)
+ Ival.scale_div ~pos:true elem_size ival,
+ Ival.scale_rem ~pos:true elem_size ival
with Cil.SizeOfError (_,_) ->
(* Cil.bitsSizeOf can raise an exception when elements are
themselves array of execution-time size *)
if Ival.is_zero ival then
- let sub = of_ival elem_typ typ ival in
- Index (ival, elem_typ, sub)
+ ival, ival
else
raise Abstract_interp.Error_Top
- end
+ in
+ assert_valid_index range array_size;
+ let sub = of_ival ~base_typ:elem_typ ~typ rem in
+ Index (range, elem_typ, sub)
| TComp (ci, _, _) ->
if not ci.cstruct then
@@ -158,11 +159,11 @@ struct
| fi :: q ->
let offset, width = Cil.fieldBitsOffset fi in
let l = Integer.(of_int offset) in
- let u = Integer.(add l (of_int width)) in
+ let u = Integer.(pred (add l (of_int width))) in
let range = Ival.inject_range (Some l) (Some u) in
if Ival.is_included ival range then
let sub_ival = Ival.add_singleton_int (Integer.neg l) ival in
- Field (fi, of_ival fi.ftype typ sub_ival)
+ Field (fi, of_ival ~base_typ:fi.ftype ~typ sub_ival)
else
find_field q
in
@@ -170,14 +171,14 @@ struct
| _ -> raise Abstract_interp.Error_Top
- let of_ival base_typ typ ival =
+ let of_ival ~base_typ ~typ ival =
if Ival.is_small_set ival then
let f i acc =
- Bottom.join join acc (`Value (of_ival base_typ typ i))
+ Bottom.join join acc (`Value (of_ival ~base_typ ~typ i))
in
Bottom.non_bottom (Ival.fold_enum f ival `Bottom)
else
- of_ival base_typ typ ival
+ of_ival ~base_typ ~typ ival
let index_of_term array_size t = (* Exact constant ranges *)
match t.Cil_types.term_node with
@@ -239,8 +240,8 @@ struct
try `Value (TypedOffset.of_cil_offset oracle base_typ offset)
with Abstract_interp.Error_Top -> `Top
- let of_ival base_typ typ ival =
- try `Value (TypedOffset.of_ival base_typ typ ival)
+ let of_ival ~base_typ ~typ ival =
+ try `Value (TypedOffset.of_ival ~base_typ ~typ ival)
with Abstract_interp.Error_Top -> `Top
let of_term_offset base_typ toffset =
diff --git a/src/kernel_services/abstract_interp/abstract_offset.mli b/src/kernel_services/abstract_interp/abstract_offset.mli
index 8d0dde615cec5b1beb78ef27c2da599102ea8d72..519427ffd2aec3ea53284ab8860d2b61c69b559e 100644
--- a/src/kernel_services/abstract_interp/abstract_offset.mli
+++ b/src/kernel_services/abstract_interp/abstract_offset.mli
@@ -28,7 +28,7 @@ sig
val append : t -> t -> t (* Does not check that the appened offset fits *)
val join : t -> t -> t
val of_cil_offset : (Cil_types.exp -> Ival.t) -> Cil_types.typ -> Cil_types.offset -> t
- val of_ival : Cil_types.typ -> Cil_types.typ -> Ival.t -> t
+ val of_ival : base_typ:Cil_types.typ -> typ:Cil_types.typ -> Ival.t -> t
val of_term_offset : Cil_types.typ -> Cil_types.term_offset -> t
val is_singleton : t -> bool
end
diff --git a/src/kernel_services/abstract_interp/memory_map.ml b/src/kernel_services/abstract_interp/memory_map.ml
index 0beaf5ac7708f292dd93bcf0f2c0bdf4f8c7f331..ae56952e492c1ed7bb5fa4cd932b71b7a1da7854 100644
--- a/src/kernel_services/abstract_interp/memory_map.ml
+++ b/src/kernel_services/abstract_interp/memory_map.ml
@@ -127,7 +127,7 @@ struct
type location = Abstract_offset.typed_offset
type value = Value.t
- type 'fieldmap memory' =
+ type 'fieldmap memory =
| Raw of bit
| Scalar of memory_scalar
| Struct of 'fieldmap memory_struct
@@ -140,16 +140,16 @@ struct
and 'fieldmap memory_struct = {
struct_value: 'fieldmap;
struct_info: Cil_types.compinfo;
- struct_padding: bit; (* for missing fields *)
+ struct_padding: bit; (* for missing fields and padding *)
}
(* unions are handled separately from struct to avoid confusion and error *)
and 'fieldmap memory_union = {
- union_value: 'fieldmap memory';
+ union_value: 'fieldmap memory;
union_field: Cil_types.fieldinfo;
union_padding: bit;
}
and 'fieldmap memory_array = {
- array_value: 'fieldmap memory';
+ array_value: 'fieldmap memory;
array_cell_type: Cil_types.typ;
}
@@ -166,7 +166,7 @@ struct
end
module rec Memory :
- Hptmap.V with type t = FieldMap.t memory' =
+ Hptmap.V with type t = FieldMap.t memory =
struct
include Datatype.Make (
struct
@@ -183,14 +183,14 @@ struct
to FieldMap and no constants, only functions *)
and MemorySafe :
sig
- type t = FieldMap.t memory'
+ type t = FieldMap.t memory
val pretty : Format.formatter -> t -> unit
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
end =
struct
- type t = FieldMap.t memory'
+ type t = FieldMap.t memory
let rec pretty fmt =
let rec leading_indexes acc = function
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index 055b2b278f7dc86b2622b2647a5b7d878a41f3ce..170c56321a7cf547d6252d41e7669f1292df7f2b 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -227,7 +227,7 @@ end
module DomainPrototype =
struct
(* The domain is essentially a map from bases to individual memory abstractions *)
- module Initial_Values = struct let v = [] end
+ module Initial_Values = struct let v = [[]] end
module Deps = struct let l = [Ast.self] end
include Hptmap.Make
@@ -269,7 +269,7 @@ struct
let decide _ v1 v2 =
Memory.narrow v1 v2
in
- let narrow = join ~cache ~symmetric:true ~idempotent:true ~decide in
+ let narrow = join ~cache ~symmetric:false ~idempotent:true ~decide in
fun a b -> `Value (narrow a b)
let join =
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index b6cf1f8372e87e9f32484e878209d371c6600147..df4f7885cbb5e9847bf47054b41569dbf8d85ebb 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -138,7 +138,6 @@ module Domains =
let arg_name = "d1,...,dn"
let help = "Enable a list of analysis domains."
let default = Datatype.String.Set.of_list ["cvalue"]
- (* let default = Datatype.String.Set.singleton "cvalue" *)
end)
let () = add_precision_dep Domains.parameter