diff --git a/share/analysis-scripts/analysis.mk b/share/analysis-scripts/analysis.mk
index 479753a326111a812e8c8a78c65ff1fc7ed82287..dc9e7e41e9c6d3a108c5a10e99352c74dffca705 100644
--- a/share/analysis-scripts/analysis.mk
+++ b/share/analysis-scripts/analysis.mk
@@ -121,7 +121,7 @@ EVAFLAGS ?= \
-eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state \
-eva-print-callstacks -eva-warn-key alarm=inactive \
-no-deps-print -no-calldeps-print \
- -eva-warn-key garbled-mix=active,garbled-mix:write=feedback \
+ -eva-warn-key garbled-mix=active,garbled-mix:write=active \
-calldeps -from-verbose 0 \
$(if $(EVABUILTINS), -eva-builtin=$(call fc_list,$(EVABUILTINS)),) \
$(if $(EVAUSESPECS), -eva-use-spec $(call fc_list,$(EVAUSESPECS)),)
diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml
index cd0302182f097efe009c8ea7585809ed908c4857..f401f1594ad1c808bca9fa2c2909eaba6f127dd5 100644
--- a/src/kernel_services/abstract_interp/cvalue.ml
+++ b/src/kernel_services/abstract_interp/cvalue.ml
@@ -240,7 +240,7 @@ module V = struct
let pretty_typ typ fmt v =
let pretty_org fmt org =
- if not (Origin.is_top org) then
+ if not (Origin.is_unknown org) then
Format.fprintf fmt "@ @[(origin: %a)@]" Origin.pretty org
in
match v with
@@ -510,7 +510,7 @@ module V = struct
(topify_with_origin_kind topify e2)
end
- let arithmetic_function = import_function ~topify:Origin.K_Arith
+ let arithmetic_function = import_function ~topify:Origin.Arith
(* Compute the pointwise difference between two Locations_Bytes.t. *)
let sub_untyped_pointwise = sub_pointwise
@@ -600,13 +600,13 @@ module V = struct
else if equal singleton_zero v2 then v1
else if equal v1 v2 && cardinal_zero_or_one v1 then v1
else
- import_function ~topify:Origin.K_Arith Ival.bitwise_or v1 v2
+ import_function ~topify:Origin.Arith Ival.bitwise_or v1 v2
let bitwise_and v1 v2 =
if equal v1 v2 && cardinal_zero_or_one v1 then v1
else
let f i1 i2 = Ival.bitwise_and i1 i2 in
- import_function ~topify:Origin.K_Arith f v1 v2
+ import_function ~topify:Origin.Arith f v1 v2
let shift_right e1 e2 =
arithmetic_function Ival.shift_right e1 e2
@@ -706,7 +706,7 @@ module V = struct
Int.min card (Int.two_power size)
let add_untyped ~factor v1 v2 =
- add_untyped ~topify:Origin.K_Arith ~factor v1 v2
+ add_untyped ~topify:Origin.Arith ~factor v1 v2
end
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index c289a18af63691b080c6045239c82b5ba653d95a..e09243ea9c2a696788354c95601053fd8a269e08 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -187,7 +187,7 @@ struct
let offm' =
match size with
| Int_Base.Top ->
- let orig = Origin.current Origin.K_Arith in
+ let orig = Origin.current Origin.Misalign_write in
Offsetmap.update_imprecise_everywhere ~validity orig v offm
| Int_Base.Value size ->
assert (Int.ge size Int.zero);
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index c6e327fac31841eacbf50aebd569c2ee1b8e1ab1..4e951a71e40ac0261ed1587cde7b900bb860f053 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -190,57 +190,9 @@ module Location_Bytes = struct
in
M.fold aux_base m (Some Int.zero)
- (* These two states contain the garbled mix that we track. The list preserves
- the creation order (except it is reversed), while the set is used to test
- inclusion efficiently so far. Only "original" garbled mix are tracked,
- i.e. operations that _transform a garbled mix are not tracked. *)
- module ListGarbledMix = State_builder.List_ref(MapSetLattice)
- (struct
- let name = "Locations.ListGarbledMix"
- let dependencies = [M.self]
- end)
- module SetGarbledMix = State_builder.Set_ref(MapSetLattice.Set)
- (struct
- let name = "Locations.SetGarbledMix"
- let dependencies = [M.self]
- end)
-
- let get_garbled_mix () = List.rev (ListGarbledMix.get ())
- let clear_garbled_mix () =
- ListGarbledMix.clear ();
- SetGarbledMix.clear ();
- ;;
-
- (* We skip Well origins, because they have no location information and can be
- tracked in the initial state. Unknown origins have no location, and are
- only built as a side-product of the analysis. Leaf origins are also
- skipped, because we may create tons of those, that get reduced to precise
- values by the specifications of the function. *)
- let is_gm_to_log m =
- let open Origin in
- match m with
- | Map _ | Top (_, (Well | Unknown | Leaf _)) -> false
- | Top (_, (Misalign_read _ | Merge _ | Arith _)) -> true
-
- let ref_track_garbled_mix = ref true
- let do_track_garbled_mix b = ref_track_garbled_mix := b
-
- (* track a garbled mix if needed, then return it (more convenient for the
- caller). *)
- let track_garbled_mix gm =
- if !ref_track_garbled_mix && is_gm_to_log gm && not (SetGarbledMix.mem gm)
- then begin
- SetGarbledMix.set (MapSetLattice.Set.add gm (SetGarbledMix.get ()));
- ListGarbledMix.set (gm :: ListGarbledMix.get ());
- end;
- gm
-
- let top_with_origin origin =
- track_garbled_mix (Top(Base.SetLattice.top, origin))
-
- (* This internal function builds a garbled mix, but does *not* track its
- creation. This is useful for functions that transform existing GMs. *)
- let inject_top_origin_internal o b =
+ let top_with_origin origin = Top (Base.SetLattice.top, origin)
+
+ let inject_top_origin o b =
if Base.Hptset.(equal b empty || equal b Base.null_set) then
top_int
else begin
@@ -250,15 +202,12 @@ module Location_Bytes = struct
Top (Base.(SetLattice.inject (Hptset.add null b)), o)
end
- let inject_top_origin o b =
- track_garbled_mix (inject_top_origin_internal o b)
-
(** some functions can reduce a garbled mix, make sure to normalize
the result when only NULL remains *)
let normalize_top m =
match m with
| Top (Base.SetLattice.Top, _) | Map _ -> m
- | Top (Base.SetLattice.Set s, o) -> inject_top_origin_internal o s
+ | Top (Base.SetLattice.Set s, o) -> inject_top_origin o s
let narrow m1 m2 = normalize_top (narrow m1 m2)
let meet m1 m2 = normalize_top (meet m1 m2)
@@ -273,8 +222,7 @@ module Location_Bytes = struct
else
match get_keys v with
| Base.SetLattice.Top -> top_with_origin o
- | Base.SetLattice.Set b ->
- track_garbled_mix (inject_top_origin_internal o b)
+ | Base.SetLattice.Set b -> inject_top_origin o b
let topify_with_origin_kind ok v =
let o = Origin.current ok in
@@ -291,16 +239,16 @@ module Location_Bytes = struct
with Not_found -> false
let topify_merge_origin v =
- topify_with_origin_kind Origin.K_Merge v
+ topify_with_origin_kind Origin.Merge v
let topify_misaligned_read_origin v =
- topify_with_origin_kind Origin.K_Misalign_read v
+ topify_with_origin_kind Origin.Misalign_read v
let topify_arith_origin v =
- topify_with_origin_kind Origin.K_Arith v
+ topify_with_origin_kind Origin.Arith v
let topify_leaf_origin v =
- topify_with_origin_kind Origin.K_Leaf v
+ topify_with_origin_kind Origin.Leaf v
let may_reach base loc =
if Base.is_null base then true
@@ -331,7 +279,7 @@ module Location_Bytes = struct
if Base.Hptset.equal garble nonlocals then
false, v
else
- true, inject_top_origin_internal orig nonlocals
+ true, inject_top_origin orig nonlocals
| Map m ->
let nonlocals = M.filter non_local m in
if M.equal nonlocals m then
@@ -370,7 +318,7 @@ module Location_Bytes = struct
match v with
| Top (Base.SetLattice.Top, _) -> false, v
| Top (Base.SetLattice.Set set, origin) ->
- substitute Base.Hptset.replace (inject_top_origin_internal origin) set
+ substitute Base.Hptset.replace (inject_top_origin origin) set
| Map map ->
let decide _key = Ival.join in
substitute (M.replace_key ~decide) (fun m -> Map m) map
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index fe99c8a4a3830755707a30b1d4d46dcaf655c9ca..c00226fda5c88eb32e638f77ccfe6857cb1b8a60 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -216,17 +216,6 @@ module Location_Bytes : sig
val may_reach : Base.t -> t -> bool
(** [may_reach base loc] is true if [base] might be accessed from [loc]. *)
-
- val get_garbled_mix: unit -> t list
- (** All the garbled mix that have been created so far, sorted by "temporal"
- order of emission. *)
-
- val clear_garbled_mix: unit -> unit
- (** Clear the information on created garbled mix. *)
-
- val do_track_garbled_mix: bool -> unit
- val track_garbled_mix: t -> t
-
(**/**)
val pretty_debug: t Pretty_utils.formatter
val clear_caches: unit -> unit
diff --git a/src/kernel_services/abstract_interp/map_lattice.ml b/src/kernel_services/abstract_interp/map_lattice.ml
index 7a64bce7a05c21606a7fe6076943933e596c80fd..46c8138c810a831fb0e3ebf926354588849c5788 100644
--- a/src/kernel_services/abstract_interp/map_lattice.ml
+++ b/src/kernel_services/abstract_interp/map_lattice.ml
@@ -286,7 +286,7 @@ module Make_MapSet_Lattice
type t = Top of KSet.t * Origin.t | Map of KVMap.t
- let top = Top (KSet.top, Origin.top)
+ let top = Top (KSet.top, Origin.unknown)
let bottom = Map KVMap.empty
@@ -366,12 +366,12 @@ module Make_MapSet_Lattice
match t1, t2 with
| Top _ as x, Map _
| Map _, (Top _ as x) -> x (* arbitrary, may be approximated *)
- | Top (s1, o1), Top (s2, o2) -> Top (KSet.link s1 s2, Origin.link o1 o2)
+ | Top (s1, o1), Top (s2, o2) -> Top (KSet.link s1 s2, Origin.join o1 o2)
| Map m1, Map m2 -> Map (KVMap.link m1 m2)
let meet t1 t2 =
match t1, t2 with
- | Top (s1, o1), Top (s2, o2) -> Top (KSet.meet s1 s2, Origin.meet o1 o2)
+ | Top (s1, o1), Top (s2, o2) -> Top (KSet.meet s1 s2, Origin.join o1 o2)
| Top (KSet.Top, _), (Map _ as m)
| (Map _ as m), Top (KSet.Top, _) -> m
| Top (KSet.Set s, _), (Map m)
@@ -382,7 +382,7 @@ module Make_MapSet_Lattice
let narrow t1 t2 =
match t1, t2 with
| Top (s1, o1), Top (s2, o2) ->
- Top (KSet.narrow s1 s2, Origin.narrow o1 o2)
+ Top (KSet.narrow s1 s2, Origin.join o1 o2)
| Top (KSet.Top, _), (Map _ as m)
| (Map _ as m), Top (KSet.Top, _) -> m
| Top (KSet.Set set, _), (Map m)
@@ -392,8 +392,7 @@ module Make_MapSet_Lattice
let is_included t1 t2 =
match t1, t2 with
- | Top (s1, o1), Top (s2, o2) ->
- KSet.is_included s1 s2 && Origin.is_included o1 o2
+ | Top (s1, _), Top (s2, _) -> KSet.is_included s1 s2
| Map _, Top (KSet.Top, _) -> true
| Map m, Top (KSet.Set s, _) -> KVMap.for_all (fun k _ -> KSet.O.mem k s) m
| Top _, Map _ -> false
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index aea3c83d87c39b133c34d5a4614a815bcda873b7..08fa4d98a93a955bd17f37776e332b8e9bca9a84 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -1144,7 +1144,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
pretty_int abs_min pretty_int abs_max pretty_int rem1 pretty_int
modu1 V.pretty v1 pretty_int rem2 pretty_int modu2 V.pretty v2 ; *)
else
- let topify = Origin.K_Merge in
+ let topify = Origin.Merge in
let offset = abs_min in
let size = Integer.length abs_min abs_max in
let v1_fit = modu1 =~ size && Rel.is_zero rem1
@@ -1174,7 +1174,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
(* similar to [f_aux_merge_generic], but we perform a reinterpretation in
all cases. This is to ensure that [V.narrow] can be applied soundly. *)
let f_aux_merge_narrow merge_v abs_min abs_max rem1 modu1 v1 rem2 modu2 v2 =
- let topify = Origin.K_Merge in
+ let topify = Origin.Merge in
let offset = abs_min in
let size = Integer.length abs_min abs_max in
let v1' =
@@ -1380,7 +1380,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
if V.is_isotropic v
then v
else
- let origin = Origin.(current K_Misalign_read) in
+ let origin = Origin.(current Misalign_read) in
V.topify_with_origin origin v
in
V.join subl_value (V.join subr_value current_node_value)
@@ -1523,7 +1523,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
(* Finds the value associated to some offsets represented as an ival. *)
let find ~validity ?(conflate_bottom=true) ~offsets ~size tree =
let offsets = Tr_offset.trim_by_validity offsets size validity in
- let topify = Origin.K_Misalign_read in
+ let topify = Origin.Misalign_read in
let read_one_node ~offset node ~start ~size acc =
extract_bits_and_stitch ~topify ~conflate_bottom
~offset:start ~size
@@ -1666,7 +1666,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
else if V.is_isotropic v_node
then rem, size, V.anisotropic_cast ~size joined_value
else
- let origin = Origin.(current K_Merge) in
+ let origin = Origin.(current Merge) in
let new_value = V.topify_with_origin origin joined_value in
let new_rem = Rel.zero and new_modu = Integer.one in
new_rem, new_modu, new_value
@@ -1846,9 +1846,10 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let update_aux_tr_offsets ~exact ~offsets ~size v curr_off t =
match offsets with
| Tr_offset.Overlap (mn, mx, origin) ->
- let origin = if origin = Origin.Unknown
- then Origin.(current K_Misalign_read)
- else origin
+ let origin =
+ match origin with
+ | Some origin -> origin
+ | None -> Origin.(current Misalign_write)
in
let v = V.topify_with_origin origin v in
(* TODO: check *)
@@ -1871,7 +1872,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let v =
if Int.is_zero (period %~ size) then v
else
- let origin = Origin.(current K_Misalign_read) in
+ let origin = Origin.(current Misalign_write) in
let v' = V.topify_with_origin origin v in
if not (V.equal v v') then
Lattice_messages.emit_approximation msg_emitter
@@ -2802,14 +2803,14 @@ module Make_bitwise(V: sig
in
`Value (Int_Intervals.fold aux_itv itvs m)
with Error_Top ->
- update_imprecise_everywhere ~validity Origin.top v m
+ update_imprecise_everywhere ~validity Origin.(current Misalign_write) v m
let add_binding_ival ~validity ~exact offsets ~size v m =
match size with
| Int_Base.Value size ->
update ~validity ~exact ~offsets ~size v m
| Int_Base.Top ->
- update_imprecise_everywhere ~validity Origin.top v m
+ update_imprecise_everywhere ~validity Origin.(current Misalign_write) v m
let fold_itv ?direction ~entire f itv m acc =
let f' itv (v, _, _) acc = f itv v acc in
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index b804d1db97f5c4d417e95faeb2a0359694006b5f..357ebfd681a2f55cc8dd3ab93b61e9545dac4988 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -21,249 +21,181 @@
(**************************************************************************)
type kind =
- | K_Misalign_read
- | K_Leaf
- | K_Merge
- | K_Arith
-
-module Location = Cil_datatype.Location
-
-module LocationLattice = struct
-
- type t = Top | Bottom | Value of Location.t
-
- module Datatype_Input = struct
- include Datatype.Serializable_undefined
-
- type nonrec t = t
- let name = "Origin.LocationLattice"
- let reprs = [ Top ]
- let structural_descr =
- Structural_descr.t_sum [| [| Location.packed_descr |] |]
-
- let compare l1 l2 =
- match l1, l2 with
- | Top, Top | Bottom, Bottom -> 0
- | Value loc1, Value loc2 -> Location.compare loc1 loc2
- | Top, _ -> 1
- | _, Top -> -1
- | Bottom, _ -> -1
- | _, Bottom -> 1
-
- let equal l1 l2 =
- match l1, l2 with
- | Top, Top | Bottom, Bottom -> true
- | Value loc1, Value loc2 -> Location.equal loc1 loc2
- | _ -> false
-
- let hash = function
- | Top -> 3
- | Bottom -> 5
- | Value loc -> Location.hash loc * 7
-
- let pretty fmt = function
- | Top -> Format.fprintf fmt "Top"
- | Bottom -> Format.fprintf fmt "Bottom"
- | Value loc -> Format.fprintf fmt "{%a}" Location.pretty loc
- end
-
- include (Datatype.Make (Datatype_Input) : Datatype.S with type t := t)
-
- let current_loc () = Value (Cil.CurrentLoc.get ())
-
- let join l1 l2 =
- if l1 == l2 then l1 else
- match l1, l2 with
- | Top, _ | _, Top -> Top
- | Bottom , l | l, Bottom -> l
- | Value loc1, Value loc2 ->
- if Location.equal loc1 loc2 then l1 else Top
-
- let narrow l1 l2 =
- if l1 == l2 then l1 else
- match l1, l2 with
- | Bottom, _ | _, Bottom -> Bottom
- | Top , l | l, Top -> l
- | Value loc1, Value loc2 ->
- if Location.equal loc1 loc2 then l1 else Bottom
-
- let meet = narrow
-end
-
-type origin =
- | Misalign_read of LocationLattice.t
- | Leaf of LocationLattice.t
- | Merge of LocationLattice.t
- | Arith of LocationLattice.t
+ | Misalign_read
+ | Misalign_write
+ | Leaf
+ | Merge
+ | Arith
+
+let kind_rank = function
+ | Misalign_read -> 0
+ | Misalign_write -> 1
+ | Leaf -> 2
+ | Merge -> 3
+ | Arith -> 4
+
+let kind_label = function
+ | Misalign_read -> "Misaligned read"
+ | Misalign_write -> "Misaligned write"
+ | Leaf -> "Library function"
+ | Merge -> "Merge"
+ | Arith -> "Arithmetic"
+
+type location = Cil_datatype.Location.t
+
+type tt =
+ | Origin of { kind: kind; loc: location; id: int; }
| Well
| Unknown
+(* Unique id for each origin. Used to keep the oldest origin when a garbled
+ mix may have several origins. *)
+module Id = State_builder.Counter (struct let name = "Origin.Id" end)
+
+let current kind =
+ let id = Id.next () in
+ let loc = Cil.CurrentLoc.get () in
+ Origin { kind; loc; id; }
+
+let well = Well
+let unknown = Unknown
+let is_unknown t = t = Unknown
+
+module Prototype = struct
+ include Datatype.Serializable_undefined
+ type t = tt
+ let name = "Origin"
+ let reprs = [ Unknown ]
+
+ let compare t1 t2 =
+ match t1, t2 with
+ | Origin o1, Origin o2 ->
+ if o1.kind = o2.kind
+ then Cil_datatype.Location.compare o1.loc o2.loc
+ else kind_rank o2.kind - kind_rank o1.kind
+ | Well, Well | Unknown, Unknown -> 0
+ | Origin _, _ | Well, Unknown -> 1
+ | _, Origin _ | Unknown, Well -> -1
+
+ let equal = Datatype.from_compare
+
+ let hash = function
+ | Well -> 0
+ | Unknown -> 1
+ | Origin { kind; loc; } ->
+ Hashtbl.hash (kind_rank kind, Cil_datatype.Location.hash loc) + 2
+
+ let pretty fmt = function
+ | Well -> Format.fprintf fmt "Well"
+ | Unknown -> Format.fprintf fmt "Unknown"
+ | Origin { kind; loc; } ->
+ let pretty_loc = Cil_datatype.Location.pretty in
+ Format.fprintf fmt "%s@ {%a}" (kind_label kind) pretty_loc loc
+end
-let current = function
- | K_Misalign_read -> Misalign_read (LocationLattice.current_loc ())
- | K_Leaf -> Leaf (LocationLattice.current_loc ())
- | K_Merge -> Merge (LocationLattice.current_loc ())
- | K_Arith -> Arith (LocationLattice.current_loc ())
-
-let equal o1 o2 = match o1, o2 with
- | Well, Well | Unknown, Unknown -> true
- | Leaf o1, Leaf o2 | Arith o1, Arith o2 | Merge o1, Merge o2
- | Misalign_read o1, Misalign_read o2 ->
- LocationLattice.equal o1 o2
- | Misalign_read _, _ -> false
- | _, Misalign_read _ -> false
- | Leaf _, _ -> false
- | _, Leaf _ -> false
- | Merge _, _ -> false
- | _, Merge _ -> false
- | Arith _, _ -> false
- | _, Arith _ -> false
- | _, Well | Well, _ -> false
-
-let compare o1 o2 = match o1, o2 with
- | Misalign_read s1, Misalign_read s2
- | Leaf s1, Leaf s2
- | Merge s1, Merge s2
- | Arith s1, Arith s2 ->
- LocationLattice.compare s1 s2
-
- | Well, Well | Unknown, Unknown -> 0
-
- | Misalign_read _, (Leaf _ | Merge _ | Arith _ | Well | Unknown)
- | Leaf _, (Merge _ | Arith _ | Well | Unknown)
- | Merge _, (Arith _ | Well | Unknown)
- | Arith _, (Well | Unknown)
- | Well, Unknown ->
- -1
-
- | Unknown, (Well | Arith _ | Merge _ | Leaf _ | Misalign_read _)
- | Well, (Arith _ | Merge _ | Leaf _ | Misalign_read _)
- | Arith _, (Merge _ | Leaf _ | Misalign_read _)
- | Merge _, (Leaf _ | Misalign_read _)
- | Leaf _, Misalign_read _
- -> 1
-
-let top = Unknown
-let is_top x = equal top x
-
-
-let pretty_source fmt = function
- | LocationLattice.Top -> () (* Hide unhelpful 'TopSet' *)
- | LocationLattice.Value _ | LocationLattice.Bottom as s ->
- Format.fprintf fmt "@ %a" LocationLattice.pretty s
-
-let pretty fmt o = match o with
- | Unknown ->
- Format.fprintf fmt "Unknown"
- | Misalign_read o ->
- Format.fprintf fmt "Misaligned%a" pretty_source o
- | Leaf o ->
- Format.fprintf fmt "Library function%a" pretty_source o
- | Merge o ->
- Format.fprintf fmt "Merge%a" pretty_source o
- | Arith o ->
- Format.fprintf fmt "Arithmetic%a" pretty_source o
- | Well -> Format.fprintf fmt "Well"
+include Datatype.Make_with_collections (Prototype)
let pretty_as_reason fmt org =
- if not (is_top org) then
- Format.fprintf fmt " because of %a" pretty org
-
-
-let hash o = match o with
- | Misalign_read o ->
- 2001 + (LocationLattice.hash o)
- | Leaf o ->
- 2501 + (LocationLattice.hash o)
- | Merge o ->
- 3001 + (LocationLattice.hash o)
- | Arith o ->
- 3557 + (LocationLattice.hash o)
- | Well -> 17
- | Unknown -> 97
-
-include Datatype.Make
- (struct
- type t = origin
- let name = "Origin"
- let structural_descr = Structural_descr.t_unknown
- let reprs = [ Well; Unknown ]
- let compare = compare
- let equal = equal
- let hash = hash
- let rehash = Datatype.undefined
- let copy = Datatype.undefined
- let pretty = pretty
- let mem_project = Datatype.never_any_project
- end)
-
-let bottom = Arith LocationLattice.Bottom
+ if not (is_unknown org)
+ then Format.fprintf fmt " because of %a" pretty org
+
+let descr = function
+ | Unknown -> "unknown origin"
+ | Well -> "well in initial state"
+ | Origin { kind } ->
+ match kind with
+ | Misalign_read -> "misaligned read of addresses"
+ | Misalign_write -> "misaligned write of addresses"
+ | Leaf -> "assigns clause on addresses"
+ | Merge -> "imprecise merge of addresses"
+ | Arith -> "arithmetic operation on addresses"
+
+(* Keep the oldest known origin: it is probably the most relevant origin, as
+ subsequent ones may have been created because of the first. *)
+let join t1 t2 =
+ if t1 == t2 then t1 else
+ match t1, t2 with
+ | Unknown, x | x, Unknown -> x
+ | Well, _ | _, Well -> Well
+ | Origin o1, Origin o2 -> if o1.id <= o2.id then t1 else t2
+
+
+(* For each garbled mix origin, keep track of:
+ - the number of writes (according to [register_write] below), i.e. the number
+ of times a garbled mix with this origin has been written in a state during
+ the analysis.
+ - the number of reads (according to [register_read] below), i.e. the number
+ of times a garbled mix with this origin is used by the analysis.
+ Only reads at a different location than that of the origin are counted:
+ if a garbled mix is only used where it has been created, it has no more
+ impact on the analysis precision than any other imprecise value.
+ - the set of bases related to garbled mix with this origin.
+
+ These info are printed at the end of an Eva analysis. *)
+
+module History_Info = struct
+ let name = "Origin.History"
+ let dependencies = []
+ let size = 32
+end
-let join o1 o2 =
- let result =
- if o1 == o2
- then o1
- else
- match o1, o2 with
- | Unknown,_ | _, Unknown -> Unknown
- | Well,_ | _ , Well -> Well
- | Misalign_read o1, Misalign_read o2 ->
- Misalign_read(LocationLattice.join o1 o2)
- | _, (Misalign_read _ as m) | (Misalign_read _ as m), _ -> m
- | Leaf o1, Leaf o2 ->
- Leaf(LocationLattice.join o1 o2)
- | (Leaf _ as m), _ | _, (Leaf _ as m) -> m
- | Merge o1, Merge o2 ->
- Merge(LocationLattice.join o1 o2)
- | (Merge _ as m), _ | _, (Merge _ as m) -> m
- | Arith o1, Arith o2 ->
- Arith(LocationLattice.join o1 o2)
- (* | (Arith _ as m), _ | _, (Arith _ as m) -> m *)
+(* Number of writes, number of reads, related bases. *)
+module History_Data =
+ Datatype.Triple (Datatype.Int) (Datatype.Int) (Base.SetLattice)
+module History = State_builder.Hashtbl (Hashtbl) (History_Data) (History_Info)
+
+let clear () = Id.reset (); History.clear ()
+
+let is_current = function
+ | Unknown | Well -> false
+ | Origin { loc } -> Cil_datatype.Location.equal loc (Cil.CurrentLoc.get ())
+
+(* Returns true if the origin has never been registered and is related to the
+ current location. *)
+let register_write bases t =
+ if is_unknown t then false else
+ let change (w, r, b) = w+1, r, Base.SetLattice.join b bases in
+ let count, _, _ = History.memo ~change (fun _ -> 1, 0, bases) t in
+ count < 2 && is_current t
+
+(* Registers a read only if the current location is not that of the origin. *)
+let register_read bases t =
+ if not (is_unknown t || is_current t) then
+ let change (w, r, b) = w, r+1, Base.SetLattice.join b bases in
+ ignore (History.memo ~change (fun _ -> 0, 1, bases) t)
+
+(* Returns the list of recorded origins, sorted by number of reads.
+ Origins with no reads are filtered. *)
+let get_history () =
+ let list = List.of_seq (History.to_seq ()) in
+ let list = List.filter (fun (_origin, (_, r, _)) -> r > 0) list in
+ let cmp (origin1, (_, r1, _)) (origin2, (_, r2, _)) =
+ let r = r2 - r1 in
+ if r <> 0 then r else compare origin1 origin2
in
- (* Format.printf "Origin.join %a %a -> %a@." pretty o1 pretty o2 pretty result;
- *)
- result
-
-let link = join
-
-let meet o1 o2 =
- if o1 == o2
- then o1
- else
- match o1, o2 with
- | Arith o1, Arith o2 ->
- Arith(LocationLattice.meet o1 o2)
- | (Arith _ as m), _ | _, (Arith _ as m) -> m
- | Merge o1, Merge o2 ->
- Merge(LocationLattice.meet o1 o2)
- | (Merge _ as m), _ | _, (Merge _ as m) -> m
- | Leaf o1, Leaf o2 ->
- Leaf(LocationLattice.meet o1 o2)
- | (Leaf _ as m), _ | _, (Leaf _ as m) -> m
- | Misalign_read o1, Misalign_read o2 ->
- Misalign_read(LocationLattice.meet o1 o2)
- | _, (Misalign_read _ as m) | (Misalign_read _ as m), _ -> m
- | Well, Well -> Well
- | Well,m | m, Well -> m
- | Unknown, Unknown -> Unknown
-
-let narrow o1 o2 =
- if o1 == o2
- then o1
- else
- match o1, o2 with
- | Arith o1, Arith o2 -> Arith (LocationLattice.narrow o1 o2)
- | Merge o1, Merge o2 -> Merge (LocationLattice.narrow o1 o2)
- | Leaf o1, Leaf o2 -> Leaf (LocationLattice.narrow o1 o2)
- | Misalign_read o1, Misalign_read o2 ->
- Misalign_read (LocationLattice.narrow o1 o2)
- | Well, Well -> Well
- | Unknown, m | m, Unknown -> m
- | _, _ -> Unknown
-
-let is_included o1 o2 =
- (equal o1 (meet o1 o2))
-
+ List.sort cmp list
+
+let pretty_origin fmt origin =
+ match origin with
+ | Unknown -> Format.fprintf fmt "Unknown origin"
+ | Well -> Format.fprintf fmt "Initial state"
+ | Origin { loc } ->
+ Format.fprintf fmt "%a: %s"
+ Cil_datatype.Location.pretty loc (descr origin)
+
+let pretty_history fmt =
+ let list = get_history () in
+ let pp_origin fmt (origin, (w, r, bases)) =
+ let bases = Base.SetLattice.filter (fun b -> not (Base.is_null b)) bases in
+ Format.fprintf fmt
+ "@[<hov 2>%a@ (read %i times, propagated %i times)@ \
+ garbled mix of &%a@]"
+ pretty_origin origin r w Base.SetLattice.pretty bases
+ in
+ if list <> [] then
+ Format.fprintf fmt
+ "@[<v 2>Origins of garbled mix generated during analysis:@,%a@]"
+ (Pretty_utils.pp_list ~sep:"@," pp_origin) list
(*
Local Variables:
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index 4f6b0a4fa8f30e7216564041337bdc71afaf5303..bb8cdc57192bd5ebf3e2932f41bbb66f10f855ad 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/src/kernel_services/abstract_interp/origin.mli
@@ -20,57 +20,58 @@
(* *)
(**************************************************************************)
-(** The datastructures of this module can be used to track the origin
- of a major imprecision in the values of an abstract domain. *)
+(** This module is used to track the origin of very imprecise values
+ (namely "garbled mix", created on imprecise or unsupported operations on
+ addresses) propagated by an Eva analysis. *)
-(** This module is generic, although currently used only by the plugin Value.
- Within Value, values that have an imprecision origin are "garbled mix",
- ie. a numeric value that contains bits extracted from at least one
- pointer, and that are not the result of a translation *)
+include Datatype.S
+type kind =
+ | Misalign_read (* Misaligned read of addresses *)
+ | Misalign_write (* Misaligned write of addresses *)
+ | Leaf (* Interpretation of assigns clause *)
+ | Merge (* Imprecise merge of addresses *)
+ | Arith (* Arithmetic operation on addresses *)
-(** Lattice of source locations. *)
-module LocationLattice : Datatype.S
-
-(** List of possible origins. Most of them also include the set of
- source locations where the operation took place. *)
-type origin =
- | Misalign_read of LocationLattice.t (** Read of not all the bits of a
- pointer, typically through a pointer cast *)
- | Leaf of LocationLattice.t (** Result of a function without a body *)
- | Merge of LocationLattice.t (** Join between two control-flows *)
- | Arith of LocationLattice.t (** Arithmetic operation that cannot be
- represented, eg. ['&x * 2'] *)
- | Well (** Imprecise variables of the initial state *)
- | Unknown
+(** Creates an origin of the given kind, associated with the current source
+ location extracted from [Cil.CurrentLoc]. *)
+val current: kind -> t
-include Datatype.S with type t = origin
+(** Origin for garbled mix created in the initial state of the analysis
+ (not associated to a source location). *)
+val well: t
+(** Unknown origin. *)
+val unknown: t
+val is_unknown: t -> bool
-type kind =
- | K_Misalign_read
- | K_Leaf
- | K_Merge
- | K_Arith
+(** Pretty-print [because of <origin>] if the origin is not {!Unknown}, or
+ nothing otherwise. *)
+val pretty_as_reason: Format.formatter -> t -> unit
-val current: kind -> origin
-(** This is automatically extracted from [Cil.CurrentLoc] *)
+(** Short description of an origin. *)
+val descr: t -> string
-val pretty_as_reason: Format.formatter -> t -> unit
-(** Pretty-print [because of <origin>] if the origin is not {!Unknown}, or
- nothing otherwise *)
+val join: t -> t -> t
-val top: t
-val is_top: t -> bool
+(** Records the write of an imprecise value of the given bases,
+ with the given origin.
+ Returns [true] if the given origin has never been written before,
+ and if it is related to the current location — in which case a warning
+ should probably be emitted. *)
+val register_write: Base.SetLattice.t -> t -> bool
-val bottom: t
+(** Records the read of an imprecise value of the given bases,
+ with the given origin. *)
+val register_read: Base.SetLattice.t -> t -> unit
-val join: t -> t -> t
-val link: t -> t -> t
-val meet: t -> t -> t
-val narrow: t -> t -> t
+(** Pretty-print a summary of the origins of imprecise values recorded
+ by [register_write] and [register_read] above. *)
+val pretty_history: Format.formatter -> unit
-val is_included: t -> t -> bool
+(** Clears the history of origins saved by [register_write] and
+ [register_read] above. *)
+val clear: unit -> unit
(*
Local Variables:
diff --git a/src/kernel_services/abstract_interp/tr_offset.ml b/src/kernel_services/abstract_interp/tr_offset.ml
index 7df602f5d22549ba73b6b201ca00e887e9de23f9..4f4093907f48e38c81700e6a897d8803693f8b0c 100644
--- a/src/kernel_services/abstract_interp/tr_offset.ml
+++ b/src/kernel_services/abstract_interp/tr_offset.ml
@@ -26,7 +26,7 @@ type t =
| Invalid
| Set of Int.t list
| Interval of Int.t * Int.t * Int.t
- | Overlap of Int.t * Int.t * Origin.t
+ | Overlap of Int.t * Int.t * Origin.t option
let pretty fmt = function
| Invalid -> Format.fprintf fmt "Invalid"
@@ -35,7 +35,8 @@ let pretty fmt = function
| Interval (mn, mx, modu) -> Format.fprintf fmt "Interval (%a,%a,%a)"
Int.pretty mn Int.pretty mx Int.pretty modu
| Overlap (mn, mx, o) -> Format.fprintf fmt "Overlap (%a,%a,%a)"
- Int.pretty mn Int.pretty mx Origin.pretty o
+ Int.pretty mn Int.pretty mx
+ (Pretty_utils.pp_opt Origin.pretty) o
(* Reduces [ival] for an access according to [validity]. *)
let reduce_offset_by_validity origin ival size validity =
@@ -64,7 +65,7 @@ let reduce_offset_by_validity origin ival size validity =
| Base.Unknown (min, _, max) -> reduce_for_bounds min max
| Base.Variable v -> reduce_for_bounds Int.zero v.Base.max_alloc
-let trim_by_validity ?(origin=Origin.Unknown) ival size validity =
+let trim_by_validity ?origin ival size validity =
reduce_offset_by_validity origin ival size validity
(*
diff --git a/src/kernel_services/abstract_interp/tr_offset.mli b/src/kernel_services/abstract_interp/tr_offset.mli
index 7f72dff4878d09edeb5d9247d8bcb0c00ca7e652..8b16d56ebda0da7ba18a0b9a989766ce3741a419 100644
--- a/src/kernel_services/abstract_interp/tr_offset.mli
+++ b/src/kernel_services/abstract_interp/tr_offset.mli
@@ -29,10 +29,10 @@ type t = private
| Set of Integer.t list (** Limited number of locations *)
| Interval of Integer.t * Integer.t * Integer.t
(** [Interval(min, max, modulo)]*)
- | Overlap of Integer.t * Integer.t * Origin.t
- (**[Overlap(min, max, origin)]
- - [origin]: the location covers the entire range [min..max],
- but consecutive offsets overlap *)
+ | Overlap of Integer.t * Integer.t * Origin.t option
+ (** [Overlap(min, max, origin)]
+ - [origin]: the location covers the entire range [min..max],
+ but consecutive offsets overlap *)
val pretty: t Pretty_utils.formatter
diff --git a/src/libraries/project/state_builder.ml b/src/libraries/project/state_builder.ml
index 519505130bd580bf084dd7da1794cb95d391c33a..231dae0d4a6f80b181125d185a98c0fdcafb40be 100644
--- a/src/libraries/project/state_builder.ml
+++ b/src/libraries/project/state_builder.ml
@@ -814,6 +814,7 @@ module Hashconsing_tbl =
module type Counter = sig
val next : unit -> int
val get: unit -> int
+ val reset: unit -> unit
val self: State.t
end
@@ -849,6 +850,7 @@ module SharedCounter(Info : sig val name : string end) = struct
let next () = incr cpt ; !cpt
let get () = !cpt
+ let reset () = cpt := 0
let self = Cpt.self
end
@@ -886,6 +888,7 @@ module Counter(Info : sig val name : string end) = struct
let next () = incr !cpt ; !(!cpt)
let get () = !(!cpt)
+ let reset () = !cpt := 0
let self = Cpt.self
end
diff --git a/src/libraries/project/state_builder.mli b/src/libraries/project/state_builder.mli
index f4770180a8efd00c05ccd310951dc0f511cde48d..10bbb9e968622ebbe64792f4f2c0d4ad083688c9 100644
--- a/src/libraries/project/state_builder.mli
+++ b/src/libraries/project/state_builder.mli
@@ -507,6 +507,10 @@ module type Counter = sig
(** @return the current value of the counter, without incrementing it.
@since Fluorine-20130401 *)
+ (** Resets the counter to 0.
+ @since Frama-C+dev *)
+ val reset: unit -> unit
+
val self: State.t
(** @since Oxygen-20120901 *)
diff --git a/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle b/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
index 7cfe3e4ea5cf0dc4afe4fc3594f5fc056a737886..ae50bf359dc8ec7fdd730f6d2635af6d25ce7453 100644
--- a/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
+++ b/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
@@ -1,14 +1,8 @@
[kernel] Parsing exceptional.i (no preprocessing)
[eva] Analyzing a complete application starting at main
[eva:garbled-mix:write] exceptional.i:5:
- Assigning imprecise value to __retres.
- The imprecision originates from Arithmetic {exceptional.i:5}
-[eva:garbled-mix:write] exceptional.i:5:
- Assigning imprecise value to \result<gm>.
- The imprecision originates from Arithmetic {exceptional.i:5}
-[eva:garbled-mix:write] exceptional.i:16:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {exceptional.i:5}
+ Assigning imprecise value to __retres
+ because of arithmetic operation on addresses.
[eva:alarm] exceptional.i:17: Warning:
accessing uninitialized left-value. assert \initialized(p);
[eva:alarm] exceptional.i:17: Warning:
@@ -19,6 +13,10 @@
signed overflow. assert a + x ≤ 2147483647;
[eva:alarm] exceptional.i:23: Warning:
signed overflow. assert (int)(a + x) + (int)c ≤ 2147483647;
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ exceptional.i:5: arithmetic operation on addresses
+ (read 3 times, propagated 3 times) garbled mix of &{i}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
2 functions analyzed (out of 2): 100% coverage.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
index 44a3cdfd58d00b48dd99a2a3a393754880497e23..201d2b2a599aa089c5debb92d71b0fd2e6d33d98 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
@@ -18,6 +18,9 @@
[eva] using specification for function __e_acsl_full_init
[eva] using specification for function __e_acsl_valid
[eva] using specification for function __e_acsl_assert_register_ptr
+[eva:garbled-mix:assigns] issue-eacsl-145.c:9:
+ The specification of function __e_acsl_assert_register_ptr
+ has generated a garbled mix of addresses for assigns clause data->values.
[eva] using specification for function __e_acsl_assert_register_ulong
[eva:alarm] issue-eacsl-145.c:9: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
diff --git a/src/plugins/eva/domains/cvalue/builtins.ml b/src/plugins/eva/domains/cvalue/builtins.ml
index 4dc7cb838a7542869c60076fb8ea28dc82287eb3..b128b35eed8387cf041c595f1438392a8f0bc3e9 100644
--- a/src/plugins/eva/domains/cvalue/builtins.ml
+++ b/src/plugins/eva/domains/cvalue/builtins.ml
@@ -252,6 +252,8 @@ let process_result call state call_result =
| Some value, Some vi_ret ->
let b_ret = Base.of_varinfo vi_ret in
let offsm = Eval_op.offsetmap_of_v ~typ:vi_ret.vtype value in
+ let prefix = "Builtin " ^ Kernel_function.get_name call.kf in
+ Cvalue_transfer.warn_imprecise_offsm_write ~prefix (Cil.var vi_ret) offsm;
Cvalue.Model.add_base b_ret offsm state, clob
| _, _ -> state, clob (* TODO: error? *)
in
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index 9cfa63a0dc9bdeb2a69c7f92614b36e039790f2f..073fc79acf09987e1fd82a7623e58bd1257f3e97 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -30,6 +30,12 @@ let register_builtin name ?replace builtin =
let dkey = Self.register_category "imprecision"
+let rec lval_of_address exp =
+ match exp.enode with
+ | AddrOf lval -> lval
+ | CastE (_typ, exp) -> lval_of_address exp
+ | _ -> Cil.mkMem ~addr:exp ~off:Cil_types.NoOffset
+
let frama_C_is_base_aligned _state = function
| [_, x; _, y] ->
let result =
@@ -99,8 +105,10 @@ let deps_nth_arg n =
with Failure _ -> Kernel.fatal "%d arguments expected" n
-let frama_c_memcpy state actuals =
- let compute (_exp_dst,dst_bytes) (_exp_src,src_bytes) (_exp_size,size) =
+let frama_c_memcpy name state actuals =
+ let prefix = "Builtin " ^ name in
+ let compute (exp_dst,dst_bytes) (_exp_src,src_bytes) (_exp_size,size) =
+ let dst_lval = lval_of_address exp_dst in
let plevel = Parameters.ArrayPrecisionLevel.get() in
let size =
try Cvalue.V.project_ival size
@@ -132,6 +140,7 @@ let frama_c_memcpy state actuals =
memcpy_check_indeterminate_offsetmap offsetmap;
(* Read succeeded. We write the result *)
let loc_src = make_loc src (Int_Base.inject size_min) in
+ Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval offsetmap;
let new_state =
Cvalue.Model.paste_offsetmap
~from:offsetmap ~dst_loc:dst_bits ~size:size_min ~exact:true state
@@ -212,6 +221,7 @@ let frama_c_memcpy state actuals =
raise (Memcpy_result (state,c_from,sure_zone))
| `Value offsetmap ->
memcpy_check_indeterminate_offsetmap offsetmap;
+ Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval offsetmap;
let new_state =
Cvalue.Model.paste_offsetmap
~from:offsetmap ~dst_loc:dst ~size:diff ~exact:false state
@@ -247,6 +257,8 @@ let frama_c_memcpy state actuals =
"@[In memcpy@ builtin:@ imprecise@ copy of@ indeterminate@ values@]%t"
Eva_utils.pp_callstack
end;
+ let value = Cvalue.V_Or_Uninitialized.get_v v in
+ Cvalue_transfer.warn_imprecise_write ~prefix dst_lval loc_dst value;
let updated_state =
Cvalue.Model.add_indeterminate_binding
~exact:false new_state loc_dst v
@@ -287,11 +299,13 @@ let frama_c_memcpy state actuals =
| [dst; src; size] -> compute dst src size
| _ -> raise (Builtins.Invalid_nb_of_args 3)
-let () = register_builtin ~replace:"memcpy" "Frama_C_memcpy" frama_c_memcpy
-let () = register_builtin ~replace:"memmove" "Frama_C_memmove" frama_c_memcpy
+let () =
+ register_builtin ~replace:"memcpy" "Frama_C_memcpy" (frama_c_memcpy "memcpy");
+ register_builtin ~replace:"memmove" "Frama_C_memmove" (frama_c_memcpy "memmove")
(* Implementation of [memset] that accepts imprecise arguments. *)
-let frama_c_memset_imprecise state dst v size =
+let frama_c_memset_imprecise state dst_lval dst v size =
+ let prefix = "Builtin memset" in
let size_char = Bit_utils.sizeofchar () in
let size_min, size_max_bytes =
try
@@ -317,6 +331,7 @@ let frama_c_memset_imprecise state dst v size =
let loc = Location_Bytes.shift shift dst in
let loc = loc_bytes_to_loc_bits loc in
let loc = make_loc loc (Int_Base.inject size_char) in
+ Cvalue_transfer.warn_imprecise_write ~prefix dst_lval loc v;
let state = Cvalue.Model.add_binding ~exact:false state loc v in
(state,enumerate_valid_bits Locations.Write loc)
else (state,Zone.bottom)
@@ -335,6 +350,7 @@ let frama_c_memset_imprecise state dst v size =
let left' = Location_Bits.inject base (Ival.inject_singleton maxb) in
let vuninit = V_Or_Uninitialized.initialized v in
let from = V_Offsetmap.create ~size:sure vuninit ~size_v:size_char in
+ Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval from;
let state =
Cvalue.Model.paste_offsetmap
~from ~dst_loc:left' ~size:sure ~exact:true new_state
@@ -521,7 +537,7 @@ let memset_typ_offsm typ v =
(* Precise memset builtin, that requires its arguments to be sufficiently
precise abstract values. *)
-let frama_c_memset_precise state dst v (exp_size, size) =
+let frama_c_memset_precise state dst_lval dst v (exp_size, size) =
try
let size_char = Bit_utils.sizeofchar () in
(* We want an exact size, Otherwise, we can use the imprecise memset as a
@@ -571,6 +587,8 @@ let frama_c_memset_precise state dst v (exp_size, size) =
c_from,dst_zone
in
let _ = c_from in
+ let prefix = "Builtin memset" in
+ Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval offsm;
let state' =
Cvalue.Model.paste_offsetmap
~from:offsm ~dst_loc ~size:size_bits ~exact:true state
@@ -590,24 +608,25 @@ let frama_c_memset_precise state dst v (exp_size, size) =
let frama_c_memset state actuals =
match actuals with
- | [(_exp_dst, dst); (_, v); (exp_size, size)] ->
+ | [(exp_dst, dst); (_, v); (exp_size, size)] ->
begin
+ let dst_lval = lval_of_address exp_dst in
(* Remove read-only destinations *)
let dst = V.filter_base (fun b -> not (Base.is_read_only b)) dst in
(* Keep only the first byte of the value argument *)
let _, v = Cvalue.V.extract_bits
- ~topify:Origin.K_Misalign_read
+ ~topify:Origin.Misalign_read
~start:Int.zero ~stop:(Int.pred (Bit_utils.sizeofchar ()))
~size:(Int.of_int (Cil.bitsSizeOfInt IInt))
v
in
- try frama_c_memset_precise state dst v (exp_size, size)
+ try frama_c_memset_precise state dst_lval dst v (exp_size, size)
with ImpreciseMemset reason ->
Self.debug ~dkey ~current:true
"Call to builtin precise_memset(%a) failed; %a%t"
Eva_utils.pretty_actuals actuals pretty_imprecise_memset_reason reason
Eva_utils.pp_callstack;
- frama_c_memset_imprecise state dst v size
+ frama_c_memset_imprecise state dst_lval dst v size
end
| _ -> raise (Builtins.Invalid_nb_of_args 3)
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 28d8274aa83aa006de84c4838b1a4092b345c800..43b19bd42586c0c09577be32dd4c1aefe5958e90 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -148,6 +148,15 @@ module State = struct
finalize_recursive_call stmt call ~pre:(pre, clob) a post
in
let post = Option.fold ~some:finalize ~none:post recursion in
+ (* Deallocate memory allocated via alloca().
+ To minimize computations, only do it for function definitions. *)
+ let post =
+ if Kernel_function.is_definition call.kf then
+ let callstack = Eva_utils.current_call_stack () in
+ let callstack = Callstack.push call.kf stmt callstack in
+ Builtins_malloc.free_automatic_bases callstack post
+ else post
+ in
Cvalue_transfer.finalize_call stmt call recursion ~pre ~post
>>-: fun state ->
state, clob
diff --git a/src/plugins/eva/domains/cvalue/cvalue_init.ml b/src/plugins/eva/domains/cvalue/cvalue_init.ml
index d6b5fc4dc83b90f048cd6dbc2be85148db3168b4..a606eac714e321bfa78df6709fd39685665b7439 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_init.ml
@@ -33,7 +33,7 @@ let add_initialized state loc v =
let make_well hidden_base state loc =
let size = Bit_utils.max_bit_size () in
let well =
- Cvalue.V.inject_top_origin Origin.Well (Base.Hptset.singleton hidden_base)
+ Cvalue.V.inject_top_origin Origin.well (Base.Hptset.singleton hidden_base)
in
let well_loc =
Locations.make_loc
diff --git a/src/plugins/eva/domains/cvalue/cvalue_offsetmap.ml b/src/plugins/eva/domains/cvalue/cvalue_offsetmap.ml
index b025905db610ec025920ff50613359a8e74d733d..b2d0019e28ae7a67b2e5a6e58ccda40dd182d66f 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_offsetmap.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_offsetmap.ml
@@ -22,35 +22,6 @@
open Eval
-exception Got_imprecise of Cvalue.V.t
-let offsetmap_contains_imprecision offs =
- try
- Cvalue.V_Offsetmap.iter_on_values
- (fun v ->
- match Cvalue.V_Or_Uninitialized.get_v v with
- | Locations.Location_Bytes.Map _ -> ()
- | Locations.Location_Bytes.Top _ as v -> raise (Got_imprecise v)
- ) offs;
- None
- with Got_imprecise v -> Some v
-
-let warn_right_imprecision lval loc offsetmap =
- match offsetmap_contains_imprecision offsetmap with
- | Some v -> Warn.warn_right_exp_imprecision lval loc v
- | None -> ()
-
-let warn_if_imprecise lval loc offsm =
- match offsetmap_contains_imprecision offsm with
- | Some v ->
- let loc = Precise_locs.imprecise_location loc in
- Warn.warn_imprecise_lval_read lval loc v
- | None -> ()
-
-let offsetmap_of_lval state lval loc =
- let offsm = Bottom.non_bottom (Eval_op.offsetmap_of_loc loc state) in
- warn_if_imprecise lval loc offsm;
- offsm
-
let offsetmap_of_v ~typ v =
let size = Integer.of_int (Cil.bitsSizeOf typ) in
let v = Cvalue.V.anisotropic_cast ~size v in
@@ -58,5 +29,7 @@ let offsetmap_of_v ~typ v =
Cvalue.V_Offsetmap.create ~size v ~size_v:size
let offsetmap_of_assignment state expr = function
- | Copy (lv, _value) -> offsetmap_of_lval state lv.lval lv.lloc
- | Assign value -> offsetmap_of_v ~typ:(Cil.typeOf expr) value
+ | Copy (lv, _value) ->
+ Bottom.non_bottom (Eval_op.offsetmap_of_loc lv.lloc state)
+ | Assign value ->
+ offsetmap_of_v ~typ:(Cil.typeOf expr) value
diff --git a/src/plugins/eva/domains/cvalue/cvalue_offsetmap.mli b/src/plugins/eva/domains/cvalue/cvalue_offsetmap.mli
index 8d6903e821611855a4ff6831055b57186dda3434..8e0119621709ef78e080b02d5a3af3a896e8e94f 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_offsetmap.mli
+++ b/src/plugins/eva/domains/cvalue/cvalue_offsetmap.mli
@@ -25,18 +25,6 @@
open Cil_types
open Cvalue
-(** [warn_right_imprecision lval loc offsm] is used for the assignment of the
- lvalue [lval] pointing to the location [loc]; it warns if the offsetmap
- [offsm] contains a garbled mix. *)
-val warn_right_imprecision:
- lval -> Locations.location -> V_Offsetmap.t -> unit
-
-(** [offsetmap_of_lval state lval loc] extracts from state [state] the offsetmap
- at location [loc], corresponding to the lvalue [lval]. Warns if this
- offsetmap contains a garbled mix. *)
-val offsetmap_of_lval:
- Model.t -> lval -> Precise_locs.precise_location -> V_Offsetmap.t
-
(** Computes the offsetmap for an assignment:
- in case of a copy, extracts the offsetmap from the state;
- otherwise, translates the value assigned into an offsetmap. *)
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
index ae31230b0e8ede332ce8a485e99431acb7c51d83..a39492a45942563e4e8cdaaa3368a8812ff5480f 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_queries.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
@@ -76,6 +76,10 @@ module Queries = struct
let is_float v =
Cvalue.V.(is_included v top_float) && Cvalue.V.contains_non_zero v
+ let read_garbled_mix = function
+ | Cvalue.V.Top (bases, origin) -> Origin.register_read bases origin
+ | _ -> ()
+
let extract_scalar_lval state lval typ loc =
let process_one_loc = eval_one_loc state lval typ in
let acc = Cvalue.V.bottom, None in
@@ -88,6 +92,7 @@ module Queries = struct
let incompatible_type = is_float value <> Cil.isFloatingType typ in
let origin = if incompatible_type then Some value else None in
let value = Cvalue_forward.reinterpret typ value in
+ read_garbled_mix value;
if Cvalue.V.is_bottom value
then `Bottom, alarms
else `Value (value, origin), alarms
@@ -106,6 +111,7 @@ module Queries = struct
let value = Cvalue.V_Offsetmap.find_imprecise_everywhere offsm in
let alarms = indeterminate_alarms lval value in
let v = Cvalue.V_Or_Uninitialized.get_v value in
+ read_garbled_mix v;
let v = if Cvalue.V.is_bottom v then `Bottom else `Value (v, None) in
v, alarms
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
index 007674371f657ba8bdca117a649689e86287b3be..bbe73b8013d315befd32c8bdf48195e8a6a8ce61 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
@@ -22,7 +22,6 @@
open Cil_types
open Eval
-open Cvalue.Model
type value = Main_values.CVal.t
type origin = value
@@ -32,6 +31,40 @@ let unbottomize = function
| `Bottom -> Cvalue.V.bottom
| `Value v -> v
+(* ---------------------------------------------------------------------- *)
+(* Garbled mix warnings *)
+(* ---------------------------------------------------------------------- *)
+
+let warn_imprecise_value ?prefix lval value =
+ match value with
+ | Locations.Location_Bytes.Top (bases, origin) ->
+ if Origin.register_write bases origin then
+ let prefix = Option.fold ~none:"A" ~some:(fun s -> s ^ ": a") prefix in
+ Self.warning ~wkey:Self.wkey_garbled_mix_write ~once:true ~current:true
+ "@[%sssigning imprecise value to %a@ because of %s.@]%t"
+ prefix Printer.pp_lval lval (Origin.descr origin)
+ Eva_utils.pp_callstack
+ | _ -> ()
+
+let warn_imprecise_location ?prefix loc =
+ match loc.Locations.loc with
+ | Locations.Location_Bits.Top (Base.SetLattice.Top, orig) ->
+ let prefix = Option.fold ~none:"" ~some:(fun s -> s ^ ": ") prefix in
+ Self.fatal ~current:true
+ "@[%swriting at a completely unknown address@ because of %s.@]@\nAborting."
+ prefix (Origin.descr orig)
+ | _ -> ()
+
+let warn_imprecise_write ?prefix lval loc value =
+ warn_imprecise_location ?prefix loc;
+ warn_imprecise_value ?prefix lval value
+
+let warn_imprecise_offsm_write ?prefix lval offsm =
+ let warn value =
+ warn_imprecise_value ?prefix lval (Cvalue.V_Or_Uninitialized.get_v value)
+ in
+ Cvalue.V_Offsetmap.iter_on_values warn offsm
+
(* ---------------------------------------------------------------------- *)
(* Assumptions *)
(* ---------------------------------------------------------------------- *)
@@ -45,7 +78,7 @@ let reduce valuation lval value t =
| `Value record ->
let loc = Precise_locs.imprecise_location record.loc in
if Locations.cardinal_zero_or_one loc
- then reduce_indeterminate_binding t loc value
+ then Cvalue.Model.reduce_indeterminate_binding t loc value
else t
| `Top -> t (* Cannot reduce without the location of the lvalue. *)
@@ -90,38 +123,26 @@ let update valuation t =
let write_abstract_value state (lval, loc, typ) assigned_value =
let {v; initialized; escaping} = assigned_value in
let value = unbottomize v in
- Warn.warn_right_exp_imprecision lval loc value;
let value =
if Cil.typeHasQualifier "volatile" typ
then Cvalue_forward.make_volatile value
else value
in
- match loc.Locations.loc with
- | Locations.Location_Bits.Top (Base.SetLattice.Top, orig) ->
- Self.result
- "State before degeneration:@\n======%a@\n======="
- Cvalue.Model.pretty state;
- Self.fatal ~current:true
- "writing at a completely unknown address@[%a@].@\nAborting."
- Origin.pretty_as_reason orig
- | _ ->
- let exact = Locations.cardinal_zero_or_one loc in
- let value =
- Cvalue.V_Or_Uninitialized.make ~initialized ~escaping value in
- (* let value = Cvalue.V_Or_Uninitialized.initialized value in *)
- add_indeterminate_binding ~exact state loc value
+ warn_imprecise_write lval loc value;
+ let exact = Locations.cardinal_zero_or_one loc in
+ let value = Cvalue.V_Or_Uninitialized.make ~initialized ~escaping value in
+ Cvalue.Model.add_indeterminate_binding ~exact state loc value;
exception Do_assign_imprecise_copy
let copy_one_loc state left_lv right_lv =
let left_lval, left_loc, left_typ = left_lv
- and right_lval, right_loc, right_typ = right_lv in
- (* Warn if right_loc is imprecise *)
- Warn.warn_imprecise_lval_read right_lval right_loc Cvalue.V.bottom;
+ and _right_lval, right_loc, right_typ = right_lv in
(* top size is tested before this function is called, in which case
the imprecise copy mode is used. *)
let size = Int_Base.project right_loc.Locations.size in
- let offsetmap = copy_offsetmap right_loc.Locations.loc size state in
+ let right_loc = right_loc.Locations.loc in
+ let offsetmap = Cvalue.Model.copy_offsetmap right_loc size state in
let make_volatile =
Cil.typeHasQualifier "volatile" left_typ ||
Cil.typeHasQualifier "volatile" right_typ
@@ -139,9 +160,9 @@ let copy_one_loc state left_lv right_lv =
in
if not (Eval_typ.offsetmap_matches_type left_typ offsetmap) then
raise Do_assign_imprecise_copy;
- Cvalue_offsetmap.warn_right_imprecision left_lval left_loc offsetmap;
+ warn_imprecise_offsm_write left_lval offsetmap;
`Value
- (paste_offsetmap ~exact:true
+ (Cvalue.Model.paste_offsetmap ~exact:true
~from:offsetmap ~dst_loc:left_loc.Locations.loc ~size state)
let make_determinate value =
@@ -164,9 +185,9 @@ let copy_right_lval state left_lv right_lv copied_value =
and right_lv = right_lv.lval, right_loc, right_lv.ltyp in
match copy_one_loc state left_lv right_lv with
| `Bottom -> acc
- | `Value state -> join acc state
+ | `Value state -> Cvalue.Model.join acc state
in
- Precise_locs.fold process right_lv.lloc bottom
+ Precise_locs.fold process right_lv.lloc Cvalue.Model.bottom
with
Do_assign_imprecise_copy ->
write_abstract_value state (lval, loc, typ) copied_value
@@ -183,10 +204,10 @@ let assign _stmt { lval; ltyp; lloc } _expr assigned valuation state =
in
let aux_loc loc acc_state =
let s = assign_one_loc loc in
- join acc_state s
+ Cvalue.Model.join acc_state s
in
- let state = Precise_locs.fold aux_loc lloc bottom in
- if not (is_reachable state)
+ let state = Precise_locs.fold aux_loc lloc Cvalue.Model.bottom in
+ if not (Cvalue.Model.is_reachable state)
then `Bottom
else `Value state
@@ -199,6 +220,7 @@ let actualize_formals state arguments =
let offsm =
Cvalue_offsetmap.offsetmap_of_assignment state arg.concrete arg.avalue
in
+ warn_imprecise_offsm_write (Cil.var arg.formal) offsm;
Cvalue.Model.add_base (Base.of_varinfo arg.formal) offsm state
in
List.fold_left treat_one_formal state arguments
@@ -206,26 +228,17 @@ let actualize_formals state arguments =
let start_call _stmt call _recursion _valuation state =
`Value (actualize_formals state call.arguments)
-let finalize_call stmt call _recursion ~pre:_ ~post:state =
- (* Deallocate memory allocated via alloca().
- To minimize computations, only do it for function definitions. *)
- let state' =
- if Kernel_function.is_definition call.kf then
- let callstack = Eva_utils.current_call_stack () in
- let callstack = Callstack.push call.kf stmt callstack in
- Builtins_malloc.free_automatic_bases callstack state
- else state
- in
- `Value state'
+let finalize_call _stmt _call _recursion ~pre:_ ~post:state =
+ `Value state
let show_expr valuation state fmt expr =
match expr.enode with
| Lval lval | StartOf lval ->
- let record = match valuation.Abstract_domain.find_loc lval with
- | `Value record -> record
+ let loc = match valuation.Abstract_domain.find_loc lval with
+ | `Value record -> record.loc
| `Top -> assert false
in
- let offsm = Cvalue_offsetmap.offsetmap_of_lval state lval record.loc in
+ let offsm = Bottom.non_bottom (Eval_op.offsetmap_of_loc loc state) in
let typ = Cil.typeOfLval lval in
Eval_op.pretty_offsetmap typ fmt offsm
| _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.mli b/src/plugins/eva/domains/cvalue/cvalue_transfer.mli
index 5b01daee42dfc4630b86ce8ba5fd76ca38c8b8e8..0b16f6a3034fcd4378805815ffe1644c711e8dde 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.mli
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.mli
@@ -32,6 +32,18 @@ include Abstract_domain.Transfer
and type location := location
and type origin := origin
+(** [warn_imprecise_write lval loc v] emits a warning about the assignment of
+ value [v] into location [loc] if one of them is overly imprecise. [lval] is
+ the assigned lvalue, and [prefix] is an optional prefix to the warning. *)
+val warn_imprecise_write:
+ ?prefix:string -> Cil_types.lval -> Locations.location -> Cvalue.V.t -> unit
+
+(** [warn_imprecise_offsm_write lval offsm] emits a warning about the assignment
+ of offsetmap [offsm] if it contains an overly imprecise value. [lval] is the
+ assigned lvalue, and [prefix] is an optional prefix to the warning. *)
+val warn_imprecise_offsm_write:
+ ?prefix:string -> Cil_types.lval -> Cvalue.V_Offsetmap.t -> unit
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/eva/domains/cvalue/locals_scoping.ml b/src/plugins/eva/domains/cvalue/locals_scoping.ml
index 2e263ae8d1f369514c6351153e9628b3e8b0bc62..afd70681b564287638238667bde0e910b012714f 100644
--- a/src/plugins/eva/domains/cvalue/locals_scoping.ml
+++ b/src/plugins/eva/domains/cvalue/locals_scoping.ml
@@ -54,6 +54,17 @@ let offsetmap_contains_local offm =
with Exit -> true
+let warn_locals_escape is_block fundec k locals =
+ let pretty_base = Base.pretty in
+ let pretty_block fmt = Pretty_utils.pp_cond is_block fmt "a block of " in
+ let sv = fundec.svar in
+ Self.warning
+ ~wkey:Self.wkey_locals_escaping
+ ~current:true ~once:true
+ "locals %a escaping the scope of %t%a through %a"
+ Base.Hptset.pretty locals pretty_block Printer.pp_varinfo sv pretty_base k
+
+
(* Rebuild [offsm] by applying [f] to the bindings that verify [test].
Also call [warn] in this case. *)
let rebuild_offsetmap f warn offsm =
@@ -123,7 +134,7 @@ let make_escaping_fundec fundec clob vars state =
| Base.SetLattice.Top -> escaping
| Base.SetLattice.Set bases -> Base.Hptset.inter bases escaping
in
- Warn.warn_locals_escape is_inner_block fundec b bases
+ warn_locals_escape is_inner_block fundec b bases
in
make_escaping ~exact:true ~escaping ~on_escaping ~within:clob.clob state
diff --git a/src/plugins/eva/domains/cvalue/warn.ml b/src/plugins/eva/domains/cvalue/warn.ml
deleted file mode 100644
index 3604d914973d55ba0cf412c4b6aee1436ec81f32..0000000000000000000000000000000000000000
--- a/src/plugins/eva/domains/cvalue/warn.ml
+++ /dev/null
@@ -1,125 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-open Locations
-
-let warn_locals_escape is_block fundec k locals =
- let pretty_base = Base.pretty in
- let pretty_block fmt = Pretty_utils.pp_cond is_block fmt "a block of " in
- let sv = fundec.svar in
- Self.warning
- ~wkey:Self.wkey_locals_escaping
- ~current:true ~once:true
- "locals %a escaping the scope of %t%a through %a"
- Base.Hptset.pretty locals pretty_block Printer.pp_varinfo sv pretty_base k
-
-let warn_imprecise_lval_read lv loc contents =
- if Self.verbose_atleast 1 then
- let pretty_gm fmt s =
- let s = Base.SetLattice.(inject (O.remove Base.null s)) in
- Base.SetLattice.pretty fmt s
- in
- let pretty_param fmt param =
- match param with
- | Base.SetLattice.Top -> Format.fprintf fmt "is imprecise"
- | Base.SetLattice.Set s ->
- Format.fprintf fmt "is a garbled mix of %a" pretty_gm s
- in
- let pretty_param_b fmt param =
- match param with
- | Base.SetLattice.Top ->
- Format.fprintf fmt "The contents@ are imprecise"
- | Base.SetLattice.Set s ->
- Format.fprintf fmt "It contains@ a garbled@ mix@ of@ %a" pretty_gm s
- in
- let something_to_warn =
- match loc.loc with
- | Location_Bits.Top _ -> true
- | Location_Bits.Map _ ->
- match contents with
- | Location_Bytes.Top _ -> true
- | Location_Bytes.Map _ -> false
- in
- if something_to_warn
- then
- Self.warning ~wkey:Self.wkey_garbled_mix_read ~current:true ~once:true
- "@[<v>@[Reading left-value %a.@]@ %t%t%t@]"
- Printer.pp_lval lv
- (fun fmt ->
- match loc.loc with
- | Location_Bits.Top (param,o) when Origin.equal o Origin.top ->
- Format.fprintf fmt "@[The location %a.@]@ "
- pretty_param param
- | Location_Bits.Top (param,orig) ->
- Format.fprintf fmt "@[The location @[%a@]@ because of@ %a.@]@ "
- pretty_param param
- Origin.pretty orig
- | Location_Bits.Map _ ->
- match lv with
- | Mem _, _ ->
- Format.fprintf fmt "@[The location is @[%a@].@]@ "
- Location_Bits.pretty loc.loc
- | Var _, _ -> ()
- )
- (fun fmt ->
- match contents with
- | Location_Bytes.Top (param,o) when Origin.equal o Origin.top ->
- Format.fprintf fmt "@[%a.@]"
- pretty_param_b param
- | Location_Bytes.Top (param,orig) ->
- Format.fprintf fmt "@[%a@ because of@ %a.@]"
- pretty_param_b param
- Origin.pretty orig
- | Location_Bytes.Map _ -> ())
- Eva_utils.pp_callstack
-
-(* Auxiliary function for [do_assign] below. When computing the
- result of [lv = exp], warn if the evaluation of [exp] results in
- an imprecision. [loc_lv] is the location pointed to by [lv].
- [exp_val] is the part of the evaluation of [exp] that is imprecise. *)
-let warn_right_exp_imprecision lv loc_lv exp_val =
- match exp_val with
- | Location_Bytes.Top(_topparam,origin) ->
- Self.warning ~wkey:Self.wkey_garbled_mix_write ~once:true ~current:true
- "@[<v>@[Assigning imprecise value to %a%t.@]%a%t@]"
- Printer.pp_lval lv
- (fun fmt -> match lv with
- | (Mem _, _) ->
- Format.fprintf fmt "@ (pointing to %a)"
- (Locations.pretty_english ~prefix:false) loc_lv
- | (Var _, _) -> ())
- (fun fmt org ->
- if not (Origin.is_top origin) then
- Format.fprintf fmt
- "@ @[The imprecision@ originates@ from@ %a@]"
- Origin.pretty org)
- origin
- Eva_utils.pp_callstack
- | Location_Bytes.Map _ -> ()
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../../.."
-End:
-*)
diff --git a/src/plugins/eva/domains/cvalue/warn.mli b/src/plugins/eva/domains/cvalue/warn.mli
deleted file mode 100644
index 2c9664ff6b7d31dbfdb591aed7230ff3788a8247..0000000000000000000000000000000000000000
--- a/src/plugins/eva/domains/cvalue/warn.mli
+++ /dev/null
@@ -1,30 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(** Alarms and imprecision warnings emitted during the analysis. *)
-
-open Cil_types
-open Locations
-
-val warn_locals_escape: bool -> fundec -> Base.t -> Base.Hptset.t -> unit
-val warn_imprecise_lval_read: lval -> location -> Location_Bytes.t -> unit
-val warn_right_exp_imprecision: lval -> location -> Cvalue.V.t -> unit
diff --git a/src/plugins/eva/domains/equality/equality_domain.ml b/src/plugins/eva/domains/equality/equality_domain.ml
index 9c7407b2d0138c580d74b96b56252074168718ea..55affa63dc9a97b8759e9139264972c7e574d5c2 100644
--- a/src/plugins/eva/domains/equality/equality_domain.ml
+++ b/src/plugins/eva/domains/equality/equality_domain.ml
@@ -212,7 +212,7 @@ module Make
fun v ->
let c = get v in
if Cvalue.V.is_imprecise c then
- let c' = Cvalue.V.topify_with_origin Origin.top c in
+ let c' = Cvalue.V.topify_with_origin Origin.unknown c in
Value.set Main_values.CVal.key c' v
else v
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index d721e62e638a22343470bb3815108b0e92ad2ec0..c5606b0ebeb8571025778bb05ca5f1fb8434c374 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -75,12 +75,12 @@ struct
let of_bit ~typ:_ = function
| Abstract_memory.Uninitialized -> uninitialized
| Zero i -> make i (V.inject_int Integer.zero)
- | Any (Top, i) -> make i (V.top_with_origin Origin.top)
+ | Any (Top, i) -> make i (V.top_with_origin Origin.unknown)
| Any (Set s, i) ->
let v =
if Base.Hptset.is_empty s
then V.inject_ival Ival.top
- else V.inject_top_origin Origin.top s
+ else V.inject_top_origin Origin.unknown s
in
make i v
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 09a3b4d353b06d83d8a5a5c13396a4b28c90765f..88b6280b2e75a83b72bf2a90b23921754ba17269 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -101,7 +101,7 @@ let pre_analysis () =
(* We may be resuming Value from a previously crashed analysis. Clear
degeneration states *)
Eva_utils.DegenerationPoints.clear ();
- Cvalue.V.clear_garbled_mix ();
+ Origin.clear ();
Eva_utils.clear_call_stack ()
let post_analysis_cleanup ~aborted =
@@ -114,7 +114,7 @@ let post_analysis () =
(* Garbled mix must be dumped here -- at least before the call to
mark_green_and_red -- because fresh ones are created when re-evaluating
all the alarms, and we get an unpleasant "ghost effect". *)
- Eva_utils.dump_garbled_mix ();
+ Self.warning ~wkey:Self.wkey_garbled_mix_summary "%t" Origin.pretty_history;
(* Mark unreachable and RTE statuses. Only do this there, not when the
analysis was aborted (hence, not in post_cleanup), because the
propagation is incomplete. Also do not mark unreachable statutes if
@@ -303,13 +303,9 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
Self.feedback ~current:true "Call to builtin %s%s"
name (if kf_name = name then "" else " for function " ^ kf_name);
apply_call_hooks call state `Builtin;
- (* Do not track garbled mixes created when interpreting the specification,
- as the result of the cvalue builtin will overwrite them. *)
- Locations.Location_Bytes.do_track_garbled_mix false;
let states =
Spec.compute_using_specification ~warn:false kinstr call spec state
in
- Locations.Location_Bytes.do_track_garbled_mix true;
let final_state = join_states states in
match final_state with
| `Bottom ->
diff --git a/src/plugins/eva/engine/transfer_specification.ml b/src/plugins/eva/engine/transfer_specification.ml
index bd0b649c6bdaa5c7d80f0a64e713d08caf666c63..c0520b22fcdeefcc45e9882f89f38bb43780267b 100644
--- a/src/plugins/eva/engine/transfer_specification.ml
+++ b/src/plugins/eva/engine/transfer_specification.ml
@@ -306,21 +306,25 @@ module Make
let env = make_env pre in
let assigns = get_assigns_for_behavior spec behavior in
let check_one_assign cvalue_state (assign, _) =
- match evaluate_location env retres_loc Assign assign with
- | None -> ()
- | Some location ->
- let loc = Precise_locs.imprecise_location (get_ploc location) in
- let cvalue = Cvalue.Model.find cvalue_state loc in
- if Cvalue.V.is_imprecise cvalue
- then
- begin
- ignore (Locations.Location_Bytes.track_garbled_mix cvalue);
- Self.warning ~current:true ~once:true
- ~wkey:Self.wkey_garbled_mix_assigns
- "The specification of function %a has generated a garbled mix \
- for %a."
- Kernel_function.pretty kf pp_assign_clause (Assign, assign)
- end
+ let location = evaluate_location env retres_loc Assign assign in
+ let precise_loc = Option.map get_ploc location in
+ let loc = Option.map Precise_locs.imprecise_location precise_loc in
+ match loc with
+ | None | Some Locations.{ size = Top } -> ()
+ | Some Locations.{ loc; size = Value size } ->
+ let offsm = Cvalue.Model.copy_offsetmap loc size cvalue_state in
+ let warn v =
+ match Cvalue.V_Or_Uninitialized.get_v v with
+ | Top (bases, origin) ->
+ if Origin.register_write bases origin then
+ Self.warning ~current:true ~once:true
+ ~wkey:Self.wkey_garbled_mix_assigns
+ "@[The specification of function %a@ has generated \
+ a garbled mix of addresses@ for %a.@]"
+ Kernel_function.pretty kf pp_assign_clause (Assign, assign)
+ | _ -> ()
+ in
+ Bottom.iter (Cvalue.V_Offsetmap.iter_on_values warn) offsm
in
let check_one_state state =
let cvalue_state = get_cvalue_or_top state in
@@ -335,7 +339,6 @@ module Make
and [status] the status of the behaviors. *)
let compute_effects ~warn kf spec result behaviors status states =
States.join states >>- fun pre_state ->
- Locations.Location_Bytes.do_track_garbled_mix false;
let behavior = List.hd behaviors in
let retres_loc = Option.map Location.eval_varinfo result in
let assigns = get_assigns_for_behavior spec behavior in
@@ -353,7 +356,6 @@ module Make
(* Warn on garbled mixes created by specifications, except on builtins. *)
if warn
then check_post_assigns kf retres_loc spec behavior ~pre:pre_state states;
- Locations.Location_Bytes.do_track_garbled_mix true;
states
(* Reduces the [states] by the assumes and requires clauses of the [behavior]
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 13a12c2e3005871a3047ab6bcc774d8d3c1ae1a4..1bb0994dc6e1d37e40f2327b477b4a1df71ad98a 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -189,13 +189,8 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Assignment by copying the value of a right lvalue. *)
let assign_by_copy ~subdivnb state valuation lval lloc ltyp =
- (* This code about garbled mix is specific to the Cvalue domain.
- Unfortunately, the current API for abstract_domain does not permit
- distinguishing between an evaluation or a copy. *)
- Locations.Location_Bytes.do_track_garbled_mix false;
- let r = copy_lvalue_and_check ~valuation ~subdivnb state lval in
- Locations.Location_Bytes.do_track_garbled_mix true;
- r >>=: fun (valuation, value) ->
+ copy_lvalue_and_check ~valuation ~subdivnb state lval
+ >>=: fun (valuation, value) ->
Copy ({lval; lloc; ltyp}, value), valuation
(* For an initialization, use for_writing:false for the evaluation of
diff --git a/src/plugins/eva/self.ml b/src/plugins/eva/self.ml
index cfe1067963566392dca48328322c3eda7545609a..d1c33a8a5ee375b35ac4c016138ba4181b58cfd3 100644
--- a/src/plugins/eva/self.ml
+++ b/src/plugins/eva/self.ml
@@ -93,14 +93,12 @@ let () =
(* Warning categories. *)
let wkey_alarm = register_warn_category "alarm"
let wkey_locals_escaping = register_warn_category "locals-escaping"
-let wkey_garbled_mix_read = register_warn_category "garbled-mix:read"
-let () = set_warn_status wkey_garbled_mix_read Log.Wfeedback
let wkey_garbled_mix_write = register_warn_category "garbled-mix:write"
let () = set_warn_status wkey_garbled_mix_write Log.Wfeedback
let wkey_garbled_mix_assigns = register_warn_category "garbled-mix:assigns"
-let () = set_warn_status wkey_garbled_mix_assigns Log.Winactive
+let () = set_warn_status wkey_garbled_mix_assigns Log.Wfeedback
let wkey_garbled_mix_summary = register_warn_category "garbled-mix:summary"
-let () = set_warn_status wkey_garbled_mix_summary Log.Winactive
+let () = set_warn_status wkey_garbled_mix_summary Log.Wfeedback
let wkey_builtins_missing_spec = register_warn_category "builtins:missing-spec"
let wkey_builtins_override = register_warn_category "builtins:override"
let wkey_libc_unsupported_spec = register_warn_category "libc:unsupported-spec"
diff --git a/src/plugins/eva/self.mli b/src/plugins/eva/self.mli
index 3ff073a5baab3e01b761681f798d13ddafd4d9ab..c5d22caedb189e077fdff74d9d18bd70de0b950f 100644
--- a/src/plugins/eva/self.mli
+++ b/src/plugins/eva/self.mli
@@ -56,7 +56,6 @@ val dkey_recursion : category
val wkey_alarm: warn_category
val wkey_locals_escaping: warn_category
-val wkey_garbled_mix_read: warn_category
val wkey_garbled_mix_write: warn_category
val wkey_garbled_mix_assigns: warn_category
val wkey_garbled_mix_summary: warn_category
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index 73d1517b788b01dac7dfa5f7aeb7e0c589e5bb6c..e1a9d043fec882e18870b54ba124cdf87ce62943 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -285,16 +285,6 @@ let lval_to_exp =
MemoLvalToExp.memo
(fun lv -> Cil.new_exp ~loc:Cil_datatype.Location.unknown (Lval lv))
-let dump_garbled_mix () =
- let l = Cvalue.V.get_garbled_mix () in
- if l <> [] then
- let pp_one fmt v = Format.fprintf fmt "@[<hov 2>%a@]" Cvalue.V.pretty v in
- Self.warning ~wkey:Self.wkey_garbled_mix_summary
- "Garbled mix generated during analysis:@.\
- @[<v>%a@]"
- (Pretty_utils.pp_list ~pre:"" ~suf:"" ~sep:"@ " pp_one) l
-
-
type deps = Function_Froms.Deps.deps = {
data: Locations.Zone.t;
indirect: Locations.Zone.t;
diff --git a/src/plugins/eva/utils/eva_utils.mli b/src/plugins/eva/utils/eva_utils.mli
index 2e3ab131c5c85d921a2eecf7bc1d6fa42912b002..b7c7a84512a3e487546f175d94229b679fcb82b7 100644
--- a/src/plugins/eva/utils/eva_utils.mli
+++ b/src/plugins/eva/utils/eva_utils.mli
@@ -112,9 +112,6 @@ val is_value_zero: exp -> bool
val lval_to_exp: lval -> exp
(** This function is memoized to avoid creating too many expressions *)
-val dump_garbled_mix: unit -> unit
-(** print information on the garbled mix created during evaluation *)
-
(** Dependences of expressions and lvalues. *)
diff --git a/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle b/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
index c46681a1dfb4df684a4d7739e3782d316a48a598..0597fca78db0c2d14ac7825ecfcc7ffbaa0c75f8 100644
--- a/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
@@ -5,9 +5,6 @@
out of bounds read. assert \valid_read(list);
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
out of bounds read. assert \valid_read((int *)*list);
-[eva:garbled-mix:write] sum_with_unspecified_sequence.c:14:
- Assigning imprecise value to tmp_unroll_5.
- The imprecision originates from Well
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
signed overflow.
assert -2147483648 ≤ ret + tmp_unroll_5;
@@ -16,25 +13,20 @@
signed overflow.
assert ret + tmp_unroll_5 ≤ 2147483647;
(tmp_unroll_5 from vararg)
-[eva:garbled-mix:write] sum_with_unspecified_sequence.c:14:
- Assigning imprecise value to ret.
- The imprecision originates from Well
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
out of bounds read. assert \valid_read(list);
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
out of bounds read. assert \valid_read((int *)*list);
-[eva:garbled-mix:write] sum_with_unspecified_sequence.c:14:
- Assigning imprecise value to tmp.
- The imprecision originates from Well
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
signed overflow. assert -2147483648 ≤ ret + tmp;
(tmp from vararg)
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
signed overflow. assert ret + tmp ≤ 2147483647;
(tmp from vararg)
-[eva:garbled-mix:write] sum_with_unspecified_sequence.c:17:
- Assigning imprecise value to \result<sum>.
- The imprecision originates from Well
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ Initial state (read 12 times, propagated 6 times)
+ garbled mix of &{S_0_S___va_params; S_1_S___va_params}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function sum:
ret ∈
diff --git a/src/plugins/variadic/tests/known/oracle/exec.res.oracle b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
index 74ea04f2c8f1a5bfd993c56fc4632ae881ab3cb7..335dfe32f04bc71a0f8347d6161575ecc33dbca2 100644
--- a/src/plugins/variadic/tests/known/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
@@ -20,8 +20,20 @@
Fallback translation of call execlp to a call to the specialized version execlp_fallback_1.
[eva] Analyzing a complete application starting at main
[eva] using specification for function execve
+[eva:garbled-mix:assigns] exec.c:9:
+ The specification of function execve has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] using specification for function execv
+[eva:garbled-mix:assigns] exec.c:11:
+ The specification of function execv has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] using specification for function execvp
+[eva:garbled-mix:assigns] exec.c:12:
+ The specification of function execvp has generated a garbled mix of addresses
+ for assigns clause \result.
+[eva:garbled-mix:assigns] exec.c:13:
+ The specification of function execve has generated a garbled mix of addresses
+ for assigns clause \result.
[kernel:annot:missing-spec] exec.c:15: Warning:
Neither code nor specification for function execlp_fallback_1,
generating default assigns. See -generated-spec-* options for more info
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 96c9680ea4b2dab373d1c3ef0f45d8451e8ee2f8..7b945647be0216ee15d342ea55494da9642fb01b 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -114,6 +114,10 @@
[eva] using specification for function printf_va_23
[eva] using specification for function printf_va_24
[eva] using specification for function printf_va_25
+[eva:garbled-mix:assigns] printf.c:68:
+ The specification of function printf_va_25
+ has generated a garbled mix of addresses
+ for assigns clause __fc_stdout->__fc_FILE_data.
[eva] using specification for function printf_va_26
[kernel:annot:missing-spec] printf.c:71: Warning:
Neither code nor specification for function printf_fallback_1,
@@ -129,7 +133,7 @@
__fc_initial_stdout.__fc_FILE_id ∈ {1}
.__fc_FILE_data ∈
{{ garbled mix of &{"Hello world !\n"}
- (origin: Library function) }}
+ (origin: Library function {printf.c:68}) }}
string ∈ {{ "Hello world !\n" }}
wstring ∈ {{ L"Hello world !\n" }}
c ∈ {52}
diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
index 88fba0600f56111170990308fe5ce792df30e713..2db3d36303765a91e701f6147e9efaacfb3e789d 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -20,13 +20,16 @@
Translating call to printf to a call to the specialized version printf_va_1.
[eva] Analyzing a complete application starting at main
[eva:garbled-mix:write] printf_garbled_mix.c:6:
- Assigning imprecise value to b.
- The imprecision originates from Arithmetic {printf_garbled_mix.c:6}
+ Assigning imprecise value to b because of arithmetic operation on addresses.
[eva:alarm] printf_garbled_mix.c:7: Warning:
pointer downcast. assert (unsigned long)b ≤ 2147483647;
[eva] using specification for function printf_va_1
[eva] printf_garbled_mix.c:8:
Frama_C_show_each_nb_printed: [-2147483648..2147483647]
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ printf_garbled_mix.c:6: arithmetic operation on addresses
+ (read 2 times, propagated 3 times) garbled mix of &{a}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
a[0] ∈ {1}
@@ -36,7 +39,7 @@
S___fc_stdout[0].__fc_FILE_id ∈ [--..--]
[0].__fc_FILE_data ∈
{{ garbled mix of &{a}
- (origin: Library function {printf_garbled_mix.c:7}) }}
+ (origin: Arithmetic {printf_garbled_mix.c:6}) }}
[1] ∈ [--..--]
/* Generated by Frama-C */
#include "errno.h"
diff --git a/tests/builtins/oracle/alloc.0.res.oracle b/tests/builtins/oracle/alloc.0.res.oracle
index 3ef4276dae84fa303cf368b3375377e8ac2e783b..684b949a466e6344892b87d74be20242abcbd010 100644
--- a/tests/builtins/oracle/alloc.0.res.oracle
+++ b/tests/builtins/oracle/alloc.0.res.oracle
@@ -39,8 +39,7 @@
[eva:alarm] alloc.c:26: Warning:
signed overflow. assert -((int)q) ≤ 2147483647;
[eva:garbled-mix:write] alloc.c:26:
- Assigning imprecise value to r.
- The imprecision originates from Arithmetic {alloc.c:26}
+ Assigning imprecise value to r because of arithmetic operation on addresses.
[eva:alarm] alloc.c:27: Warning: out of bounds write. assert \valid(r);
[eva:alarm] alloc.c:27: Warning: out of bounds read. assert \valid_read(r + 1);
[eva] alloc.c:32: Call to builtin malloc
@@ -65,6 +64,10 @@
all target addresses were invalid. This path is assumed to be dead.
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ alloc.c:26: arithmetic operation on addresses
+ (read 3 times, propagated 1 times) garbled mix of &{__malloc_main_l25}
[eva] alloc.c:18: assertion 'Eva,mem_access' got final status invalid.
[eva] alloc.c:19: assertion 'Eva,mem_access' got final status invalid.
[eva] alloc.c:20: assertion 'Eva,mem_access' got final status invalid.
diff --git a/tests/builtins/oracle/alloc.1.res.oracle b/tests/builtins/oracle/alloc.1.res.oracle
index d2683593c4b609727030a1db6ff6813ea4a0f654..3ce9953a7b83089a4d07f17bbecd883f451dca85 100644
--- a/tests/builtins/oracle/alloc.1.res.oracle
+++ b/tests/builtins/oracle/alloc.1.res.oracle
@@ -22,8 +22,7 @@
[eva:alarm] alloc.c:51: Warning:
signed overflow. assert -((int)q) ≤ 2147483647;
[eva:garbled-mix:write] alloc.c:51:
- Assigning imprecise value to r.
- The imprecision originates from Arithmetic {alloc.c:51}
+ Assigning imprecise value to r because of arithmetic operation on addresses.
[eva:alarm] alloc.c:54: Warning: out of bounds write. assert \valid(r);
[eva:alarm] alloc.c:54: Warning:
pointer downcast. assert (unsigned int)r ≤ 2147483647;
@@ -31,11 +30,16 @@
[eva:alarm] alloc.c:56: Warning: signed overflow. assert *q + 1 ≤ 2147483647;
[eva] Recording results for main_abs
[eva] Done for function main_abs
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ alloc.c:51: arithmetic operation on addresses
+ (read 2 times, propagated 1 times)
+ garbled mix of &{__malloc_main_abs_l50}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main_abs:
NULL[rbits 2048 to 4103] ∈
{{ garbled mix of &{__malloc_main_abs_l50}
- (origin: Misaligned {alloc.c:54}) }}
+ (origin: Misaligned write {alloc.c:54}) }}
__fc_heap_status ∈ [--..--]
q ∈ {{ &__malloc_main_abs_l50 }}
r ∈ {{ NULL + [256..509] ; &__malloc_main_abs_l50 }}
diff --git a/tests/builtins/oracle/imprecise-malloc-free.res.oracle b/tests/builtins/oracle/imprecise-malloc-free.res.oracle
index 2d02014061a0fa9b8a3b45c488f4446d6f17f178..4cd01a4b78eb93961e52f4939f1736ed257095bb 100644
--- a/tests/builtins/oracle/imprecise-malloc-free.res.oracle
+++ b/tests/builtins/oracle/imprecise-malloc-free.res.oracle
@@ -13,10 +13,13 @@
[eva:alarm] imprecise-malloc-free.c:13: Warning:
signed overflow. assert i + (int)((int)(&size2) >> 1) ≤ 2147483647;
[eva:garbled-mix:write] imprecise-malloc-free.c:13:
- Assigning imprecise value to size2.
- The imprecision originates from Arithmetic {imprecise-malloc-free.c:13}
+ Assigning imprecise value to size2
+ because of arithmetic operation on addresses.
[eva:alarm] imprecise-malloc-free.c:14: Warning:
pointer downcast. assert (unsigned int)(&i) ≤ 2147483647;
+[eva:garbled-mix:write] imprecise-malloc-free.c:14:
+ Assigning imprecise value to size
+ because of arithmetic operation on addresses.
[eva] imprecise-malloc-free.c:14: Call to builtin malloc
[eva] imprecise-malloc-free.c:14: allocating variable __malloc_main_l14
[eva] imprecise-malloc-free.c:15: Call to builtin malloc
@@ -44,12 +47,16 @@
pointer downcast. assert (unsigned int)(r + 3) ≤ 2147483647;
[eva:alarm] imprecise-malloc-free.c:25: Warning:
pointer downcast. assert (unsigned int)p ≤ 2147483647;
+[eva:garbled-mix:write] imprecise-malloc-free.c:25:
+ Assigning imprecise value to p because of arithmetic operation on addresses.
[eva] imprecise-malloc-free.c:25: Call to builtin free
[eva:alarm] imprecise-malloc-free.c:25: Warning:
function free: precondition 'freeable' got status unknown.
[eva:malloc] imprecise-malloc-free.c:25: weak free on bases: {__malloc_main_l14}
[eva:alarm] imprecise-malloc-free.c:26: Warning:
pointer downcast. assert (unsigned int)r ≤ 2147483647;
+[eva:garbled-mix:write] imprecise-malloc-free.c:26:
+ Assigning imprecise value to p because of arithmetic operation on addresses.
[eva] imprecise-malloc-free.c:26: Call to builtin free
[eva:alarm] imprecise-malloc-free.c:26: Warning:
function free: precondition 'freeable' got status unknown.
@@ -57,6 +64,10 @@
weak free on bases: {__malloc_main_l15, __malloc_main_l16}
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ imprecise-malloc-free.c:13: arithmetic operation on addresses
+ (read 1 times, propagated 2 times) garbled mix of &{size2}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index bc169708e5bc2c84ecf6d7b2538ebbd7611b688d..d5857d6a3780f56d151fe939579bfa1bfc81ef4d 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -51,8 +51,7 @@
[eva:alarm] imprecise.c:19: Warning:
pointer downcast. assert (unsigned int)(&k) ≤ 2147483647;
[eva:garbled-mix:write] imprecise.c:19:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {imprecise.c:19}
+ Assigning imprecise value to p because of arithmetic operation on addresses.
[eva:alarm] imprecise.c:20: Warning: out of bounds write. assert \valid(p);
[eva] imprecise.c:21:
Frama_C_dump_each:
@@ -121,8 +120,7 @@
[eva:alarm] imprecise.c:68: Warning:
signed overflow. assert (int)*((char *)(&p)) + 0 ≤ 2147483647;
[eva:garbled-mix:write] imprecise.c:68:
- Assigning imprecise value to c3.
- The imprecision originates from Misaligned {imprecise.c:68}
+ Assigning imprecise value to c3 because of misaligned read of addresses.
[eva] Recording results for cast_address
[from] Computing for function cast_address
[from] Done for function cast_address
@@ -266,12 +264,16 @@
[from] Computing for function main
[from] Done for function main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ imprecise.c:19: arithmetic operation on addresses
+ (read 3 times, propagated 1 times) garbled mix of &{j; k}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function cast_address:
p ∈ {{ &x }}
c1 ∈ {{ (char)&x }}
c2# ∈ {{ (? *)&x }}%32, bits 0 to 7
- c3 ∈ {{ garbled mix of &{x} (origin: Misaligned {imprecise.c:68}) }}
+ c3 ∈ {{ garbled mix of &{x} (origin: Misaligned read {imprecise.c:68}) }}
[eva:final-states] Values at end of function garbled_mix_null:
NULL[rbits 800 to 1607] ∈ [--..--] or ESCAPINGADDR
p_gm_null ∈ [100..197]
@@ -315,11 +317,12 @@
vy ∈ {1} or UNINITIALIZED
[eva:final-states] Values at end of function write_garbled:
NULL[rbits 800 to 1607] ∈
- {{ garbled mix of &{j; k} (origin: Misaligned {imprecise.c:22}) }}
+ {{ garbled mix of &{j; k}
+ (origin: Misaligned write {imprecise.c:22}) }}
i ∈ {1}
j ∈ {{ NULL + [1..197] ; (int)&j ; &k + [0..16] }}
k[0..4] ∈
- {{ garbled mix of &{j; k} (origin: Misaligned {imprecise.c:22}) }}
+ {{ garbled mix of &{j; k} (origin: Misaligned write {imprecise.c:22}) }}
p ∈ {{ NULL + [100..197] ; &j ; &k + [0..16] }}
[eva:final-states] Values at end of function main:
NULL[rbits 800 to 1607] ∈ [--..--] or ESCAPINGADDR
@@ -809,12 +812,16 @@
[from] Computing for function main
[from] Done for function main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ imprecise.c:19: arithmetic operation on addresses
+ (read 3 times, propagated 1 times) garbled mix of &{j; k}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function cast_address:
p ∈ {{ &x }}
c1 ∈ {{ (char)&x }}
c2# ∈ {{ (? *)&x }}%32, bits 0 to 7
- c3 ∈ {{ garbled mix of &{x} (origin: Misaligned {imprecise.c:68}) }}
+ c3 ∈ {{ garbled mix of &{x} (origin: Misaligned read {imprecise.c:68}) }}
[eva:final-states] Values at end of function garbled_mix_null:
NULL[rbits 800 to 1607] ∈ [--..--] or ESCAPINGADDR
p_gm_null ∈ [100..197]
@@ -855,11 +862,12 @@
vy ∈ {1} or UNINITIALIZED
[eva:final-states] Values at end of function write_garbled:
NULL[rbits 800 to 1607] ∈
- {{ garbled mix of &{j; k} (origin: Misaligned {imprecise.c:22}) }}
+ {{ garbled mix of &{j; k}
+ (origin: Misaligned write {imprecise.c:22}) }}
i ∈ {1}
j ∈ {{ NULL + [1..197] ; (int)&j ; &k + [0..16] }}
k[0..4] ∈
- {{ garbled mix of &{j; k} (origin: Misaligned {imprecise.c:22}) }}
+ {{ garbled mix of &{j; k} (origin: Misaligned write {imprecise.c:22}) }}
p ∈ {{ NULL + [100..197] ; &j ; &k + [0..16] }}
[eva:final-states] Values at end of function main:
NULL[rbits 800 to 1607] ∈ [--..--] or ESCAPINGADDR
diff --git a/tests/builtins/oracle/linked_list.1.res.oracle b/tests/builtins/oracle/linked_list.1.res.oracle
index 16a5a8ec3b5bbdf8045da8874b28335e0b4bc819..c97ebeb2a70161b6c360d6cb8bf94962bf92fb3f 100644
--- a/tests/builtins/oracle/linked_list.1.res.oracle
+++ b/tests/builtins/oracle/linked_list.1.res.oracle
@@ -806,6 +806,10 @@
Called from linked_list.c:51.
[eva] using specification for function printf_va_1
[eva] linked_list.c:51: function printf_va_1: precondition got status valid.
+[eva:garbled-mix:assigns] linked_list.c:51:
+ The specification of function printf_va_1
+ has generated a garbled mix of addresses
+ for assigns clause __fc_stdout->__fc_FILE_data.
[eva] Done for function printf_va_1
[kernel] linked_list.c:51:
more than 100(128) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 9354818cac31b53111b4fa4ed36dd05b396818c7..6fe4eedb72486a27ebdc2582a036bea66c8573cd 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -100,13 +100,22 @@
[eva] memcpy.c:85: function memcpy: precondition 'separation' got status valid.
[eva:alarm] memcpy.c:87: Warning:
pointer downcast. assert (unsigned int)((struct t1 *)t) ≤ 2147483647;
+[eva:garbled-mix:write] memcpy.c:87:
+ Assigning imprecise value to src
+ because of arithmetic operation on addresses.
[eva] memcpy.c:87: Call to builtin memcpy
[eva] memcpy.c:87: function memcpy: precondition 'valid_dest' got status valid.
[eva:alarm] memcpy.c:87: Warning:
function memcpy: precondition 'valid_src' got status unknown.
[eva] memcpy.c:87: function memcpy: precondition 'separation' got status valid.
+[eva:garbled-mix:write] memcpy.c:87:
+ Builtin memcpy: assigning imprecise value to v3
+ because of misaligned read of addresses.
[eva:alarm] memcpy.c:89: Warning:
pointer downcast. assert (unsigned int)(&v4) ≤ 2147483647;
+[eva:garbled-mix:write] memcpy.c:89:
+ Assigning imprecise value to dest
+ because of arithmetic operation on addresses.
[eva] memcpy.c:89: Call to builtin memcpy
[eva:alarm] memcpy.c:89: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
@@ -118,6 +127,9 @@
pointer downcast. assert (unsigned int)((struct t1 *)t) ≤ 2147483647;
[eva:alarm] memcpy.c:91: Warning:
pointer downcast. assert (unsigned int)(&v5) ≤ 2147483647;
+[eva:garbled-mix:write] memcpy.c:91:
+ Assigning imprecise value to dest
+ because of arithmetic operation on addresses.
[eva] memcpy.c:91: Call to builtin memcpy
[eva:alarm] memcpy.c:91: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
@@ -564,11 +576,11 @@
v2.x ∈ {5}
.y ∈ {7}
{.p; .padding[0..23]} ∈ {0}
- v3 ∈ {{ garbled mix of &{v1} (origin: Misaligned {memcpy.c:87}) }}
+ v3 ∈ {{ garbled mix of &{v1} (origin: Misaligned read {memcpy.c:87}) }}
v4.x ∈ [--..--]
.y ∈ {{ (int)&t }}
{.p; .padding[0..23]} ∈ [--..--]
- v5 ∈ {{ garbled mix of &{t} (origin: Misaligned {memcpy.c:91}) }}
+ v5 ∈ {{ garbled mix of &{t} (origin: Arithmetic {memcpy.c:91}) }}
t{[0]; [1]{.x; .y}} ∈ {0}
[1].p ∈ {{ &v1.y }}
{[1].padding[0..23]; [2]; [3]{.x; .y}} ∈ {0}
diff --git a/tests/builtins/oracle/memset.res.oracle b/tests/builtins/oracle/memset.res.oracle
index a71515ecdbf65f033962389a94fb5e9028f811f4..a6115d361b6b54206f7f038fd794ce01df915472 100644
--- a/tests/builtins/oracle/memset.res.oracle
+++ b/tests/builtins/oracle/memset.res.oracle
@@ -28,6 +28,8 @@
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[eva:alarm] memset.c:34: Warning:
pointer downcast. assert (unsigned int)((int *)t2) ≤ 2147483647;
+[eva:garbled-mix:write] memset.c:34:
+ Assigning imprecise value to s because of arithmetic operation on addresses.
[eva] memset.c:34: Call to builtin memset
[eva:alarm] memset.c:34: Warning:
function memset: precondition 'valid_s' got status unknown.
@@ -49,6 +51,9 @@
[eva] memset.c:41: function memset: precondition 'valid_s' got status valid.
[eva:imprecision] memset.c:41:
Call to builtin precise_memset(({{ (void *)&t5 }},{{ (int)&t1 }},{400})) failed; value to write is imprecise
+[eva:garbled-mix:write] memset.c:41:
+ Builtin memset: assigning imprecise value to t5[0]
+ because of misaligned read of addresses.
[eva] memset.c:44: Call to builtin memset
[eva] memset.c:44: function memset: precondition 'valid_s' got status valid.
[eva:imprecision] memset.c:44:
@@ -108,7 +113,8 @@
t3[0..9] ∈ {0}
[10..99]# ∈ {0; 17} repeated %8
t4[0..99] ∈ {0}
- t5[0..99] ∈ {{ garbled mix of &{t1} (origin: Misaligned {memset.c:41}) }}
+ t5[0..99] ∈
+ {{ garbled mix of &{t1} (origin: Misaligned read {memset.c:41}) }}
t6[0..9] ∈ {0}
[10..13]# ∈ {0; 34} repeated %8
[14..99] ∈ {0}
@@ -163,7 +169,8 @@
t3[0..9] ∈ {0}
[10..99]# ∈ {0; 17} repeated %8
t4[0..99] ∈ {0}
- t5[0..99] ∈ {{ garbled mix of &{t1} (origin: Misaligned {memset.c:41}) }}
+ t5[0..99] ∈
+ {{ garbled mix of &{t1} (origin: Misaligned read {memset.c:41}) }}
t6[0..9] ∈ {0}
[10..13]# ∈ {0; 34} repeated %8
[14..99] ∈ {0}
diff --git a/tests/builtins/oracle/strchr.res.oracle b/tests/builtins/oracle/strchr.res.oracle
index e9cfcd8c7928de0aa61c8d1c8cf267de2e8dc1bd..e1298461c038a1977a5d897d8e9a7a897efa1975 100644
--- a/tests/builtins/oracle/strchr.res.oracle
+++ b/tests/builtins/oracle/strchr.res.oracle
@@ -640,6 +640,8 @@
[eva] Done for function strchr_unbounded
[eva] computing for function strchr_invalid <- main.
Called from strchr.c:561.
+[eva:garbled-mix:write] strchr.c:536:
+ Assigning imprecise value to s because of arithmetic operation on addresses.
[eva] strchr.c:536: Call to builtin strchr
[eva:alarm] strchr.c:536: Warning:
function strchr: precondition 'valid_string_s' got status unknown.
@@ -659,8 +661,8 @@
[eva:alarm] strchr.c:541: Warning:
pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:garbled-mix:write] strchr.c:541:
- Assigning imprecise value to garbled.
- The imprecision originates from Arithmetic {strchr.c:541}
+ Assigning imprecise value to garbled
+ because of arithmetic operation on addresses.
[eva:alarm] strchr.c:542: Warning:
pointer downcast. assert (unsigned int)garbled ≤ 2147483647;
[eva] strchr.c:542: Call to builtin strchr
@@ -670,6 +672,10 @@
[eva] Done for function strchr_garbled_mix_in_char
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ strchr.c:541: arithmetic operation on addresses
+ (read 1 times, propagated 3 times) garbled mix of &{x}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function init_array_nondet:
from ∈ {-1}
diff --git a/tests/builtins/oracle_equality/imprecise.res.oracle b/tests/builtins/oracle_equality/imprecise.res.oracle
index eb4cf14573bb6394a0e018d936c72176c7b61f25..510c64aad8aaa51da0c6f9e5f58617e8b42eef36 100644
--- a/tests/builtins/oracle_equality/imprecise.res.oracle
+++ b/tests/builtins/oracle_equality/imprecise.res.oracle
@@ -1,13 +1,13 @@
-99a100,101
+98a99,100
> [kernel] imprecise.c:51:
> imprecise size for variable v3 (abstract type 'struct u')
-222a225,226
+220a223,224
> [kernel] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
-230a235,236
+228a233,234
> [kernel] imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
-239,242d244
+237,240d242
< [kernel] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
< [kernel] imprecise.c:114:
diff --git a/tests/builtins/oracle_equality/linked_list.1.res.oracle b/tests/builtins/oracle_equality/linked_list.1.res.oracle
index dc1c07fbca0f6ce44824d4bdff2b3cf9110babd1..08a077ea283d0d72948ad4ac7cc139699f42818e 100644
--- a/tests/builtins/oracle_equality/linked_list.1.res.oracle
+++ b/tests/builtins/oracle_equality/linked_list.1.res.oracle
@@ -16,9 +16,9 @@
720a731,732
> [kernel] linked_list.c:44:
> more than 100(128) elements to enumerate. Approximating.
-810,811d821
+814,815d825
< [kernel] linked_list.c:51:
< more than 100(128) elements to enumerate. Approximating.
-819,820d828
+823,824d832
< [kernel] linked_list.c:44:
< more than 100(128) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle_gauges/linked_list.1.res.oracle b/tests/builtins/oracle_gauges/linked_list.1.res.oracle
index ec6dff88c11d22b8f7b5764d51fe82406d5cd9e0..b4dd8f6901bfedbeff231430246bb6c77f704f48 100644
--- a/tests/builtins/oracle_gauges/linked_list.1.res.oracle
+++ b/tests/builtins/oracle_gauges/linked_list.1.res.oracle
@@ -1,4 +1,4 @@
-817a818,823
+821a822,827
> [eva] computing for function printf_va_1 <- main.
> Called from linked_list.c:51.
> [eva] Done for function printf_va_1
diff --git a/tests/builtins/oracle_gauges/memcpy.res.oracle b/tests/builtins/oracle_gauges/memcpy.res.oracle
index d2986d41912c0fe02c5048b90f543a07721ed311..78ce5790f07d21391745733139582ff60737e029 100644
--- a/tests/builtins/oracle_gauges/memcpy.res.oracle
+++ b/tests/builtins/oracle_gauges/memcpy.res.oracle
@@ -1,5 +1,5 @@
-138a139,140
+150a151,152
> [eva] memcpy.c:96: Call to builtin memcpy
> [eva] memcpy.c:96: Call to builtin memcpy
-364a367
+376a379
> [eva] memcpy.c:230: starting to merge loop iterations
diff --git a/tests/builtins/oracle_octagon/imprecise.res.oracle b/tests/builtins/oracle_octagon/imprecise.res.oracle
index 4001ea81170eeff5bdf55aedd0eeb81230413cab..9633a07ab0e31c0bef97b7be3027233c2a4bf0db 100644
--- a/tests/builtins/oracle_octagon/imprecise.res.oracle
+++ b/tests/builtins/oracle_octagon/imprecise.res.oracle
@@ -1,10 +1,10 @@
-222a223,224
+220a221,222
> [kernel] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
-230a233,234
+228a231,232
> [kernel] imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
-239,242d242
+237,240d240
< [kernel] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
< [kernel] imprecise.c:114:
diff --git a/tests/builtins/oracle_octagon/linked_list.1.res.oracle b/tests/builtins/oracle_octagon/linked_list.1.res.oracle
index 4083e687dd36eae966d07c6feea16e88f79ce698..166d64faad77cf59fe2003c8dda6ac23d5adf97d 100644
--- a/tests/builtins/oracle_octagon/linked_list.1.res.oracle
+++ b/tests/builtins/oracle_octagon/linked_list.1.res.oracle
@@ -10,9 +10,9 @@
720a727,728
> [kernel] linked_list.c:44:
> more than 100(128) elements to enumerate. Approximating.
-810,811d817
+814,815d821
< [kernel] linked_list.c:51:
< more than 100(128) elements to enumerate. Approximating.
-819,820d824
+823,824d828
< [kernel] linked_list.c:44:
< more than 100(128) elements to enumerate. Approximating.
diff --git a/tests/builtins/oracle_symblocs/imprecise.res.oracle b/tests/builtins/oracle_symblocs/imprecise.res.oracle
index 4001ea81170eeff5bdf55aedd0eeb81230413cab..9633a07ab0e31c0bef97b7be3027233c2a4bf0db 100644
--- a/tests/builtins/oracle_symblocs/imprecise.res.oracle
+++ b/tests/builtins/oracle_symblocs/imprecise.res.oracle
@@ -1,10 +1,10 @@
-222a223,224
+220a221,222
> [kernel] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
-230a233,234
+228a231,232
> [kernel] imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
-239,242d242
+237,240d240
< [kernel] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
< [kernel] imprecise.c:114:
diff --git a/tests/builtins/oracle_symblocs/linked_list.1.res.oracle b/tests/builtins/oracle_symblocs/linked_list.1.res.oracle
index 4083e687dd36eae966d07c6feea16e88f79ce698..166d64faad77cf59fe2003c8dda6ac23d5adf97d 100644
--- a/tests/builtins/oracle_symblocs/linked_list.1.res.oracle
+++ b/tests/builtins/oracle_symblocs/linked_list.1.res.oracle
@@ -10,9 +10,9 @@
720a727,728
> [kernel] linked_list.c:44:
> more than 100(128) elements to enumerate. Approximating.
-810,811d817
+814,815d821
< [kernel] linked_list.c:51:
< more than 100(128) elements to enumerate. Approximating.
-819,820d824
+823,824d828
< [kernel] linked_list.c:44:
< more than 100(128) elements to enumerate. Approximating.
diff --git a/tests/fc_script/make-wrapper.t/run.t b/tests/fc_script/make-wrapper.t/run.t
index b64143a7e576c1148033632a3cd74eb5c60b700e..e70aaa31a57f87209702a00fbbae0814ef2f7258 100644
--- a/tests/fc_script/make-wrapper.t/run.t
+++ b/tests/fc_script/make-wrapper.t/run.t
@@ -11,7 +11,7 @@ verbose output for Make.
[kernel] Parsing make-wrapper.c (with preprocessing)
[kernel] Parsing make-wrapper2.c (with preprocessing)
- Command: frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -eva -eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state -eva-print-callstacks -eva-warn-key alarm=inactive -no-deps-print -no-calldeps-print -eva-warn-key garbled-mix=active,garbled-mix:write=feedback -calldeps -from-verbose 0 -eva-warn-key builtins:missing-spec=abort
+ Command: frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -eva -eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state -eva-print-callstacks -eva-warn-key alarm=inactive -no-deps-print -no-calldeps-print -eva-warn-key garbled-mix=active,garbled-mix:write=active -calldeps -from-verbose 0 -eva-warn-key builtins:missing-spec=abort
[eva] Analyzing a complete application starting at main
[eva:recursion] make-wrapper.c:17:
diff --git a/tests/float/oracle/builtins.res.oracle b/tests/float/oracle/builtins.res.oracle
index 0de9a86128d5d8b7f0db04b759781353078ab46f..5039c250f6b7711f4c2d73630e0df5ae8926e78d 100644
--- a/tests/float/oracle/builtins.res.oracle
+++ b/tests/float/oracle/builtins.res.oracle
@@ -125,15 +125,14 @@
pointer downcast. assert (unsigned int)(&d) ≤ 2147483647;
[eva:alarm] builtins.c:107: Warning:
non-finite double value. assert \is_finite((double)((int)(&d)));
+[eva:garbled-mix:write] builtins.c:107:
+ Assigning imprecise value to x because of arithmetic operation on addresses.
[eva] builtins.c:107: Call to builtin log
[eva:alarm] builtins.c:107: Warning:
function log: precondition 'finite_arg' got status unknown.
[eva:alarm] builtins.c:107: Warning:
function log: precondition 'arg_positive' got status unknown.
[eva] builtins.c:107: function Frama_C_log applied to address
-[eva:garbled-mix:write] builtins.c:107:
- Assigning imprecise value to l7.
- The imprecision originates from Arithmetic {builtins.c:107}
[eva:alarm] builtins.c:111: Warning:
accessing uninitialized left-value. assert \initialized(&x);
[eva] Recording results for main_log_exp
diff --git a/tests/float/oracle/nonlin.0.res.oracle b/tests/float/oracle/nonlin.0.res.oracle
index 3c25cbe9a7e7af49f5712d3551e3f897e2695832..043c52aa669533e1deb16aecb97093e67d3ede6e 100644
--- a/tests/float/oracle/nonlin.0.res.oracle
+++ b/tests/float/oracle/nonlin.0.res.oracle
@@ -236,15 +236,12 @@
non-finite float value.
assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
[eva:garbled-mix:write] nonlin.c:98:
- Assigning imprecise value to a_0.
- The imprecision originates from Arithmetic {nonlin.c:98}
+ Assigning imprecise value to a_0
+ because of arithmetic operation on addresses.
[eva:alarm] nonlin.c:99: Warning:
non-finite float value. assert \is_finite(a_0);
[eva:alarm] nonlin.c:99: Warning:
non-finite float value. assert \is_finite(\add_float(a_0, a_0));
-[eva:garbled-mix:write] nonlin.c:99:
- Assigning imprecise value to f.
- The imprecision originates from Arithmetic
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -287,6 +284,10 @@
[eva] Done for function subdivide_strategy
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ nonlin.c:98: arithmetic operation on addresses
+ (read 1 times, propagated 2 times) garbled mix of &{x_0}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
@@ -299,7 +300,7 @@
res ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
[eva:final-states] Values at end of function garbled:
a_0 ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
- f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
+ f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
diff --git a/tests/float/oracle/nonlin.1.res.oracle b/tests/float/oracle/nonlin.1.res.oracle
index 5efd17ffac7dcc632dff44d55cc85a13e8898dfe..b69461ed024bb293807c22fcf863c634a5df7ae1 100644
--- a/tests/float/oracle/nonlin.1.res.oracle
+++ b/tests/float/oracle/nonlin.1.res.oracle
@@ -255,15 +255,12 @@
non-finite float value.
assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
[eva:garbled-mix:write] nonlin.c:98:
- Assigning imprecise value to a_0.
- The imprecision originates from Arithmetic {nonlin.c:98}
+ Assigning imprecise value to a_0
+ because of arithmetic operation on addresses.
[eva:alarm] nonlin.c:99: Warning:
non-finite float value. assert \is_finite(a_0);
[eva:alarm] nonlin.c:99: Warning:
non-finite float value. assert \is_finite(\add_float(a_0, a_0));
-[eva:garbled-mix:write] nonlin.c:99:
- Assigning imprecise value to f.
- The imprecision originates from Arithmetic
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -314,6 +311,10 @@
[eva] Done for function subdivide_strategy
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ nonlin.c:98: arithmetic operation on addresses
+ (read 1 times, propagated 2 times) garbled mix of &{x_0}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
@@ -326,7 +327,7 @@
res ∈ {-0x1.0000000000000p0}
[eva:final-states] Values at end of function garbled:
a_0 ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
- f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
+ f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
diff --git a/tests/float/oracle/nonlin.2.res.oracle b/tests/float/oracle/nonlin.2.res.oracle
index 861a2facbf87e30b66c3edbb44e96f26b64fdb9b..05b14b3983b595fd05c1a39dcc9fb51cac2aebcb 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -242,11 +242,8 @@
[eva:alarm] nonlin.c:98: Warning:
pointer downcast. assert (unsigned int)(&x_0 + (int)(&x_0)) ≤ 2147483647;
[eva:garbled-mix:write] nonlin.c:98:
- Assigning imprecise value to a_0.
- The imprecision originates from Arithmetic {nonlin.c:98}
-[eva:garbled-mix:write] nonlin.c:99:
- Assigning imprecise value to f.
- The imprecision originates from Arithmetic
+ Assigning imprecise value to a_0
+ because of arithmetic operation on addresses.
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -288,6 +285,10 @@
[eva] Done for function subdivide_strategy
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ nonlin.c:98: arithmetic operation on addresses
+ (read 1 times, propagated 2 times) garbled mix of &{x_0}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
@@ -300,7 +301,7 @@
res ∈ [-0x1.0000000000000p0 .. inf]
[eva:final-states] Values at end of function garbled:
a_0 ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
- f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
+ f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
diff --git a/tests/float/oracle/nonlin.3.res.oracle b/tests/float/oracle/nonlin.3.res.oracle
index e59972c716fe567af8459aa206ab9eb68ddee54c..24ccbef205c1cd4e1a182e9eb30eebea036393c0 100644
--- a/tests/float/oracle/nonlin.3.res.oracle
+++ b/tests/float/oracle/nonlin.3.res.oracle
@@ -236,15 +236,12 @@
non-finite float value.
assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
[eva:garbled-mix:write] nonlin.c:98:
- Assigning imprecise value to a_0.
- The imprecision originates from Arithmetic {nonlin.c:98}
+ Assigning imprecise value to a_0
+ because of arithmetic operation on addresses.
[eva:alarm] nonlin.c:99: Warning:
non-finite float value. assert \is_finite(a_0);
[eva:alarm] nonlin.c:99: Warning:
non-finite float value. assert \is_finite(\add_float(a_0, a_0));
-[eva:garbled-mix:write] nonlin.c:99:
- Assigning imprecise value to f.
- The imprecision originates from Arithmetic
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -287,6 +284,10 @@
[eva] Done for function subdivide_strategy
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ nonlin.c:98: arithmetic operation on addresses
+ (read 1 times, propagated 2 times) garbled mix of &{x_0}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
@@ -299,7 +300,7 @@
res ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
[eva:final-states] Values at end of function garbled:
a_0 ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
- f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
+ f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
diff --git a/tests/float/oracle/nonlin.4.res.oracle b/tests/float/oracle/nonlin.4.res.oracle
index a9cb1e55da7d560464a16b788891e8ebd15924c9..a0f41891c242df0ead1a4ee73efaea7f01404844 100644
--- a/tests/float/oracle/nonlin.4.res.oracle
+++ b/tests/float/oracle/nonlin.4.res.oracle
@@ -255,15 +255,12 @@
non-finite float value.
assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
[eva:garbled-mix:write] nonlin.c:98:
- Assigning imprecise value to a_0.
- The imprecision originates from Arithmetic {nonlin.c:98}
+ Assigning imprecise value to a_0
+ because of arithmetic operation on addresses.
[eva:alarm] nonlin.c:99: Warning:
non-finite float value. assert \is_finite(a_0);
[eva:alarm] nonlin.c:99: Warning:
non-finite float value. assert \is_finite(\add_float(a_0, a_0));
-[eva:garbled-mix:write] nonlin.c:99:
- Assigning imprecise value to f.
- The imprecision originates from Arithmetic
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -314,6 +311,10 @@
[eva] Done for function subdivide_strategy
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ nonlin.c:98: arithmetic operation on addresses
+ (read 1 times, propagated 2 times) garbled mix of &{x_0}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
@@ -326,7 +327,7 @@
res ∈ {-0x1.0000000000000p0}
[eva:final-states] Values at end of function garbled:
a_0 ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
- f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
+ f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
diff --git a/tests/float/oracle/nonlin.5.res.oracle b/tests/float/oracle/nonlin.5.res.oracle
index a41360104ac0b5d7e0e6c427029d9940bf1b7394..25cd26ba1ee0c29e381e99198b125dd655c37124 100644
--- a/tests/float/oracle/nonlin.5.res.oracle
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -242,11 +242,8 @@
[eva:alarm] nonlin.c:98: Warning:
pointer downcast. assert (unsigned int)(&x_0 + (int)(&x_0)) ≤ 2147483647;
[eva:garbled-mix:write] nonlin.c:98:
- Assigning imprecise value to a_0.
- The imprecision originates from Arithmetic {nonlin.c:98}
-[eva:garbled-mix:write] nonlin.c:99:
- Assigning imprecise value to f.
- The imprecision originates from Arithmetic
+ Assigning imprecise value to a_0
+ because of arithmetic operation on addresses.
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -288,6 +285,10 @@
[eva] Done for function subdivide_strategy
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ nonlin.c:98: arithmetic operation on addresses
+ (read 1 times, propagated 2 times) garbled mix of &{x_0}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function access_bits:
rbits1 ∈ {0; 1; 2}
@@ -300,7 +301,7 @@
res ∈ [-0x1.0000000000000p0 .. inf]
[eva:final-states] Values at end of function garbled:
a_0 ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
- f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
+ f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
diff --git a/tests/float/oracle_octagon/nonlin.1.res.oracle b/tests/float/oracle_octagon/nonlin.1.res.oracle
index 47df4c6b3ec06d4d53cb840cd6daf42606770e89..6eefc1b9fe0c8e2bfb44c95f71f61bc9f761dcf4 100644
--- a/tests/float/oracle_octagon/nonlin.1.res.oracle
+++ b/tests/float/oracle_octagon/nonlin.1.res.oracle
@@ -1,5 +1,5 @@
-277a278,279
+274a275,276
> [eva:nonlin] nonlin.c:113: non-linear 'f + f', lv 'f'
> [eva:nonlin] nonlin.c:113: subdividing on f
-280d281
+277d278
< [eva:nonlin] nonlin.c:113: subdividing on f
diff --git a/tests/float/oracle_octagon/nonlin.2.res.oracle b/tests/float/oracle_octagon/nonlin.2.res.oracle
index 32ee5946f24c027cb7bf9fbb4f5475f1efd4b0a9..af64eb11946572bd8f9d116a6d6731adf1112bcb 100644
--- a/tests/float/oracle_octagon/nonlin.2.res.oracle
+++ b/tests/float/oracle_octagon/nonlin.2.res.oracle
@@ -1,5 +1,5 @@
-260a261,262
+257a258,259
> [eva:nonlin] nonlin.c:113: non-linear 'f + f', lv 'f'
> [eva:nonlin] nonlin.c:113: subdividing on f
-263d264
+260d261
< [eva:nonlin] nonlin.c:113: subdividing on f
diff --git a/tests/float/oracle_octagon/nonlin.4.res.oracle b/tests/float/oracle_octagon/nonlin.4.res.oracle
index 47df4c6b3ec06d4d53cb840cd6daf42606770e89..6eefc1b9fe0c8e2bfb44c95f71f61bc9f761dcf4 100644
--- a/tests/float/oracle_octagon/nonlin.4.res.oracle
+++ b/tests/float/oracle_octagon/nonlin.4.res.oracle
@@ -1,5 +1,5 @@
-277a278,279
+274a275,276
> [eva:nonlin] nonlin.c:113: non-linear 'f + f', lv 'f'
> [eva:nonlin] nonlin.c:113: subdividing on f
-280d281
+277d278
< [eva:nonlin] nonlin.c:113: subdividing on f
diff --git a/tests/float/oracle_octagon/nonlin.5.res.oracle b/tests/float/oracle_octagon/nonlin.5.res.oracle
index 32ee5946f24c027cb7bf9fbb4f5475f1efd4b0a9..af64eb11946572bd8f9d116a6d6731adf1112bcb 100644
--- a/tests/float/oracle_octagon/nonlin.5.res.oracle
+++ b/tests/float/oracle_octagon/nonlin.5.res.oracle
@@ -1,5 +1,5 @@
-260a261,262
+257a258,259
> [eva:nonlin] nonlin.c:113: non-linear 'f + f', lv 'f'
> [eva:nonlin] nonlin.c:113: subdividing on f
-263d264
+260d261
< [eva:nonlin] nonlin.c:113: subdividing on f
diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index 59925bcb9eb92e8536134c8ff904f55dacb491f5..fe4f9414bf77cb385fed69ef556d573f56ec2282 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -112,6 +112,9 @@
function sigaction: precondition 'valid_read_act_or_null' got status valid.
[eva] signal_h.c:45:
function sigaction: precondition 'separation,separated_acts' got status valid.
+[eva:garbled-mix:assigns] signal_h.c:45:
+ The specification of function sigaction
+ has generated a garbled mix of addresses for assigns clause *oldact.
[eva] Done for function sigaction
[eva] computing for function sigaction <- main.
Called from signal_h.c:45.
@@ -128,6 +131,9 @@
function sigaction: precondition 'separation,separated_acts' got status valid.
[eva] FRAMAC_SHARE/libc/signal.h:229:
cannot evaluate ACSL term, unsupported ACSL construct: logic coercion struct sigaction -> set<struct sigaction>
+[eva:garbled-mix:assigns] signal_h.c:48:
+ The specification of function sigaction
+ has generated a garbled mix of addresses for assigns clause *oldact.
[eva] Done for function sigaction
[eva] computing for function sigaction <- main.
Called from signal_h.c:51.
@@ -178,7 +184,7 @@
[9]{.sa_mask; .sa_flags} ∈ [--..--]
[10] ∈
{{ garbled mix of &{__fc_sigaction}
- (origin: Library function) }}
+ (origin: Library function {signal_h.c:48}) }}
[11]{.sa_handler; .sa_sigaction} ∈ {0}
[11]{.sa_mask; .sa_flags} ∈ [--..--]
[12]{.sa_handler; .sa_sigaction} ∈ {0}
@@ -193,7 +199,7 @@
{[16]{.sa_mask; .sa_flags}; [17]} ∈ [--..--]
[18] ∈
{{ garbled mix of &{__fc_sigaction}
- (origin: Library function) }}
+ (origin: Library function {signal_h.c:45}) }}
[19]{.sa_handler; .sa_sigaction} ∈ {0}
[19]{.sa_mask; .sa_flags} ∈ [--..--]
[20]{.sa_handler; .sa_sigaction} ∈ {0}
diff --git a/tests/libc/oracle/spawn_h.res.oracle b/tests/libc/oracle/spawn_h.res.oracle
index 01e765f74b0657f98adf4531504ffc36c9823a12..08866e9f1aa7e5bba94b7b62fabfa540d82d32a4 100644
--- a/tests/libc/oracle/spawn_h.res.oracle
+++ b/tests/libc/oracle/spawn_h.res.oracle
@@ -7,10 +7,10 @@
[eva] computing for function getopt <- main.
Called from spawn_h.c:36.
[eva] using specification for function getopt
+[eva:garbled-mix:assigns] spawn_h.c:36:
+ The specification of function getopt has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function getopt
-[eva:garbled-mix:write] spawn_h.c:36:
- Assigning imprecise value to opt.
- The imprecision originates from Library function {spawn_h.c:36}
[kernel:annot:missing-spec] spawn_h.c:43: Warning:
Neither code nor specification for function posix_spawn_file_actions_init,
generating default assigns. See -generated-spec-* options for more info
@@ -148,6 +148,8 @@
[eva] Done for function exit
[eva:alarm] spawn_h.c:82: Warning:
out of bounds read. assert \valid_read(argv + optind);
+[eva:garbled-mix:write] spawn_h.c:82:
+ Assigning imprecise value to file because of misaligned read of addresses.
[kernel:annot:missing-spec] spawn_h.c:82: Warning:
Neither code nor specification for function posix_spawnp,
generating default assigns. See -generated-spec-* options for more info
@@ -250,6 +252,11 @@
[eva] Done for function exit
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ spawn_h.c:36: assigns clause on addresses
+ (read 20 times, propagated 13 times)
+ garbled mix of &{S_argv; S_0_S_argv; S_1_S_argv}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
NON TERMINATING FUNCTION
diff --git a/tests/libc/oracle/unistd_h.0.res.oracle b/tests/libc/oracle/unistd_h.0.res.oracle
index 67d9d4401fef5a0c8a18b573223b6dc28430953b..745680bb6430b69a9fe9a4977cd4d1a4ce99c5c5 100644
--- a/tests/libc/oracle/unistd_h.0.res.oracle
+++ b/tests/libc/oracle/unistd_h.0.res.oracle
@@ -59,6 +59,9 @@
function execv: precondition 'valid_string_path' got status valid.
[eva] unistd_h.c:17:
function execv: precondition 'valid_string_argv0' got status valid.
+[eva:garbled-mix:assigns] unistd_h.c:17:
+ The specification of function execv has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function execv
[eva] computing for function execv <- main.
Called from unistd_h.c:17.
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index 00cf86ae56d1b4d20a9fb14008edb85e659e4024..50dffc4456619419bf73da47d9715b0a4ee6ba1c 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -44,10 +44,10 @@
"unknown-size"
],
"disabled": [
- "garbled-mix:assigns", "garbled-mix:read", "garbled-mix:summary",
- "garbled-mix:write", "invalid-assigns", "loop-unroll:auto",
- "loop-unroll:missing", "loop-unroll:missing:for",
- "loop-unroll:partial", "malloc:weak", "watchpoint"
+ "garbled-mix:assigns", "garbled-mix:summary", "garbled-mix:write",
+ "invalid-assigns", "loop-unroll:auto", "loop-unroll:missing",
+ "loop-unroll:missing:for", "loop-unroll:partial", "malloc:weak",
+ "watchpoint"
]
}
},
diff --git a/tests/slicing/oracle/loops.10.res.oracle b/tests/slicing/oracle/loops.10.res.oracle
index 8b074bf06abdd613754931d1720a4884ceb3f673..7ba1874acead31fd20c084a227d3c52fa55f6fac 100644
--- a/tests/slicing/oracle/loops.10.res.oracle
+++ b/tests/slicing/oracle/loops.10.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/slicing/oracle/loops.19.res.oracle b/tests/slicing/oracle/loops.19.res.oracle
index 34457cfad25d07e2868e3518708480733f7473fa..0998264ade13e755871e320c9cd50baadbcf6c06 100644
--- a/tests/slicing/oracle/loops.19.res.oracle
+++ b/tests/slicing/oracle/loops.19.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/slicing/oracle/loops.20.res.oracle b/tests/slicing/oracle/loops.20.res.oracle
index 27d8cdb835562da76ec04f76f72017aa7aaba1b0..6e18bd872d2d86d795df7d8d77af2cc984dd6a76 100644
--- a/tests/slicing/oracle/loops.20.res.oracle
+++ b/tests/slicing/oracle/loops.20.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/slicing/oracle/loops.21.res.oracle b/tests/slicing/oracle/loops.21.res.oracle
index 9adf543884b06243c38d066d660dce7d01610e18..8636ad07b17046ce79ca5ca1ab0eb519c01bf81c 100644
--- a/tests/slicing/oracle/loops.21.res.oracle
+++ b/tests/slicing/oracle/loops.21.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/slicing/oracle/loops.22.res.oracle b/tests/slicing/oracle/loops.22.res.oracle
index 7d41e9a40cdb66446abcee9448378d0a0ddbef06..3313fbc32d943908d3b6701ed97fdd379ff18096 100644
--- a/tests/slicing/oracle/loops.22.res.oracle
+++ b/tests/slicing/oracle/loops.22.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/slicing/oracle/loops.23.res.oracle b/tests/slicing/oracle/loops.23.res.oracle
index 24eb43a90cba0b80c99d1795f5b1566d2443857b..ae8f97a78fc3c8b783c571ad7895d4ad8ea25d81 100644
--- a/tests/slicing/oracle/loops.23.res.oracle
+++ b/tests/slicing/oracle/loops.23.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/slicing/oracle/loops.8.res.oracle b/tests/slicing/oracle/loops.8.res.oracle
index 3c7880c3af1ec26d5a6c78fa64382ce48b28eaf5..f1d9bbd86696821f18cab14e3276c13346963cb5 100644
--- a/tests/slicing/oracle/loops.8.res.oracle
+++ b/tests/slicing/oracle/loops.8.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/slicing/oracle/loops.9.res.oracle b/tests/slicing/oracle/loops.9.res.oracle
index abc0b21b556922c6b9b00615dfba3fe01f412bbb..a2caa35921cfccd62af77a1b13f943464086f2cd 100644
--- a/tests/slicing/oracle/loops.9.res.oracle
+++ b/tests/slicing/oracle/loops.9.res.oracle
@@ -12,6 +12,9 @@
[eva] computing for function may_write_Y_from_Z <- main.
Called from loops.i:199.
[eva] using specification for function may_write_Y_from_Z
+[eva:garbled-mix:assigns] loops.i:199:
+ The specification of function may_write_Y_from_Z
+ has generated a garbled mix of addresses for assigns clause *p.
[eva] Done for function may_write_Y_from_Z
[eva] computing for function loop <- main.
Called from loops.i:202.
diff --git a/tests/value/oracle/addition.res.oracle b/tests/value/oracle/addition.res.oracle
index bb68a90bfb7a65ffac5bbbed34e7e8fa86d5bc50..394936b8b9df05a61b4935cb721c0e66380efa36 100644
--- a/tests/value/oracle/addition.res.oracle
+++ b/tests/value/oracle/addition.res.oracle
@@ -57,27 +57,23 @@
[eva:alarm] addition.i:34: Warning:
signed overflow. assert &p2 - &p3 ≤ 2147483647;
[eva:garbled-mix:write] addition.i:34: Warning:
- Assigning imprecise value to p1.
- The imprecision originates from Arithmetic {addition.i:34}
+ Assigning imprecise value to p1 because of arithmetic operation on addresses.
[eva:alarm] addition.i:36: Warning:
pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva:garbled-mix:write] addition.i:36: Warning:
- Assigning imprecise value to p2.
- The imprecision originates from Arithmetic {addition.i:36}
+ Assigning imprecise value to p2 because of arithmetic operation on addresses.
[eva:alarm] addition.i:38: Warning:
pointer downcast. assert (unsigned int)(&p1) ≤ 127;
[eva:alarm] addition.i:38: Warning:
pointer downcast. assert (unsigned int)(&t[(char)(&p1)]) ≤ 2147483647;
[eva:garbled-mix:write] addition.i:38: Warning:
- Assigning imprecise value to p3.
- The imprecision originates from Arithmetic {addition.i:38}
+ Assigning imprecise value to p3 because of arithmetic operation on addresses.
[eva:alarm] addition.i:40: Warning:
pointer downcast. assert (unsigned int)(&p1) ≤ 127;
[eva:alarm] addition.i:40: Warning:
pointer downcast. assert (unsigned int)(&tt[(char)(&p1)].a) ≤ 2147483647;
[eva:garbled-mix:write] addition.i:40: Warning:
- Assigning imprecise value to p4.
- The imprecision originates from Arithmetic {addition.i:40}
+ Assigning imprecise value to p4 because of arithmetic operation on addresses.
[eva:alarm] addition.i:42: Warning:
pointer downcast. assert (unsigned int)(&p1) ≤ 127;
[eva:alarm] addition.i:42: Warning:
@@ -86,24 +82,21 @@
pointer downcast.
assert (unsigned int)(&ttt[(char)(&p1)][(char)(&p2)]) ≤ 2147483647;
[eva:garbled-mix:write] addition.i:42: Warning:
- Assigning imprecise value to p5.
- The imprecision originates from Arithmetic {addition.i:42}
+ Assigning imprecise value to p5 because of arithmetic operation on addresses.
[eva:alarm] addition.i:44: Warning:
pointer downcast. assert (unsigned int)(&p1) ≤ 127;
[eva:alarm] addition.i:44: Warning:
pointer downcast.
assert (unsigned int)(&ttt[(char)(&p1)][u2]) ≤ 2147483647;
[eva:garbled-mix:write] addition.i:44: Warning:
- Assigning imprecise value to p6.
- The imprecision originates from Arithmetic {addition.i:44}
+ Assigning imprecise value to p6 because of arithmetic operation on addresses.
[eva:alarm] addition.i:46: Warning:
pointer downcast. assert (unsigned int)(&p2) ≤ 127;
[eva:alarm] addition.i:46: Warning:
pointer downcast.
assert (unsigned int)(&ttt[u2][(char)(&p2)]) ≤ 2147483647;
[eva:garbled-mix:write] addition.i:46: Warning:
- Assigning imprecise value to p7.
- The imprecision originates from Arithmetic {addition.i:46}
+ Assigning imprecise value to p7 because of arithmetic operation on addresses.
[eva:alarm] addition.i:48: Warning:
pointer comparison.
assert \pointer_comparable((void *)(&p1 + 1), (void *)(&p2));
@@ -114,57 +107,37 @@
[eva:alarm] addition.i:50: Warning:
signed overflow. assert (int)(&p1) / 2 ≤ 2147483647;
[eva:garbled-mix:write] addition.i:50: Warning:
- Assigning imprecise value to p9.
- The imprecision originates from Arithmetic {addition.i:50}
+ Assigning imprecise value to p9 because of arithmetic operation on addresses.
[eva:alarm] addition.i:52: Warning:
pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva:garbled-mix:write] addition.i:52: Warning:
- Assigning imprecise value to p10.
- The imprecision originates from Arithmetic {addition.i:52}
+ Assigning imprecise value to p10
+ because of arithmetic operation on addresses.
[eva:alarm] addition.i:56: Warning:
pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva:alarm] addition.i:56: Warning:
pointer downcast. assert (unsigned int)(&p2) ≤ 2147483647;
[eva:garbled-mix:write] addition.i:56: Warning:
- Assigning imprecise value to p12.
- The imprecision originates from Arithmetic {addition.i:56}
+ Assigning imprecise value to p12
+ because of arithmetic operation on addresses.
[eva:alarm] addition.i:59: Warning:
signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
[eva:alarm] addition.i:59: Warning:
signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
[eva:garbled-mix:write] addition.i:59: Warning:
- Assigning imprecise value to p13.
- The imprecision originates from Misaligned {addition.i:59}
+ Assigning imprecise value to p13 because of misaligned read of addresses.
[eva:alarm] addition.i:61: Warning:
signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
[eva:alarm] addition.i:61: Warning:
signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
[eva:garbled-mix:write] addition.i:61: Warning:
- Assigning imprecise value to p14.
- The imprecision originates from Misaligned {addition.i:61}
+ Assigning imprecise value to p14 because of misaligned read of addresses.
[eva:alarm] addition.i:66: Warning:
out of bounds read. assert \valid_read(*((int **)45));
[eva] addition.i:87: Frama_C_show_each_1: [-10..15]
[eva] addition.i:88: assertion got status valid.
[eva] Recording results for main
[eva] Done for function main
-[eva:garbled-mix:summary] Warning:
- Garbled mix generated during analysis:
- {{ garbled mix of &{p3} (origin: Arithmetic {addition.i:34}) }}
- {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:34}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:36}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:38}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:40}) }}
- {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:42}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:42}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:44}) }}
- {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:46}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:50}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}
- {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:56}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:56}) }}
- {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
- {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
[scope:rm_asserts] removing 9 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
@@ -186,8 +159,10 @@
p10 ∈ {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}
p11 ∈ [-2147483648..0],0%4
p12 ∈ {{ garbled mix of &{p1; p2} (origin: Arithmetic {addition.i:56}) }}
- p13 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
- p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
+ p13 ∈
+ {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
+ p14 ∈
+ {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
p15 ∈ {-1}
p16 ∈ {2949122}
p17 ∈ {-2147483648; 0}
@@ -390,23 +365,6 @@
[eva] addition.i:87: Frama_C_show_each_1: [-10..15]
[eva] Recording results for main
[eva] Done for function main
-[eva:garbled-mix:summary] Warning:
- Garbled mix generated during analysis:
- {{ garbled mix of &{p3} (origin: Arithmetic {addition.i:34}) }}
- {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:34}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:36}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:38}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:40}) }}
- {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:42}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:42}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:44}) }}
- {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:46}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:50}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}
- {{ garbled mix of &{p2} (origin: Arithmetic {addition.i:56}) }}
- {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:56}) }}
- {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
- {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
[scope:rm_asserts] removing 9 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
@@ -429,8 +387,10 @@
p10 ∈ {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}
p11 ∈ [-2147483648..0],0%4
p12 ∈ {{ garbled mix of &{p1; p2} (origin: Arithmetic {addition.i:56}) }}
- p13 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
- p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
+ p13 ∈
+ {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
+ p14 ∈
+ {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
p15 ∈ {-1}
p16 ∈ {2; 2949122; 3014658}
p17 ∈ {-2147483648; 0}
diff --git a/tests/value/oracle/arith_pointer.res.oracle b/tests/value/oracle/arith_pointer.res.oracle
index 2397783f775ed506dd5127623508426785d8e2c2..2261d0849e3e6080bb275a5c6d6ea2a23ef5ef62 100644
--- a/tests/value/oracle/arith_pointer.res.oracle
+++ b/tests/value/oracle/arith_pointer.res.oracle
@@ -25,17 +25,13 @@
[eva:alarm] arith_pointer.c:54: Warning:
pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:garbled-mix:write] arith_pointer.c:54:
- Assigning imprecise value to p1.
- The imprecision originates from Arithmetic {arith_pointer.c:54}
+ Assigning imprecise value to p1 because of arithmetic operation on addresses.
[eva:alarm] arith_pointer.c:56: Warning:
pointer subtraction. assert \base_addr(p2) ≡ \base_addr(p1);
[eva:alarm] arith_pointer.c:56: Warning:
signed overflow. assert -2147483648 ≤ p2 - p1;
[eva:alarm] arith_pointer.c:56: Warning:
signed overflow. assert p2 - p1 ≤ 2147483647;
-[eva:garbled-mix:write] arith_pointer.c:56:
- Assigning imprecise value to d.
- The imprecision originates from Arithmetic {arith_pointer.c:54}
[eva] arith_pointer.c:57:
Frama_C_show_each:
{{ garbled mix of &{x} (origin: Arithmetic {arith_pointer.c:54}) }}
@@ -46,6 +42,10 @@
[eva] Done for function main2
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ arith_pointer.c:54: arithmetic operation on addresses
+ (read 2 times, propagated 2 times) garbled mix of &{x}
[eva] arith_pointer.c:30:
assertion 'Eva,differing_blocks' got final status invalid.
[eva] ====== VALUES COMPUTED ======
@@ -117,8 +117,7 @@
[eva:alarm] arith_pointer.c:30: Warning:
signed overflow. assert p1 - p2 ≤ 2147483647;
[eva:garbled-mix:write] arith_pointer.c:30:
- Assigning imprecise value to d.
- The imprecision originates from Arithmetic {arith_pointer.c:30}
+ Assigning imprecise value to d because of arithmetic operation on addresses.
[eva] arith_pointer.c:31:
Frama_C_show_each:
{{ garbled mix of &{x; y} (origin: Arithmetic {arith_pointer.c:30}) }}
@@ -129,8 +128,7 @@
[eva:alarm] arith_pointer.c:49: Warning:
signed overflow. assert p2 - p1 ≤ 2147483647;
[eva:garbled-mix:write] arith_pointer.c:49:
- Assigning imprecise value to d.
- The imprecision originates from Arithmetic {arith_pointer.c:49}
+ Assigning imprecise value to d because of arithmetic operation on addresses.
[eva] arith_pointer.c:50:
Frama_C_show_each:
{{ garbled mix of &{x; y} (origin: Arithmetic {arith_pointer.c:49}) }}
@@ -139,8 +137,7 @@
[eva:alarm] arith_pointer.c:51: Warning:
signed overflow. assert p2 - p2 ≤ 2147483647;
[eva:garbled-mix:write] arith_pointer.c:51:
- Assigning imprecise value to d.
- The imprecision originates from Arithmetic {arith_pointer.c:51}
+ Assigning imprecise value to d because of arithmetic operation on addresses.
[eva] arith_pointer.c:52:
Frama_C_show_each:
{{ garbled mix of &{x; y} (origin: Arithmetic {arith_pointer.c:51}) }}
@@ -150,16 +147,24 @@
signed overflow. assert -2147483648 ≤ p2 - p1;
[eva:alarm] arith_pointer.c:56: Warning:
signed overflow. assert p2 - p1 ≤ 2147483647;
-[eva:garbled-mix:write] arith_pointer.c:56:
- Assigning imprecise value to d.
- The imprecision originates from Arithmetic
[eva] arith_pointer.c:57:
- Frama_C_show_each: {{ garbled mix of &{x} (origin: Arithmetic) }}
+ Frama_C_show_each:
+ {{ garbled mix of &{x} (origin: Arithmetic {arith_pointer.c:54}) }}
[eva] arith_pointer.c:64: Frama_C_show_each: [-3..5]
[eva] Recording results for main2
[eva] Done for function main2
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ arith_pointer.c:54: arithmetic operation on addresses
+ (read 2 times, propagated 2 times) garbled mix of &{x}
+ arith_pointer.c:30: arithmetic operation on addresses
+ (read 1 times, propagated 1 times) garbled mix of &{x; y}
+ arith_pointer.c:49: arithmetic operation on addresses
+ (read 1 times, propagated 1 times) garbled mix of &{x; y}
+ arith_pointer.c:51: arithmetic operation on addresses
+ (read 1 times, propagated 1 times) garbled mix of &{x; y}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main1:
t[0..1] ∈ {-3}
diff --git a/tests/value/oracle/assign-leaf-indirect.res.oracle b/tests/value/oracle/assign-leaf-indirect.res.oracle
index d1632315bcb6bce72993ab83ee145e4ba4229247..4d4a939a92b3718e5132e1408fe9eef94151bfa8 100644
--- a/tests/value/oracle/assign-leaf-indirect.res.oracle
+++ b/tests/value/oracle/assign-leaf-indirect.res.oracle
@@ -9,6 +9,9 @@
[eva] computing for function f <- main.
Called from assign-leaf-indirect.i:8.
[eva] using specification for function f
+[eva:garbled-mix:assigns] assign-leaf-indirect.i:8:
+ The specification of function f has generated a garbled mix of addresses
+ for assigns clause y.
[eva] Done for function f
[eva] computing for function g <- main.
Called from assign-leaf-indirect.i:9.
diff --git a/tests/value/oracle/assigns.res.oracle b/tests/value/oracle/assigns.res.oracle
index 744d7aab558ef0bcada92ce5326773be1186e880..110f45908bae6a5907c06fea0ab8efd97a7332c5 100644
--- a/tests/value/oracle/assigns.res.oracle
+++ b/tests/value/oracle/assigns.res.oracle
@@ -50,6 +50,9 @@
signed overflow. assert -2147483648 ≤ 2 * (int)(&T);
[eva:alarm] assigns.i:51: Warning:
signed overflow. assert 2 * (int)(&T) ≤ 2147483647;
+[eva:garbled-mix:write] assigns.i:51:
+ Assigning imprecise value to len
+ because of arithmetic operation on addresses.
[eva] computing for function g <- main1 <- main.
Called from assigns.i:51.
[eva] using specification for function g
@@ -60,6 +63,8 @@
signed overflow. assert -2147483648 ≤ 2 * (int)(&t3);
[eva:alarm] assigns.i:52: Warning:
signed overflow. assert 2 * (int)(&t3) ≤ 2147483647;
+[eva:garbled-mix:write] assigns.i:52:
+ Assigning imprecise value to p because of arithmetic operation on addresses.
[eva] computing for function h <- main1 <- main.
Called from assigns.i:52.
[eva] using specification for function h
diff --git a/tests/value/oracle/assigns_from.res.oracle b/tests/value/oracle/assigns_from.res.oracle
index 002087f31ba8abd39638d82d19e0589a787a698a..be60cecebede8380f7df749aecdd254fe0bcc968 100644
--- a/tests/value/oracle/assigns_from.res.oracle
+++ b/tests/value/oracle/assigns_from.res.oracle
@@ -298,6 +298,9 @@
[eva] computing for function f18 <- main18 <- main.
Called from assigns_from.i:215.
[eva] using specification for function f18
+[eva:garbled-mix:assigns] assigns_from.i:215:
+ The specification of function f18 has generated a garbled mix of addresses
+ for assigns clause *x.
[eva] Done for function f18
[eva] Recording results for main18
[from] Computing for function main18
@@ -370,17 +373,17 @@
base_a ∈ {17}
a_0.addr ∈
{{ garbled mix of &{base_a; base_b}
- (origin: Misaligned {assigns_from.i:215}) }}
+ (origin: Misaligned read {assigns_from.i:215}) }}
.i ∈
{{ garbled mix of &{base_a; base_b}
- (origin: Misaligned {assigns_from.i:215}) }} or UNINITIALIZED
+ (origin: Misaligned read {assigns_from.i:215}) }} or UNINITIALIZED
base_b ∈ {11}
b.addr ∈
{{ garbled mix of &{base_a; base_b}
- (origin: Misaligned {assigns_from.i:215}) }}
+ (origin: Misaligned read {assigns_from.i:215}) }}
.i ∈
{{ garbled mix of &{base_a; base_b}
- (origin: Misaligned {assigns_from.i:215}) }} or UNINITIALIZED
+ (origin: Misaligned read {assigns_from.i:215}) }} or UNINITIALIZED
[eva:final-states] Values at end of function main2:
a[0..2] ∈ {0}
[3] ∈ {2}
diff --git a/tests/value/oracle/backward_add_ptr.res.oracle b/tests/value/oracle/backward_add_ptr.res.oracle
index aa5bb85d7250e40cd2b703b4a4807dcc83115c30..35d0fce388bc2f9a9d8e16c79392d358cc71385b 100644
--- a/tests/value/oracle/backward_add_ptr.res.oracle
+++ b/tests/value/oracle/backward_add_ptr.res.oracle
@@ -40,16 +40,10 @@
[eva] computing for function gm <- main3 <- main.
Called from backward_add_ptr.c:75.
[eva:garbled-mix:write] backward_add_ptr.c:68: Warning:
- Assigning imprecise value to __retres.
- The imprecision originates from Arithmetic {backward_add_ptr.c:68}
-[eva:garbled-mix:write] backward_add_ptr.c:68: Warning:
- Assigning imprecise value to \result<gm>.
- The imprecision originates from Arithmetic {backward_add_ptr.c:68}
+ Assigning imprecise value to __retres
+ because of arithmetic operation on addresses.
[eva] Recording results for gm
[eva] Done for function gm
-[eva:garbled-mix:write] backward_add_ptr.c:75: Warning:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {backward_add_ptr.c:68}
[eva:alarm] backward_add_ptr.c:81: Warning:
out of bounds read. assert \valid_read(p + (uintptr_t)q);
[eva] backward_add_ptr.c:82:
@@ -62,18 +56,12 @@
{{ NULL + {0; 1; 2; 3} ; &a + [-4294967295..3] }},
{{ NULL + [0..4294967295] ; &b }}
[eva] backward_add_ptr.c:91: Reusing old results for call to gm
-[eva:garbled-mix:write] backward_add_ptr.c:91: Warning:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {backward_add_ptr.c:68}
[eva:alarm] backward_add_ptr.c:96: Warning:
out of bounds read. assert \valid_read(p + (uintptr_t)q);
[eva] computing for function gm <- main3 <- main.
Called from backward_add_ptr.c:100.
[eva] Recording results for gm
[eva] Done for function gm
-[eva:garbled-mix:write] backward_add_ptr.c:100: Warning:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {backward_add_ptr.c:68}
[eva:alarm] backward_add_ptr.c:106: Warning:
out of bounds read. assert \valid_read(p + (uintptr_t)q);
[eva] backward_add_ptr.c:107:
@@ -82,9 +70,6 @@
(origin: Arithmetic {backward_add_ptr.c:68}) }},
{{ NULL + [0..4294967295] ; &b }}
[eva] backward_add_ptr.c:110: Reusing old results for call to gm
-[eva:garbled-mix:write] backward_add_ptr.c:110: Warning:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {backward_add_ptr.c:68}
[eva:alarm] backward_add_ptr.c:115: Warning:
out of bounds read. assert \valid_read((char *)p + (uintptr_t)q);
[eva] backward_add_ptr.c:116: Frama_C_show_each_GM_only_c: {0}, {{ &c }}
@@ -94,9 +79,6 @@
Frama_C_show_each_GM_only_b:
{{ &b + [-17179869180..0],0%4 }}, [0..4294967295]
[eva] backward_add_ptr.c:125: Reusing old results for call to gm
-[eva:garbled-mix:write] backward_add_ptr.c:125: Warning:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {backward_add_ptr.c:68}
[eva:alarm] backward_add_ptr.c:130: Warning:
out of bounds read. assert \valid_read((char *)p + (uintptr_t)q);
[eva:alarm] backward_add_ptr.c:136: Warning:
@@ -114,19 +96,10 @@
Called from backward_add_ptr.c:145.
[eva] Recording results for gm
[eva] Done for function gm
-[eva:garbled-mix:write] backward_add_ptr.c:145: Warning:
- Assigning imprecise value to tmp_0.
- The imprecision originates from Arithmetic {backward_add_ptr.c:68}
-[eva:garbled-mix:write] backward_add_ptr.c:145: Warning:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {backward_add_ptr.c:68}
[eva] computing for function gm <- main4 <- main.
Called from backward_add_ptr.c:146.
[eva] Recording results for gm
[eva] Done for function gm
-[eva:garbled-mix:write] backward_add_ptr.c:146: Warning:
- Assigning imprecise value to q.
- The imprecision originates from Arithmetic {backward_add_ptr.c:68}
[eva:alarm] backward_add_ptr.c:150: Warning:
out of bounds read. assert \valid_read(p + (uintptr_t)q);
[eva] backward_add_ptr.c:151:
@@ -143,16 +116,10 @@
(origin: Arithmetic {backward_add_ptr.c:68}) }},
[0..4294967295]
[eva] backward_add_ptr.c:160: Reusing old results for call to gm
-[eva:garbled-mix:write] backward_add_ptr.c:160: Warning:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {backward_add_ptr.c:68}
[eva] computing for function gm <- main4 <- main.
Called from backward_add_ptr.c:161.
[eva] Recording results for gm
[eva] Done for function gm
-[eva:garbled-mix:write] backward_add_ptr.c:161: Warning:
- Assigning imprecise value to q.
- The imprecision originates from Arithmetic {backward_add_ptr.c:68}
[eva:alarm] backward_add_ptr.c:165: Warning:
out of bounds read. assert \valid_read((char *)p + (uintptr_t)q);
[eva] backward_add_ptr.c:166:
@@ -182,31 +149,9 @@
[eva] Recording results for main
[eva] Done for function main
[eva:garbled-mix:summary] Warning:
- Garbled mix generated during analysis:
- {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:25}) }}
- {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:25}) }}
- {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:32}) }}
- {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:32}) }}
- {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:38}) }}
- {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:38}) }}
- {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:54}) }}
- {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:54}) }}
- {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:60}) }}
- {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:60}) }}
- {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:68}) }}
- {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:81}) }}
- {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:87}) }}
- {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:96}) }}
- {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:68}) }}
- {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:106}) }}
- {{ garbled mix of &{c} (origin: Arithmetic {backward_add_ptr.c:115}) }}
- {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:115}) }}
- {{ garbled mix of &{c} (origin: Arithmetic {backward_add_ptr.c:121}) }}
- {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:130}) }}
- {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:136}) }}
- {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:68}) }}
- {{ garbled mix of &{c} (origin: Arithmetic {backward_add_ptr.c:68}) }}
- {{ garbled mix of &{b; c} (origin: Arithmetic {backward_add_ptr.c:68}) }}
+ Origins of garbled mix generated during analysis:
+ backward_add_ptr.c:68: arithmetic operation on addresses
+ (read 81 times, propagated 20 times) garbled mix of &{a; b; a; b; c}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function gm:
__retres ∈
diff --git a/tests/value/oracle/behaviors1.res.oracle b/tests/value/oracle/behaviors1.res.oracle
index 980bd317335a3fc4d47b65acd11b2e391f2e1c3b..6266ee5cf357f02688368950dbcf890d81a35c02 100644
--- a/tests/value/oracle/behaviors1.res.oracle
+++ b/tests/value/oracle/behaviors1.res.oracle
@@ -305,22 +305,16 @@
[eva] computing for function f <- test_assigns <- main.
Called from behaviors1.i:473.
[eva] using specification for function f
+[eva:garbled-mix:assigns] behaviors1.i:473:
+ The specification of function f has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function f
-[eva:garbled-mix:write] behaviors1.i:473:
- Assigning imprecise value to tmp.
- The imprecision originates from Library function {behaviors1.i:473}
-[eva:garbled-mix:write] behaviors1.i:473:
- Assigning imprecise value to p1.
- The imprecision originates from Library function {behaviors1.i:473}
[eva] computing for function f <- test_assigns <- main.
Called from behaviors1.i:474.
+[eva:garbled-mix:assigns] behaviors1.i:474:
+ The specification of function f has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function f
-[eva:garbled-mix:write] behaviors1.i:474:
- Assigning imprecise value to tmp_0.
- The imprecision originates from Library function {behaviors1.i:474}
-[eva:garbled-mix:write] behaviors1.i:474:
- Assigning imprecise value to p2.
- The imprecision originates from Library function {behaviors1.i:474}
[eva] computing for function f <- test_assigns <- main.
Called from behaviors1.i:475.
[eva] Done for function f
@@ -452,6 +446,12 @@
[eva] Done for function test_narrow
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ behaviors1.i:473: assigns clause on addresses
+ (read 1 times, propagated 3 times) garbled mix of &{a}
+ behaviors1.i:474: assigns clause on addresses
+ (read 1 times, propagated 3 times) garbled mix of &{b}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function test_123_comp_2345_comp_disj:
a ∈ [--..--]
diff --git a/tests/value/oracle/bitfield.res.oracle b/tests/value/oracle/bitfield.res.oracle
index 45acf78958063456e7bd3d636503dc555b6f337a..cae0f2d2936a0ef67c6846b8e569f6073fa67bb2 100644
--- a/tests/value/oracle/bitfield.res.oracle
+++ b/tests/value/oracle/bitfield.res.oracle
@@ -31,8 +31,8 @@
[eva:alarm] bitfield.i:123: Warning:
pointer downcast. assert (unsigned int)(&v) ≤ 2147483647;
[eva:garbled-mix:write] bitfield.i:123:
- Assigning imprecise value to v.c.
- The imprecision originates from Arithmetic {bitfield.i:123}
+ Assigning imprecise value to v.c
+ because of arithmetic operation on addresses.
[eva:alarm] bitfield.i:124: Warning:
pointer downcast. assert (unsigned int)(&v + 1) ≤ 2147483647;
[eva:alarm] bitfield.i:125: Warning:
@@ -83,8 +83,8 @@
[eva:alarm] bitfield.i:130: Warning:
pointer downcast. assert (unsigned int)(&v + 1) ≤ 2147483647;
[eva:garbled-mix:write] bitfield.i:130:
- Assigning imprecise value to h.c.
- The imprecision originates from Arithmetic {bitfield.i:130}
+ Assigning imprecise value to h.c
+ because of arithmetic operation on addresses.
[eva] computing for function return_8 <- main_old <- main.
Called from bitfield.i:133.
[eva] Recording results for return_8
@@ -105,31 +105,31 @@
[eva] computing for function leaf <- imprecise_bts_1671 <- main.
Called from bitfield.i:70.
[eva] using specification for function leaf
+[eva:garbled-mix:assigns] bitfield.i:70:
+ The specification of function leaf has generated a garbled mix of addresses
+ for assigns clause *p1.
[eva] Done for function leaf
[eva] bitfield.i:71:
Frama_C_show_each:
- {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
[eva] bitfield.i:73:
Frama_C_show_each:
- .next ∈ {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ .next ∈ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
.bitf ∈ {0}
.[bits 65 to 95] ∈
- {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
-[eva:garbled-mix:write] bitfield.i:74:
- Assigning imprecise value to c.
- The imprecision originates from Misaligned {bitfield.i:70}
+ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
[eva] bitfield.i:69: starting to merge loop iterations
[eva] computing for function leaf <- imprecise_bts_1671 <- main.
Called from bitfield.i:70.
[eva] Done for function leaf
[eva] bitfield.i:71:
Frama_C_show_each:
- {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
[eva:alarm] bitfield.i:72: Warning:
out of bounds write. assert \valid(&c->bitf);
[eva] bitfield.i:73:
Frama_C_show_each:
- {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
[eva:alarm] bitfield.i:74: Warning:
out of bounds read. assert \valid_read(&c->next.next);
[eva] computing for function leaf <- imprecise_bts_1671 <- main.
@@ -187,8 +187,8 @@
G ∈ {1}
H ∈ {0}
b ∈ {0}
- c ∈ {{ garbled mix of &{b; ee} (origin: Misaligned {bitfield.i:70}) }}
- ee ∈ {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ c ∈ {{ garbled mix of &{b; ee} (origin: Misaligned read {bitfield.i:70}) }}
+ ee ∈ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
foo ∈ [--..--]
y.v0_3 ∈ [--..--]
.v4 ∈ {0}
@@ -207,6 +207,10 @@
[eva] Done for function char_short
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ bitfield.i:70: misaligned read of addresses
+ (read 5 times, propagated 7 times) garbled mix of &{b; ee}
[eva] bitfield.i:102: assertion 'Eva,initialization' got final status invalid.
[scope:rm_asserts] removing 1 assertion(s)
[eva] ====== VALUES COMPUTED ======
@@ -225,8 +229,9 @@
r ∈ {1}
[eva:final-states] Values at end of function imprecise_bts_1671:
b ∈ {0}
- c ∈ {{ garbled mix of &{b; ee} (origin: Misaligned {bitfield.i:70}) }}
- ee ∈ {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ c ∈
+ {{ garbled mix of &{b; ee} (origin: Misaligned read {bitfield.i:70}) }}
+ ee ∈ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
[eva:final-states] Values at end of function logic:
y.v0_3 ∈ [--..--]
.v4 ∈ {0}
@@ -276,8 +281,9 @@
G ∈ {1}
H ∈ {0}
b ∈ {0}
- c ∈ {{ garbled mix of &{b; ee} (origin: Misaligned {bitfield.i:70}) }}
- ee ∈ {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ c ∈
+ {{ garbled mix of &{b; ee} (origin: Misaligned read {bitfield.i:70}) }}
+ ee ∈ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
y.v0_3 ∈ [--..--]
.v4 ∈ {0}
.v5_31 ∈ [--..--]
diff --git a/tests/value/oracle/bitwise_pointer.0.res.oracle b/tests/value/oracle/bitwise_pointer.0.res.oracle
index c45fec9776b8c8ee44359a0cbb5211514ab29f2e..6b52884383aab14b10f97928c0c5f0ad1b923ba5 100644
--- a/tests/value/oracle/bitwise_pointer.0.res.oracle
+++ b/tests/value/oracle/bitwise_pointer.0.res.oracle
@@ -32,19 +32,23 @@
[eva:alarm] bitwise_pointer.i:18: Warning:
pointer downcast. assert (unsigned int)(&t[7]) ≤ 2147483647;
[eva:garbled-mix:write] bitwise_pointer.i:18:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {bitwise_pointer.i:18}
+ Assigning imprecise value to p because of arithmetic operation on addresses.
[eva:alarm] bitwise_pointer.i:19: Warning:
out of bounds write. assert \valid(p);
[eva:alarm] bitwise_pointer.i:22: Warning:
pointer downcast. assert (unsigned int)(&t1[mask]) ≤ 2147483647;
[eva:garbled-mix:write] bitwise_pointer.i:22:
- Assigning imprecise value to p1.
- The imprecision originates from Arithmetic {bitwise_pointer.i:22}
+ Assigning imprecise value to p1 because of arithmetic operation on addresses.
[eva:alarm] bitwise_pointer.i:23: Warning:
out of bounds write. assert \valid(p1);
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ bitwise_pointer.i:18: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) garbled mix of &{t}
+ bitwise_pointer.i:22: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) garbled mix of &{t1}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
t[0] ∈ {0; 5}
diff --git a/tests/value/oracle/bitwise_pointer.1.res.oracle b/tests/value/oracle/bitwise_pointer.1.res.oracle
index c45fec9776b8c8ee44359a0cbb5211514ab29f2e..6b52884383aab14b10f97928c0c5f0ad1b923ba5 100644
--- a/tests/value/oracle/bitwise_pointer.1.res.oracle
+++ b/tests/value/oracle/bitwise_pointer.1.res.oracle
@@ -32,19 +32,23 @@
[eva:alarm] bitwise_pointer.i:18: Warning:
pointer downcast. assert (unsigned int)(&t[7]) ≤ 2147483647;
[eva:garbled-mix:write] bitwise_pointer.i:18:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {bitwise_pointer.i:18}
+ Assigning imprecise value to p because of arithmetic operation on addresses.
[eva:alarm] bitwise_pointer.i:19: Warning:
out of bounds write. assert \valid(p);
[eva:alarm] bitwise_pointer.i:22: Warning:
pointer downcast. assert (unsigned int)(&t1[mask]) ≤ 2147483647;
[eva:garbled-mix:write] bitwise_pointer.i:22:
- Assigning imprecise value to p1.
- The imprecision originates from Arithmetic {bitwise_pointer.i:22}
+ Assigning imprecise value to p1 because of arithmetic operation on addresses.
[eva:alarm] bitwise_pointer.i:23: Warning:
out of bounds write. assert \valid(p1);
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ bitwise_pointer.i:18: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) garbled mix of &{t}
+ bitwise_pointer.i:22: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) garbled mix of &{t1}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
t[0] ∈ {0; 5}
diff --git a/tests/value/oracle/context_free.res.oracle b/tests/value/oracle/context_free.res.oracle
index ded8a88ce5e55edf2670cfc8359f746cb22b25e7..ba68025f931ff6945455604a0f240ca29897ba3a 100644
--- a/tests/value/oracle/context_free.res.oracle
+++ b/tests/value/oracle/context_free.res.oracle
@@ -77,26 +77,11 @@
[eva:initial-state] creating variable S_1_S_vvv with imprecise size (type void)
[eva:initial-state] creating variable S_vv with imprecise size (type void)
[eva:alarm] context_free.i:46: Warning: out of bounds write. assert \valid(p);
-[eva:garbled-mix:write] context_free.i:51:
- Assigning imprecise value to vv.
- The imprecision originates from Well
[eva:alarm] context_free.i:52: Warning: out of bounds write. assert \valid(vvv);
-[eva:garbled-mix:write] context_free.i:52:
- Assigning imprecise value to *vvv (pointing to S_vvv with offsets {0}).
- The imprecision originates from Well
-[eva:garbled-mix:write] context_free.i:54:
- Assigning imprecise value to uu.u1.
- The imprecision originates from Well
[eva:alarm] context_free.i:56: Warning:
out of bounds write. assert \valid(ta + 1);
-[eva:garbled-mix:write] context_free.i:58:
- Assigning imprecise value to pvoid.
- The imprecision originates from Well
[eva:alarm] context_free.i:59: Warning:
out of bounds write. assert \valid(pvoid);
-[eva:garbled-mix:write] context_free.i:60:
- Assigning imprecise value to pvoid.
- The imprecision originates from Well
[eva:alarm] context_free.i:61: Warning:
out of bounds write. assert \valid(pvoid);
[eva:alarm] context_free.i:61: Warning:
@@ -105,6 +90,10 @@
pointer to function with incompatible type. assert \valid_function(g);
[eva] Recording results for f
[eva] Done for function f
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ Initial state (read 9 times, propagated 5 times)
+ garbled mix of &{WELL_uu; S_p_svoid; S_qvoid; S_0_S_vvv; S_vv}
[eva] context_free.i:62:
assertion 'Eva,function_pointer' got final status invalid.
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/conversion.res.oracle b/tests/value/oracle/conversion.res.oracle
index a5eac26eb5864977bc397b24838f33c695313822..8e34af8ffa8cd0bbe61d85a13d38a00d5badd442 100644
--- a/tests/value/oracle/conversion.res.oracle
+++ b/tests/value/oracle/conversion.res.oracle
@@ -163,8 +163,7 @@
[eva:alarm] conversion.i:39: Warning:
non-finite float value. assert \is_finite(*((float *)(&x)));
[eva:garbled-mix:write] conversion.i:39:
- Assigning imprecise value to f.
- The imprecision originates from Arithmetic {conversion.i:39}
+ Assigning imprecise value to f because of arithmetic operation on addresses.
[eva] conversion.i:40:
Frama_C_dump_each:
# cvalue:
diff --git a/tests/value/oracle/degeneration2.res.oracle b/tests/value/oracle/degeneration2.res.oracle
index b8f35c91cf1d94287e82e88c045e04502e9214ed..e792578b81a6454041457f7b7d52776de01325ce 100644
--- a/tests/value/oracle/degeneration2.res.oracle
+++ b/tests/value/oracle/degeneration2.res.oracle
@@ -13,8 +13,7 @@
[eva:alarm] degeneration2.i:14: Warning:
signed overflow. assert -((int)A) ≤ 2147483647;
[eva:garbled-mix:write] degeneration2.i:14:
- Assigning imprecise value to A.
- The imprecision originates from Arithmetic {degeneration2.i:14}
+ Assigning imprecise value to A because of arithmetic operation on addresses.
[eva:alarm] degeneration2.i:17: Warning:
accessing uninitialized left-value. assert \initialized((int *)A);
[eva:alarm] degeneration2.i:17: Warning:
@@ -24,6 +23,10 @@
accessing uninitialized left-value. assert \initialized(&offset_uninit);
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ degeneration2.i:14: arithmetic operation on addresses
+ (read 6 times, propagated 1 times) garbled mix of &{B; C; D; E}
[eva] degeneration2.i:25:
assertion 'Eva,initialization' got final status invalid.
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/deps_mixed.res.oracle b/tests/value/oracle/deps_mixed.res.oracle
index 446d6ada2d274f86c552e0abac55ffbbe73eef09..c1b9017883b5e17ab37579df0ddf684097d9acc4 100644
--- a/tests/value/oracle/deps_mixed.res.oracle
+++ b/tests/value/oracle/deps_mixed.res.oracle
@@ -33,11 +33,8 @@
[eva:alarm] deps_mixed.i:24: Warning:
pointer downcast. assert (unsigned int)(p + (int)q) ≤ 2147483647;
[eva:garbled-mix:write] deps_mixed.i:24:
- Assigning imprecise value to __retres.
- The imprecision originates from Arithmetic {deps_mixed.i:24}
-[eva:garbled-mix:write] deps_mixed.i:24:
- Assigning imprecise value to \result<main>.
- The imprecision originates from Arithmetic {deps_mixed.i:24}
+ Assigning imprecise value to __retres
+ because of arithmetic operation on addresses.
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/div.0.res.oracle b/tests/value/oracle/div.0.res.oracle
index 28621d9706abb4ce92bdb0c1b6c61043fe28fccc..5595ff6926a98d1312568297b44dd166c8d063ce 100644
--- a/tests/value/oracle/div.0.res.oracle
+++ b/tests/value/oracle/div.0.res.oracle
@@ -38,8 +38,7 @@
[eva:alarm] div.i:33: Warning:
signed overflow. assert (int)(&Z2) / Z2 ≤ 2147483647;
[eva:garbled-mix:write] div.i:33:
- Assigning imprecise value to b.
- The imprecision originates from Arithmetic {div.i:33}
+ Assigning imprecise value to b because of arithmetic operation on addresses.
[eva:alarm] div.i:34: Warning:
pointer downcast. assert (unsigned int)(&X + 2) ≤ 2147483647;
[eva:alarm] div.i:34: Warning: division by zero. assert (int)(&X + 2) ≢ 0;
@@ -48,8 +47,7 @@
[eva:alarm] div.i:34: Warning:
signed overflow. assert 100 / (int)(&X + 2) ≤ 2147483647;
[eva:garbled-mix:write] div.i:34:
- Assigning imprecise value to d2.
- The imprecision originates from Arithmetic {div.i:34}
+ Assigning imprecise value to d2 because of arithmetic operation on addresses.
[eva:alarm] div.i:35: Warning:
pointer downcast. assert (unsigned int)(&X + 1) ≤ 2147483647;
[eva:alarm] div.i:35: Warning:
@@ -57,8 +55,7 @@
[eva:alarm] div.i:35: Warning:
signed overflow. assert 100 / (int)(&X + 1) ≤ 2147483647;
[eva:garbled-mix:write] div.i:35:
- Assigning imprecise value to d1.
- The imprecision originates from Arithmetic {div.i:35}
+ Assigning imprecise value to d1 because of arithmetic operation on addresses.
[eva:alarm] div.i:36: Warning:
pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
[eva:alarm] div.i:36: Warning:
@@ -66,8 +63,7 @@
[eva:alarm] div.i:36: Warning:
signed overflow. assert 100 / (int)(&X) ≤ 2147483647;
[eva:garbled-mix:write] div.i:36:
- Assigning imprecise value to d0.
- The imprecision originates from Arithmetic {div.i:36}
+ Assigning imprecise value to d0 because of arithmetic operation on addresses.
[eva:alarm] div.i:37: Warning:
pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
[eva:alarm] div.i:37: Warning:
@@ -75,8 +71,7 @@
[eva:alarm] div.i:37: Warning:
signed overflow. assert -((int)(&X)) ≤ 2147483647;
[eva:garbled-mix:write] div.i:37:
- Assigning imprecise value to e.
- The imprecision originates from Arithmetic {div.i:37}
+ Assigning imprecise value to e because of arithmetic operation on addresses.
[eva] Recording results for main
[eva] Done for function main
[scope:rm_asserts] removing 2 assertion(s)
diff --git a/tests/value/oracle/div.1.res.oracle b/tests/value/oracle/div.1.res.oracle
index 6eabca0d307bcee7d1a03dad4795ec22a4f54530..d2a683468cbd53aa220ad3eab5454b1ab977ed7c 100644
--- a/tests/value/oracle/div.1.res.oracle
+++ b/tests/value/oracle/div.1.res.oracle
@@ -60,8 +60,7 @@
[eva:alarm] div.i:33: Warning:
signed overflow. assert (int)(&Z2) / Z2 ≤ 2147483647;
[eva:garbled-mix:write] div.i:33:
- Assigning imprecise value to b.
- The imprecision originates from Arithmetic {div.i:33}
+ Assigning imprecise value to b because of arithmetic operation on addresses.
[eva:alarm] div.i:34: Warning:
assertion 'rte,pointer_downcast' got status unknown.
[eva:alarm] div.i:34: Warning:
@@ -74,8 +73,7 @@
[eva:alarm] div.i:34: Warning:
signed overflow. assert 100 / (int)(&X + 2) ≤ 2147483647;
[eva:garbled-mix:write] div.i:34:
- Assigning imprecise value to d2.
- The imprecision originates from Arithmetic {div.i:34}
+ Assigning imprecise value to d2 because of arithmetic operation on addresses.
[eva:alarm] div.i:35: Warning:
assertion 'rte,pointer_downcast' got status unknown.
[eva] div.i:35: assertion 'rte,division_by_zero' got status valid.
@@ -86,8 +84,7 @@
[eva:alarm] div.i:35: Warning:
signed overflow. assert 100 / (int)(&X + 1) ≤ 2147483647;
[eva:garbled-mix:write] div.i:35:
- Assigning imprecise value to d1.
- The imprecision originates from Arithmetic {div.i:35}
+ Assigning imprecise value to d1 because of arithmetic operation on addresses.
[eva:alarm] div.i:36: Warning:
assertion 'rte,pointer_downcast' got status unknown.
[eva] div.i:36: assertion 'rte,division_by_zero' got status valid.
@@ -98,8 +95,7 @@
[eva:alarm] div.i:36: Warning:
signed overflow. assert 100 / (int)(&X) ≤ 2147483647;
[eva:garbled-mix:write] div.i:36:
- Assigning imprecise value to d0.
- The imprecision originates from Arithmetic {div.i:36}
+ Assigning imprecise value to d0 because of arithmetic operation on addresses.
[eva:alarm] div.i:37: Warning:
assertion 'rte,pointer_downcast' got status unknown.
[eva:alarm] div.i:37: Warning:
@@ -111,8 +107,7 @@
[eva:alarm] div.i:37: Warning:
signed overflow. assert -((int)(&X)) ≤ 2147483647;
[eva:garbled-mix:write] div.i:37:
- Assigning imprecise value to e.
- The imprecision originates from Arithmetic {div.i:37}
+ Assigning imprecise value to e because of arithmetic operation on addresses.
[eva] Recording results for main
[eva] Done for function main
[eva] div.i:22: assertion 'rte,signed_overflow' got final status valid.
diff --git a/tests/value/oracle/downcast.4.res.oracle b/tests/value/oracle/downcast.4.res.oracle
index aaae6f3d0b6996f66845a397c8e56dceb80aa583..5417bdf0ee0768eba91482a4a276e95abf21b4e5 100644
--- a/tests/value/oracle/downcast.4.res.oracle
+++ b/tests/value/oracle/downcast.4.res.oracle
@@ -46,11 +46,9 @@
[eva] computing for function main6_val_warn_converted_signed <- main.
Called from downcast.i:161.
[eva:garbled-mix:write] downcast.i:96:
- Assigning imprecise value to y.
- The imprecision originates from Arithmetic {downcast.i:96}
+ Assigning imprecise value to y because of arithmetic operation on addresses.
[eva:garbled-mix:write] downcast.i:97:
- Assigning imprecise value to z.
- The imprecision originates from Arithmetic {downcast.i:97}
+ Assigning imprecise value to z because of arithmetic operation on addresses.
[eva] Recording results for main6_val_warn_converted_signed
[eva] Done for function main6_val_warn_converted_signed
[eva] computing for function main7_signed_upcast <- main.
diff --git a/tests/value/oracle/empty_struct.6.res.oracle b/tests/value/oracle/empty_struct.6.res.oracle
index c67a99bfed4c23f7e2f3276860441cc21fd2ad5f..cf2ce4f7e5017fc89087bc192e005d7dec7f2189 100644
--- a/tests/value/oracle/empty_struct.6.res.oracle
+++ b/tests/value/oracle/empty_struct.6.res.oracle
@@ -8,10 +8,10 @@
[eva] computing for function f <- main4.
Called from empty_struct.c:99.
[eva] using specification for function f
+[eva:garbled-mix:assigns] empty_struct.c:99:
+ The specification of function f has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function f
-[eva:garbled-mix:write] empty_struct.c:99:
- Assigning imprecise value to r.
- The imprecision originates from Library function {empty_struct.c:99}
[kernel:annot:missing-spec] empty_struct.c:100: Warning:
Neither code nor specification for function g,
generating default assigns. See -generated-spec-* options for more info
@@ -21,6 +21,10 @@
[eva] Done for function g
[eva] Recording results for main4
[eva] Done for function main4
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ empty_struct.c:99: assigns clause on addresses
+ (read 2 times, propagated 3 times) garbled mix of &{gs}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main4:
r ∈
diff --git a/tests/value/oracle/eval_separated.res.oracle b/tests/value/oracle/eval_separated.res.oracle
index 899ef89f2cc0386e2732a8e9c87eb7b835dcd3a1..de147cad6d37b70214fd95bc61ec7c25842b6875 100644
--- a/tests/value/oracle/eval_separated.res.oracle
+++ b/tests/value/oracle/eval_separated.res.oracle
@@ -18,8 +18,7 @@
[eva:alarm] eval_separated.c:11: Warning:
signed overflow. assert (int)(&q) + (int)(&q) ≤ 2147483647;
[eva:garbled-mix:write] eval_separated.c:11:
- Assigning imprecise value to q.
- The imprecision originates from Arithmetic {eval_separated.c:11}
+ Assigning imprecise value to q because of arithmetic operation on addresses.
[eva:alarm] eval_separated.c:12: Warning:
pointer downcast. assert (unsigned int)(&r) ≤ 2147483647;
[eva:alarm] eval_separated.c:12: Warning:
@@ -27,8 +26,7 @@
[eva:alarm] eval_separated.c:12: Warning:
signed overflow. assert (int)(&r) + (int)(&r) ≤ 2147483647;
[eva:garbled-mix:write] eval_separated.c:12:
- Assigning imprecise value to r.
- The imprecision originates from Arithmetic {eval_separated.c:12}
+ Assigning imprecise value to r because of arithmetic operation on addresses.
[eva:alarm] eval_separated.c:13: Warning: assertion got status unknown.
[eva:alarm] eval_separated.c:14: Warning: assertion got status unknown.
[eva:alarm] eval_separated.c:15: Warning: assertion got status unknown.
diff --git a/tests/value/oracle/from_call.0.res.oracle b/tests/value/oracle/from_call.0.res.oracle
index 88c6c5d8c6d416983f927de6f9655687531bbebf..f3377d39ae638c90c299fa32083c399803a221ef 100644
--- a/tests/value/oracle/from_call.0.res.oracle
+++ b/tests/value/oracle/from_call.0.res.oracle
@@ -178,6 +178,9 @@
[eva] computing for function unavailable_f <- main.
Called from from_call.i:96.
[eva] using specification for function unavailable_f
+[eva:garbled-mix:assigns] from_call.i:96:
+ The specification of function unavailable_f
+ has generated a garbled mix of addresses for assigns clause AR.
[eva] Done for function unavailable_f
[eva] Recording results for main
[from] Computing for function main
diff --git a/tests/value/oracle/from_call.1.res.oracle b/tests/value/oracle/from_call.1.res.oracle
index 560d21d929a84ba7eec01b95ef43454445de32a5..18901931cee6b75386e480ca4f21c8681cb5955b 100644
--- a/tests/value/oracle/from_call.1.res.oracle
+++ b/tests/value/oracle/from_call.1.res.oracle
@@ -142,6 +142,9 @@
[eva] computing for function unavailable_f <- main.
Called from from_call.i:96.
[eva] using specification for function unavailable_f
+[eva:garbled-mix:assigns] from_call.i:96:
+ The specification of function unavailable_f
+ has generated a garbled mix of addresses for assigns clause AR.
[eva] Done for function unavailable_f
[eva] Recording results for main
[eva] Done for function main
diff --git a/tests/value/oracle/gauges.res.oracle b/tests/value/oracle/gauges.res.oracle
index 050ed73c53ad6db810ce0e3f0b9c795c17b33450..4b7f0372dd0bb9eb70ae5e95a7ad3d083f33c162 100644
--- a/tests/value/oracle/gauges.res.oracle
+++ b/tests/value/oracle/gauges.res.oracle
@@ -235,11 +235,7 @@
[eva:alarm] gauges.c:188: Warning:
signed overflow. assert (int)p + (int)q ≤ 2147483647;
[eva:garbled-mix:write] gauges.c:188:
- Assigning imprecise value to z.
- The imprecision originates from Arithmetic {gauges.c:188}
-[eva:garbled-mix:write] gauges.c:189:
- Assigning imprecise value to r.
- The imprecision originates from Arithmetic {gauges.c:188}
+ Assigning imprecise value to z because of arithmetic operation on addresses.
[eva:alarm] gauges.c:190: Warning: out of bounds write. assert \valid(r);
[eva:alarm] gauges.c:192: Warning: out of bounds write. assert \valid(p);
[eva:alarm] gauges.c:193: Warning: out of bounds write. assert \valid(q);
@@ -714,6 +710,10 @@
[eva] Done for function main17
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ gauges.c:188: arithmetic operation on addresses
+ (read 14 times, propagated 12 times) garbled mix of &{x; y}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main0:
i ∈ {1; 162}
diff --git a/tests/value/oracle/imprecise_invalid_write.res.oracle b/tests/value/oracle/imprecise_invalid_write.res.oracle
index 3edbb6d07b05abbb8a627315a7e04d341fcd40ee..49172ffd8d93700972e082185b7f3d691c1be222 100644
--- a/tests/value/oracle/imprecise_invalid_write.res.oracle
+++ b/tests/value/oracle/imprecise_invalid_write.res.oracle
@@ -24,8 +24,7 @@
[eva:alarm] imprecise_invalid_write.i:9: Warning:
pointer downcast. assert (unsigned int)(&main1) ≤ 2147483647;
[eva:garbled-mix:write] imprecise_invalid_write.i:9:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {imprecise_invalid_write.i:9}
+ Assigning imprecise value to p because of arithmetic operation on addresses.
[eva:alarm] imprecise_invalid_write.i:10: Warning:
out of bounds write. assert \valid((int *)p);
[kernel] imprecise_invalid_write.i:10: Warning:
@@ -37,8 +36,7 @@
[eva:alarm] imprecise_invalid_write.i:16: Warning:
pointer downcast. assert (unsigned int)s ≤ 2147483647;
[eva:garbled-mix:write] imprecise_invalid_write.i:16:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {imprecise_invalid_write.i:16}
+ Assigning imprecise value to p because of arithmetic operation on addresses.
[eva:alarm] imprecise_invalid_write.i:17: Warning:
out of bounds write. assert \valid(p);
[kernel] imprecise_invalid_write.i:17: Warning:
@@ -47,6 +45,12 @@
[eva] Done for function main3
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ imprecise_invalid_write.i:9: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) garbled mix of &{main1}
+ imprecise_invalid_write.i:16: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) garbled mix of &{"abc"}
[eva] imprecise_invalid_write.i:5:
assertion 'Eva,mem_access' got final status invalid.
[eva] imprecise_invalid_write.i:10:
diff --git a/tests/value/oracle/initialized.res.oracle b/tests/value/oracle/initialized.res.oracle
index d7b4af3ec6e4bc9398250cf52ce0acc4a026ff7e..150e3f1824268b9374592e59ea74da1ccc0c4429 100644
--- a/tests/value/oracle/initialized.res.oracle
+++ b/tests/value/oracle/initialized.res.oracle
@@ -73,11 +73,8 @@
[eva:alarm] initialized.c:50: Warning:
signed overflow. assert (int)(&b4) + (int)(&b4) ≤ 2147483647;
[eva:garbled-mix:write] initialized.c:50:
- Assigning imprecise value to t[6].
- The imprecision originates from Arithmetic {initialized.c:50}
-[eva:garbled-mix:write] initialized.c:51:
- Assigning imprecise value to t[7].
- The imprecision originates from Arithmetic {initialized.c:50}
+ Assigning imprecise value to t[6]
+ because of arithmetic operation on addresses.
[eva] initialized.c:63:
Frama_C_dump_each:
# cvalue:
@@ -234,6 +231,10 @@
[eva] Done for function reduce_by_negation
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ initialized.c:50: arithmetic operation on addresses
+ (read 1 times, propagated 2 times) garbled mix of &{b4}
[eva] initialized.c:93: assertion 'Eva,initialization' got final status invalid.
[eva] initialized.c:104:
assertion 'Eva,initialization' got final status invalid.
diff --git a/tests/value/oracle/inout_proto.res.oracle b/tests/value/oracle/inout_proto.res.oracle
index 77fcb77f70191983ad3627233361879ec9e288a7..d96ee3689cbfcaf14df1fbc700e908385e2a6247 100644
--- a/tests/value/oracle/inout_proto.res.oracle
+++ b/tests/value/oracle/inout_proto.res.oracle
@@ -13,6 +13,9 @@
[eva] computing for function SendBuffer <- main <- main_main.
Called from inout_proto.i:19.
[eva] using specification for function SendBuffer
+[eva:garbled-mix:assigns] inout_proto.i:19:
+ The specification of function SendBuffer
+ has generated a garbled mix of addresses for assigns clause *RETURN_CODE.
[eva] Done for function SendBuffer
[eva] Recording results for main
[eva] Done for function main
diff --git a/tests/value/oracle/join_misaligned.res.oracle b/tests/value/oracle/join_misaligned.res.oracle
index 82adf0d093dbffd8bfb9b2ca4928d6650ad4e8af..923f7c4aa5d06383052e0ed08a4ac10cfc406200 100644
--- a/tests/value/oracle/join_misaligned.res.oracle
+++ b/tests/value/oracle/join_misaligned.res.oracle
@@ -20,10 +20,6 @@
pointer downcast. assert (unsigned int)(&u) ≤ 2147483647;
[eva] Recording results for main
[eva] Done for function main
-[eva:garbled-mix:summary] Warning:
- Garbled mix generated during analysis:
- {{ garbled mix of &{t} (origin: Merge {join_misaligned.i:42}) }}
- {{ garbled mix of &{u} (origin: Merge {join_misaligned.i:42}) }}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
t{[0]; [1][bits 0 to 15]} ∈ {0}
diff --git a/tests/value/oracle/label.res.oracle b/tests/value/oracle/label.res.oracle
index 7634f9cc0083b4c837f6a2435f8269b29c667ea5..4b44fa1adfa728e27f6f9d97a39125ec045b12c2 100644
--- a/tests/value/oracle/label.res.oracle
+++ b/tests/value/oracle/label.res.oracle
@@ -14,20 +14,7 @@
pointer downcast. assert (unsigned int)(&d + 1) ≤ 2147483647;
[eva:garbled-mix:write] label.i:18:
Assigning imprecise value to *((char *)(& p) + i)
- (pointing to p with offsets {0}).
- The imprecision originates from Misaligned {label.i:18}
-[eva:garbled-mix:write] label.i:18:
- Assigning imprecise value to *((char *)(& p) + i)
- (pointing to p with offsets {0; 8}).
- The imprecision originates from Misaligned {label.i:18}
-[eva:garbled-mix:write] label.i:18:
- Assigning imprecise value to *((char *)(& p) + i)
- (pointing to p with offsets {0; 8; 16}).
- The imprecision originates from Misaligned {label.i:18}
-[eva:garbled-mix:write] label.i:18:
- Assigning imprecise value to *((char *)(& p) + i)
- (pointing to p with offsets {0; 8; 16; 24}).
- The imprecision originates from Misaligned {label.i:18}
+ because of misaligned read of addresses.
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
@@ -35,7 +22,7 @@
a ∈ {{ &d + {4} }}
b ∈ {1; 2}
i ∈ {4}
- p ∈ {{ garbled mix of &{a; b} (origin: Misaligned {label.i:18}) }}
+ p ∈ {{ garbled mix of &{a; b} (origin: Misaligned read {label.i:18}) }}
q ∈ {{ &a }}
[from] Computing for function main
[from] Done for function main
diff --git a/tests/value/oracle/leaf.res.oracle b/tests/value/oracle/leaf.res.oracle
index 7ccd5e0302a676eb3ee7293c6683d039208b0eca..865b2bc8486622735e111a273c8a8300c3b277a9 100644
--- a/tests/value/oracle/leaf.res.oracle
+++ b/tests/value/oracle/leaf.res.oracle
@@ -39,20 +39,20 @@
[eva] computing for function f_int_star_int <- main.
Called from leaf.i:50.
[eva] using specification for function f_int_star_int
+[eva:garbled-mix:assigns] leaf.i:50:
+ The specification of function f_int_star_int
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function f_int_star_int
-[eva:garbled-mix:write] leaf.i:50:
- Assigning imprecise value to p.
- The imprecision originates from Library function {leaf.i:50}
[eva] leaf.i:51: Frama_C_show_each_F: [-2147483648..2147483647]
[eva:alarm] leaf.i:52: Warning: out of bounds write. assert \valid(p);
[eva] leaf.i:53: Frama_C_show_each_F: {5}
[eva] computing for function f_int_star_int_star_int <- main.
Called from leaf.i:55.
[eva] using specification for function f_int_star_int_star_int
+[eva:garbled-mix:assigns] leaf.i:55:
+ The specification of function f_int_star_int_star_int
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function f_int_star_int_star_int
-[eva:garbled-mix:write] leaf.i:55:
- Assigning imprecise value to pp.
- The imprecision originates from Library function {leaf.i:55}
[eva] leaf.i:56: Frama_C_show_each_G: {{ &g }}
[eva] leaf.i:57: Frama_C_show_each_F: {5}
[eva] leaf.i:59: Frama_C_show_each_G: {{ &g }}
@@ -91,20 +91,20 @@
[eva] computing for function f_st_star_cint_st_star_cint <- main.
Called from leaf.i:68.
[eva] using specification for function f_st_star_cint_st_star_cint
+[eva:garbled-mix:assigns] leaf.i:68:
+ The specification of function f_st_star_cint_st_star_cint
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function f_st_star_cint_st_star_cint
-[eva:garbled-mix:write] leaf.i:68:
- Assigning imprecise value to st_star_cint_1.
- The imprecision originates from Library function {leaf.i:68}
[kernel:annot:missing-spec] leaf.i:69: Warning:
Neither code nor specification for function f_st_star_int_st_star_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f_st_star_int_st_star_int <- main.
Called from leaf.i:69.
[eva] using specification for function f_st_star_int_st_star_int
+[eva:garbled-mix:assigns] leaf.i:69:
+ The specification of function f_st_star_int_st_star_int
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function f_st_star_int_st_star_int
-[eva:garbled-mix:write] leaf.i:69:
- Assigning imprecise value to st_star_int_1.
- The imprecision originates from Library function {leaf.i:69}
[kernel:annot:missing-spec] leaf.i:70: Warning:
Neither code nor specification for function f_st_tab3_int_st_tab3_int,
generating default assigns. See -generated-spec-* options for more info
@@ -118,6 +118,9 @@
[eva] computing for function f_star_st_star_cint_int <- main.
Called from leaf.i:72.
[eva] using specification for function f_star_st_star_cint_int
+[eva:garbled-mix:assigns] leaf.i:72:
+ The specification of function f_star_st_star_cint_int
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function f_star_st_star_cint_int
[kernel:annot:missing-spec] leaf.i:73: Warning:
Neither code nor specification for function f_star_st_star_int_int,
@@ -125,6 +128,9 @@
[eva] computing for function f_star_st_star_int_int <- main.
Called from leaf.i:73.
[eva] using specification for function f_star_st_star_int_int
+[eva:garbled-mix:assigns] leaf.i:73:
+ The specification of function f_star_st_star_int_int
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function f_star_st_star_int_int
[kernel:annot:missing-spec] leaf.i:74: Warning:
Neither code nor specification for function f_star_st_tab3_int_int,
@@ -135,6 +141,12 @@
[eva] Done for function f_star_st_tab3_int_int
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ leaf.i:55: assigns clause on addresses (read 10 times, propagated 2 times)
+ garbled mix of &{pg}
+ leaf.i:50: assigns clause on addresses (read 4 times, propagated 2 times)
+ garbled mix of &{g}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
T[0] ∈ [--..--]
diff --git a/tests/value/oracle/leaf2.res.oracle b/tests/value/oracle/leaf2.res.oracle
index 3f486d154c0c0f64d200520942925f611f485b1d..c03b05b96d49fc64e90e969fc0d3b0d84c0cd8fd 100644
--- a/tests/value/oracle/leaf2.res.oracle
+++ b/tests/value/oracle/leaf2.res.oracle
@@ -14,17 +14,18 @@
[eva] computing for function f <- main.
Called from leaf2.i:6.
[eva] using specification for function f
+[eva:garbled-mix:assigns] leaf2.i:6:
+ The specification of function f has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function f
-[eva:garbled-mix:write] leaf2.i:6:
- Assigning imprecise value to G.
- The imprecision originates from Library function {leaf2.i:6}
[eva:alarm] leaf2.i:7: Warning: signed overflow. assert -2147483648 ≤ G + 1;
[eva:alarm] leaf2.i:7: Warning: signed overflow. assert G + 1 ≤ 2147483647;
-[eva:garbled-mix:write] leaf2.i:7:
- Assigning imprecise value to G.
- The imprecision originates from Library function {leaf2.i:6}
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ leaf2.i:6: assigns clause on addresses (read 4 times, propagated 4 times)
+ garbled mix of &{I}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
G ∈ {{ garbled mix of &{I} (origin: Library function {leaf2.i:6}) }}
diff --git a/tests/value/oracle/library.res.oracle b/tests/value/oracle/library.res.oracle
index 3a3a113d63804454659655d9caeb4b00194905de..992d56c788e072721596736c0b2e43b90e331267 100644
--- a/tests/value/oracle/library.res.oracle
+++ b/tests/value/oracle/library.res.oracle
@@ -86,10 +86,10 @@
[eva] computing for function f_star_int <- main.
Called from library.i:31.
[eva] using specification for function f_star_int
+[eva:garbled-mix:assigns] library.i:31:
+ The specification of function f_star_int
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function f_star_int
-[eva:garbled-mix:write] library.i:31:
- Assigning imprecise value to G1.
- The imprecision originates from Library function {library.i:31}
[eva:alarm] library.i:32: Warning: out of bounds write. assert \valid(G1);
[eva:alarm] library.i:33: Warning: out of bounds read. assert \valid_read(G);
[eva:alarm] library.i:33: Warning: out of bounds read. assert \valid_read(*G);
@@ -112,10 +112,10 @@
[eva] computing for function i <- main.
Called from library.i:41.
[eva] using specification for function i
+[eva:garbled-mix:assigns] library.i:41:
+ The specification of function i has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function i
-[eva:garbled-mix:write] library.i:41:
- Assigning imprecise value to pf.
- The imprecision originates from Library function {library.i:41}
[eva:alarm] library.i:42: Warning: out of bounds read. assert \valid_read(pf);
[eva:alarm] library.i:42: Warning:
non-finite float value. assert \is_finite(*pf);
@@ -128,13 +128,21 @@
[eva] computing for function k <- main.
Called from library.i:45.
[eva] using specification for function k
+[eva:garbled-mix:assigns] library.i:45:
+ The specification of function k has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function k
-[eva:garbled-mix:write] library.i:45:
- Assigning imprecise value to pd.
- The imprecision originates from Library function {library.i:45}
[eva:alarm] library.i:46: Warning: out of bounds write. assert \valid(pd);
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ library.i:31: assigns clause on addresses
+ (read 2 times, propagated 2 times) garbled mix of &{S_gpi}
+ library.i:41: assigns clause on addresses
+ (read 2 times, propagated 2 times) garbled mix of &{S_gpf}
+ library.i:45: assigns clause on addresses
+ (read 2 times, propagated 2 times) garbled mix of &{S_gpd}
[eva] library.i:38: assertion 'Eva,function_pointer' got final status invalid.
[eva] library.i:39: assertion 'Eva,function_pointer' got final status invalid.
[eva] library.i:40: assertion 'Eva,function_pointer' got final status invalid.
diff --git a/tests/value/oracle/logic.res.oracle b/tests/value/oracle/logic.res.oracle
index f88f05e9117129bb86b043b56223a54f5c3c6475..77e8322bc7e61c9497bbd89beac20ade5492cac4 100644
--- a/tests/value/oracle/logic.res.oracle
+++ b/tests/value/oracle/logic.res.oracle
@@ -415,10 +415,10 @@
[eva] logic.c:408: Frama_C_show_each_set: {0; 1; 2; 3; 4; 5}
[eva] computing for function abs <- int_abs <- main.
Called from logic.c:411.
+[eva:garbled-mix:assigns] logic.c:411:
+ The specification of function abs has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function abs
-[eva:garbled-mix:write] logic.c:411:
- Assigning imprecise value to x_0.
- The imprecision originates from Library function {logic.c:411}
[eva] logic.c:412:
Frama_C_show_each_gm:
{{ garbled mix of &{x_0} (origin: Library function {logic.c:411}) }}
@@ -563,6 +563,10 @@
[eva] Done for function plet
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ logic.c:411: assigns clause on addresses (read 1 times, propagated 2 times)
+ garbled mix of &{x_0}
[eva] logic.c:530:
Cannot evaluate range bound __fc_len - 1
(unsupported logic var __fc_len). Approximating
diff --git a/tests/value/oracle/logic_ptr_cast.res.oracle b/tests/value/oracle/logic_ptr_cast.res.oracle
index 2cc7cbd033fd40684cf2d7c55f957e8a43fb8e41..8c23da7de9a82c9380add324962fc335b475540e 100644
--- a/tests/value/oracle/logic_ptr_cast.res.oracle
+++ b/tests/value/oracle/logic_ptr_cast.res.oracle
@@ -6,8 +6,7 @@
p ∈ {0}
t[0..89] ∈ {0}
[eva:garbled-mix:write] logic_ptr_cast.i:8:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {logic_ptr_cast.i:8}
+ Assigning imprecise value to p because of arithmetic operation on addresses.
[eva:alarm] logic_ptr_cast.i:9: Warning: assertion got status unknown.
[eva] logic_ptr_cast.i:14:
Frama_C_show_each: {{ &t + {0; 1; 2; 3; 4; 5; 6; 7} }}
diff --git a/tests/value/oracle/multidim-relations.res.oracle b/tests/value/oracle/multidim-relations.res.oracle
index e7f1d9da7ace7a3640b02aab980928a144b93e12..aa7000e536dc44b7605a8c08d43d786b47352cd0 100644
--- a/tests/value/oracle/multidim-relations.res.oracle
+++ b/tests/value/oracle/multidim-relations.res.oracle
@@ -48,6 +48,12 @@
[eva] Done for function use_array
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ multidim-relations.c:18: imprecise merge of addresses
+ (read 7 times, propagated 0 times) garbled mix of &{g; h}
+ multidim-relations.c:19: imprecise merge of addresses
+ (read 4 times, propagated 0 times) garbled mix of &{g; h}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function init_array:
t[0]{.kind; .[bits 8 to 31]#} ∈ {0; 1} repeated %8
diff --git a/tests/value/oracle/not_ct_array_arg.res.oracle b/tests/value/oracle/not_ct_array_arg.res.oracle
index bc4b35bcb5822c058be586eea8fc6709cfdad55d..560745bc9b332a6c91f73d247be11f3fdde05bd8 100644
--- a/tests/value/oracle/not_ct_array_arg.res.oracle
+++ b/tests/value/oracle/not_ct_array_arg.res.oracle
@@ -35,10 +35,11 @@
tc ∈ {{ NULL ; &S_tc[0] }}
S_tc[0..1][0..9] ∈ [--..--]
S_tb[bits 0 to 31] ∈
- {{ garbled mix of &{tb} (origin: Misaligned {not_ct_array_arg.i:12}) }}
+ {{ garbled mix of &{tb}
+ (origin: Misaligned write {not_ct_array_arg.i:12}) }}
[bits 32 to ..] ∈
{{ garbled mix of &{tb}
- (origin: Misaligned {not_ct_array_arg.i:12}) }} or UNINITIALIZED
+ (origin: Misaligned write {not_ct_array_arg.i:12}) }} or UNINITIALIZED
==END OF DUMP==
[eva:alarm] not_ct_array_arg.i:14: Warning:
out of bounds write. assert \valid(&(*(tc + 1))[1]);
@@ -56,10 +57,11 @@
[1][1] ∈ {3}
[1][2..9] ∈ [--..--]
S_tb[bits 0 to 31] ∈
- {{ garbled mix of &{tb} (origin: Misaligned {not_ct_array_arg.i:12}) }}
+ {{ garbled mix of &{tb}
+ (origin: Misaligned write {not_ct_array_arg.i:12}) }}
[bits 32 to ..] ∈
{{ garbled mix of &{tb}
- (origin: Misaligned {not_ct_array_arg.i:12}) }} or UNINITIALIZED
+ (origin: Misaligned write {not_ct_array_arg.i:12}) }} or UNINITIALIZED
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/value/oracle/origin.0.res.oracle b/tests/value/oracle/origin.0.res.oracle
index 21313b3be754e82c6d4c9570db9f1ae65208e409..e93befd14488bc1553a17bdd7359fd79315a146c 100644
--- a/tests/value/oracle/origin.0.res.oracle
+++ b/tests/value/oracle/origin.0.res.oracle
@@ -61,8 +61,8 @@
[eva:alarm] origin.i:14: Warning:
signed overflow. assert -((int)((int *)ta1)) ≤ 2147483647;
[eva:garbled-mix:write] origin.i:14:
- Assigning imprecise value to pa1.
- The imprecision originates from Arithmetic {origin.i:14}
+ Assigning imprecise value to pa1
+ because of arithmetic operation on addresses.
[eva:alarm] origin.i:15: Warning: out of bounds write. assert \valid(pa1);
[eva] Recording results for origin_arithmetic_1
[eva] Done for function origin_arithmetic_1
@@ -75,11 +75,8 @@
[eva:alarm] origin.i:19: Warning:
signed overflow. assert -((int)((int *)ta2)) ≤ 2147483647;
[eva:garbled-mix:write] origin.i:19:
- Assigning imprecise value to pa2.
- The imprecision originates from Arithmetic {origin.i:19}
-[eva:garbled-mix:write] origin.i:20:
- Assigning imprecise value to qa2.
- The imprecision originates from Arithmetic {origin.i:19}
+ Assigning imprecise value to pa2
+ because of arithmetic operation on addresses.
[eva:alarm] origin.i:20: Warning:
pointer downcast. assert (unsigned int)((int *)tta2) ≤ 2147483647;
[eva:alarm] origin.i:20: Warning:
@@ -87,8 +84,8 @@
[eva:alarm] origin.i:20: Warning:
signed overflow. assert -((int)((int *)tta2)) ≤ 2147483647;
[eva:garbled-mix:write] origin.i:20:
- Assigning imprecise value to qa2.
- The imprecision originates from Arithmetic {origin.i:20}
+ Assigning imprecise value to qa2
+ because of arithmetic operation on addresses.
[eva:alarm] origin.i:21: Warning: out of bounds write. assert \valid(qa2);
[eva:alarm] origin.i:21: Warning:
pointer downcast. assert (unsigned int)(&aa2) ≤ 2147483647;
@@ -103,8 +100,8 @@
[eva:alarm] origin.i:25: Warning:
signed overflow. assert -((int)((int *)ta3)) ≤ 2147483647;
[eva:garbled-mix:write] origin.i:25:
- Assigning imprecise value to pa3.
- The imprecision originates from Arithmetic {origin.i:25}
+ Assigning imprecise value to pa3
+ because of arithmetic operation on addresses.
[eva:alarm] origin.i:26: Warning: out of bounds write. assert \valid(pa3);
[eva] Recording results for origin_arithmetic_3
[eva] Done for function origin_arithmetic_3
@@ -131,27 +128,25 @@
[eva] computing for function gp <- main.
Called from origin.i:100.
[eva] using specification for function gp
+[eva:garbled-mix:assigns] origin.i:100:
+ The specification of function gp has generated a garbled mix of addresses
+ for assigns clause \result.
[eva] Done for function gp
-[eva:garbled-mix:write] origin.i:100:
- Assigning imprecise value to pl.
- The imprecision originates from Library function {origin.i:100}
[eva:alarm] origin.i:101: Warning: out of bounds read. assert \valid_read(pl);
[eva] computing for function origin_misalign_1 <- main.
Called from origin.i:102.
[eva:garbled-mix:write] origin.i:48:
- Assigning imprecise value to pm1.
- The imprecision originates from Misaligned {origin.i:48}
+ Assigning imprecise value to pm1 because of misaligned read of addresses.
[eva:alarm] origin.i:49: Warning: out of bounds write. assert \valid(pm1);
[eva] Recording results for origin_misalign_1
[eva] Done for function origin_misalign_1
[eva] computing for function origin_misalign_2 <- main.
Called from origin.i:103.
[eva:garbled-mix:write] origin.i:54:
- Assigning imprecise value to qm2.
- The imprecision originates from Misaligned {origin.i:54}
+ Assigning imprecise value to qm2 because of misaligned read of addresses.
[eva] origin.i:55:
Frama_C_show_each:
- {{ garbled mix of &{a; b} (origin: Misaligned {origin.i:54}) }}
+ {{ garbled mix of &{a; b} (origin: Misaligned read {origin.i:54}) }}
[eva:alarm] origin.i:56: Warning: out of bounds write. assert \valid(qm2);
[eva:alarm] origin.i:56: Warning:
pointer downcast. assert (unsigned int)(&a) ≤ 2147483647;
@@ -184,8 +179,8 @@
[eva:alarm] origin.i:85: Warning:
signed overflow. assert -((int)(&arg)) ≤ 2147483647;
[eva:garbled-mix:write] origin.i:85:
- Assigning imprecise value to esc3.
- The imprecision originates from Arithmetic {origin.i:85}
+ Assigning imprecise value to esc3
+ because of arithmetic operation on addresses.
[eva:alarm] origin.i:87: Warning:
pointer downcast. assert (unsigned int)(&local1) ≤ 2147483647;
[eva:alarm] origin.i:88: Warning:
@@ -202,6 +197,20 @@
locals {local1} escaping the scope of local_escape_1 through esc4
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ origin.i:19: arithmetic operation on addresses
+ (read 3 times, propagated 2 times) garbled mix of &{ta2; tta2}
+ origin.i:54: misaligned read of addresses
+ (read 3 times, propagated 1 times) garbled mix of &{a; b}
+ origin.i:14: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) garbled mix of &{ta1}
+ origin.i:25: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) garbled mix of &{ta3}
+ origin.i:100: assigns clause on addresses
+ (read 2 times, propagated 2 times) garbled mix of &{S_gpp}
+ origin.i:48: misaligned read of addresses
+ (read 2 times, propagated 1 times) garbled mix of &{a; b}
[eva] origin.i:75: assertion 'Eva,initialization' got final status invalid.
[scope:rm_asserts] removing 2 assertion(s)
[eva] ====== VALUES COMPUTED ======
@@ -219,9 +228,9 @@
pa2 ∈ {{ garbled mix of &{ta2} (origin: Arithmetic {origin.i:19}) }}
qa2 ∈ {{ &ta2 + [0..36] ; &tta2 + [0..36] }}
ta2[0..9] ∈
- {{ garbled mix of &{aa2} (origin: Misaligned {origin.i:21}) }}
+ {{ garbled mix of &{aa2} (origin: Misaligned write {origin.i:21}) }}
tta2[0..9] ∈
- {{ garbled mix of &{aa2} (origin: Misaligned {origin.i:21}) }}
+ {{ garbled mix of &{aa2} (origin: Misaligned write {origin.i:21}) }}
[eva:final-states] Values at end of function origin_arithmetic_3:
pa3 ∈ {{ &ta3 + [0..36] }}
ta3[0..9] ∈ [--..--]
@@ -260,10 +269,10 @@
{{ garbled mix of &{b} (origin: Merge {origin.i:106}) }}
ta1[0..9] ∈ {0}
ta2[0..9] ∈
- {{ garbled mix of &{aa2} (origin: Misaligned {origin.i:21}) }}
+ {{ garbled mix of &{aa2} (origin: Misaligned write {origin.i:21}) }}
ta3[0..9] ∈ [--..--]
tta2[0..9] ∈
- {{ garbled mix of &{aa2} (origin: Misaligned {origin.i:21}) }}
+ {{ garbled mix of &{aa2} (origin: Misaligned write {origin.i:21}) }}
l1 ∈ [--..--]
l2 ∈ [--..--]
l3 ∈ [--..--]
diff --git a/tests/value/oracle/origin.1.res.oracle b/tests/value/oracle/origin.1.res.oracle
index 2d7eae48a93c4432e4dac6e0f18275b4fdc43432..f9c473570c4ed0ed91b4da38d351db512e6bfbf2 100644
--- a/tests/value/oracle/origin.1.res.oracle
+++ b/tests/value/oracle/origin.1.res.oracle
@@ -60,11 +60,9 @@
[eva] using specification for function f
[eva] Done for function f
[eva:garbled-mix:write] origin.i:126:
- Assigning imprecise value to r.p.
- The imprecision originates from Misaligned {origin.i:126}
+ Assigning imprecise value to r.p because of misaligned read of addresses.
[eva:garbled-mix:write] origin.i:129:
- Assigning imprecise value to r.t[0].
- The imprecision originates from Merge {origin.i:129}
+ Assigning imprecise value to r.t[0] because of imprecise merge of addresses.
[eva:alarm] origin.i:130: Warning:
pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:alarm] origin.i:130: Warning:
@@ -72,19 +70,20 @@
[eva:alarm] origin.i:130: Warning:
signed overflow. assert -((int)(&x)) ≤ 2147483647;
[eva:garbled-mix:write] origin.i:130:
- Assigning imprecise value to r.t[1].
- The imprecision originates from Arithmetic {origin.i:130}
-[eva:garbled-mix:write] origin.i:131:
- Assigning imprecise value to \result<origin>.
- The imprecision originates from Misaligned {origin.i:126}
+ Assigning imprecise value to r.t[1]
+ because of arithmetic operation on addresses.
[eva] Recording results for origin
[eva] Done for function origin
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ origin.i:126: misaligned read of addresses
+ (read 1 times, propagated 2 times) garbled mix of &{x; y}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function origin:
r.c ∈ [--..--]
.[bits 8 to 15] ∈ UNINITIALIZED
.i ∈ [--..--]
- .p ∈ {{ garbled mix of &{x} (origin: Misaligned {origin.i:126}) }}
+ .p ∈ {{ garbled mix of &{x} (origin: Misaligned read {origin.i:126}) }}
.t[0][bits 0 to 7] ∈
{{ garbled mix of &{y} (origin: Merge {origin.i:129}) }}
.t[0][bits 8 to 15]# ∈ {{ NULL ; (? *)&y }}%32, bits 24 to 31
diff --git a/tests/value/oracle/period.res.oracle b/tests/value/oracle/period.res.oracle
index cca040e6158d8cb00ae2ab1bb22e787b08bec17a..3f7cc6e99f50ff733afed56c83c82de26a529a36 100644
--- a/tests/value/oracle/period.res.oracle
+++ b/tests/value/oracle/period.res.oracle
@@ -83,23 +83,28 @@
[eva:alarm] period.c:51: Warning:
pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
[eva:garbled-mix:write] period.c:51:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {period.c:51}
+ Assigning imprecise value to p because of arithmetic operation on addresses.
[eva:alarm] period.c:52: Warning: out of bounds write. assert \valid(p);
[eva:alarm] period.c:53: Warning:
pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
[eva:garbled-mix:write] period.c:53:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {period.c:53}
+ Assigning imprecise value to p because of arithmetic operation on addresses.
[eva:alarm] period.c:54: Warning: out of bounds read. assert \valid_read(p);
[eva:alarm] period.c:55: Warning:
pointer downcast. assert (unsigned int)(&vg) ≤ 2147483647;
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ period.c:51: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) garbled mix of &{g}
+ period.c:53: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) garbled mix of &{g}
[scope:rm_asserts] removing 1 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
- g[0..9] ∈ {{ garbled mix of &{vg} (origin: Misaligned {period.c:55}) }}
+ g[0..9] ∈
+ {{ garbled mix of &{vg} (origin: Misaligned write {period.c:55}) }}
Frama_C_periodic_t_320[0] ∈ {1}
[1..3] ∈ {0}
[4] ∈ {24}
diff --git a/tests/value/oracle/recursion.0.res.oracle b/tests/value/oracle/recursion.0.res.oracle
index fd044aab639e3557a18f31a7ca6e5c4194ca3689..cb1dcc89815e6b7e167b7eb1a22971dcd955bda1 100644
--- a/tests/value/oracle/recursion.0.res.oracle
+++ b/tests/value/oracle/recursion.0.res.oracle
@@ -226,6 +226,9 @@
Analysis of function escaping_stack is thus incomplete and its soundness
relies on the written specification.
[eva] using specification for function escaping_stack
+[eva:garbled-mix:assigns] recursion.c:311:
+ The specification of function escaping_stack
+ has generated a garbled mix of addresses for assigns clause p.
[eva:alarm] recursion.c:313: Warning: out of bounds write. assert \valid(p);
[eva] recursion.c:314: Frama_C_show_each_1_2: {5}
[eva:locals-escaping] recursion.c:312: Warning:
@@ -236,6 +239,10 @@
Analysis of function decr is thus incomplete and its soundness
relies on the written specification.
[eva] using specification for function decr
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ recursion.c:311: assigns clause on addresses
+ (read 2 times, propagated 1 times) garbled mix of &{x; a; \copy<x>[1]}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function alarm:
res ∈ [10..2147483647]
diff --git a/tests/value/oracle/reduce_by_valid.res.oracle b/tests/value/oracle/reduce_by_valid.res.oracle
index dcea93719575ad63fc979a58b76af32c6ed72407..826021d49273bf80cfb3f3e201cd0fa2cc3507dc 100644
--- a/tests/value/oracle/reduce_by_valid.res.oracle
+++ b/tests/value/oracle/reduce_by_valid.res.oracle
@@ -145,10 +145,10 @@
[eva] computing for function garbled_mix <- main12 <- main.
Called from reduce_by_valid.i:272.
[eva] using specification for function garbled_mix
+[eva:garbled-mix:assigns] reduce_by_valid.i:272:
+ The specification of function garbled_mix
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function garbled_mix
-[eva:garbled-mix:write] reduce_by_valid.i:272:
- Assigning imprecise value to p.
- The imprecision originates from Library function {reduce_by_valid.i:272}
[eva] reduce_by_valid.i:273:
Frama_C_show_each_gm:
{{ garbled mix of &{x; a}
@@ -170,15 +170,19 @@
out of bounds write. assert \valid(r);
[eva] computing for function garbled_mix <- main12 <- main.
Called from reduce_by_valid.i:290.
+[eva:garbled-mix:assigns] reduce_by_valid.i:290:
+ The specification of function garbled_mix
+ has generated a garbled mix of addresses for assigns clause \result.
[eva] Done for function garbled_mix
-[eva:garbled-mix:write] reduce_by_valid.i:290:
- Assigning imprecise value to r.
- The imprecision originates from Library function {reduce_by_valid.i:290}
[eva:alarm] reduce_by_valid.i:291: Warning: assertion got status unknown.
[eva] Recording results for main12
[eva] Done for function main12
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ reduce_by_valid.i:272: assigns clause on addresses
+ (read 3 times, propagated 2 times) garbled mix of &{x; a}
[scope:rm_asserts] removing 12 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main1:
diff --git a/tests/value/oracle/shift.0.res.oracle b/tests/value/oracle/shift.0.res.oracle
index bb1cdf0553127b21f9ad900a7b60b2580fc218de..38218467e1391e87dd16adb079beca1594aa854e 100644
--- a/tests/value/oracle/shift.0.res.oracle
+++ b/tests/value/oracle/shift.0.res.oracle
@@ -42,8 +42,7 @@
[eva:alarm] shift.i:52: Warning:
unsigned overflow. assert (unsigned long)((char *)t) << 8 ≤ 4294967295;
[eva:garbled-mix:write] shift.i:52:
- Assigning imprecise value to r.
- The imprecision originates from Arithmetic {shift.i:52}
+ Assigning imprecise value to r because of arithmetic operation on addresses.
[eva:alarm] shift.i:53: Warning:
pointer downcast. assert (unsigned int)((char *)t) ≤ 2147483647;
[eva:alarm] shift.i:53: Warning:
@@ -58,13 +57,14 @@
[eva:alarm] shift.i:53: Warning:
signed overflow.
assert (long)r + (long)((long)((char *)t) << 8) ≤ 2147483647;
-[eva:garbled-mix:write] shift.i:53:
- Assigning imprecise value to r.
- The imprecision originates from Arithmetic
[eva:alarm] shift.i:58: Warning:
unsigned overflow. assert 2U << 31 ≤ 4294967295;
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ shift.i:52: arithmetic operation on addresses
+ (read 1 times, propagated 2 times) garbled mix of &{t}
[eva] shift.i:35: assertion 'Eva,shift' got final status invalid.
[eva] shift.i:36: assertion 'Eva,shift' got final status invalid.
[eva] shift.i:40: assertion 'Eva,shift' got final status invalid.
diff --git a/tests/value/oracle/shift.1.res.oracle b/tests/value/oracle/shift.1.res.oracle
index 601488698eb84a19f1a5ff51d8cd97c3ac787d0e..cf118f59bd758f7162dbcf25ddf0b285625eaa62 100644
--- a/tests/value/oracle/shift.1.res.oracle
+++ b/tests/value/oracle/shift.1.res.oracle
@@ -36,8 +36,7 @@
[eva] shift.i:48:
Frama_C_show_each: {{ "ua:%u\nub:%u\n" }}, {1401}, {1073741074}
[eva:garbled-mix:write] shift.i:52:
- Assigning imprecise value to r.
- The imprecision originates from Arithmetic {shift.i:52}
+ Assigning imprecise value to r because of arithmetic operation on addresses.
[eva:alarm] shift.i:53: Warning:
pointer downcast. assert (unsigned int)((char *)t) ≤ 2147483647;
[eva:alarm] shift.i:53: Warning:
@@ -50,11 +49,12 @@
[eva:alarm] shift.i:53: Warning:
signed overflow.
assert (long)r + (long)((long)((char *)t) << 8) ≤ 2147483647;
-[eva:garbled-mix:write] shift.i:53:
- Assigning imprecise value to r.
- The imprecision originates from Arithmetic
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ shift.i:52: arithmetic operation on addresses
+ (read 1 times, propagated 2 times) garbled mix of &{t}
[eva] shift.i:35: assertion 'Eva,shift' got final status invalid.
[eva] shift.i:36: assertion 'Eva,shift' got final status invalid.
[eva] shift.i:40: assertion 'Eva,shift' got final status invalid.
diff --git a/tests/value/oracle/sizeof.res.oracle b/tests/value/oracle/sizeof.res.oracle
index e9b64cb2ded5b0d9df7a1b6e5661cfc40e6f782e..aa6a36837e24f63aa3c3f9e895594f1743c78872 100644
--- a/tests/value/oracle/sizeof.res.oracle
+++ b/tests/value/oracle/sizeof.res.oracle
@@ -21,8 +21,7 @@
[eva:alarm] sizeof.i:32: Warning:
pointer downcast. assert (unsigned int)(&s1) ≤ 2147483647;
[eva:garbled-mix:write] sizeof.i:32:
- Assigning imprecise value to p.
- The imprecision originates from Arithmetic {sizeof.i:32}
+ Assigning imprecise value to p because of arithmetic operation on addresses.
[eva:alarm] sizeof.i:33: Warning:
accessing out of bounds index.
assert (unsigned int)(sizeof(int [10]) - (unsigned int)i) < 10;
@@ -47,6 +46,10 @@
[eva] Done for function f
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ sizeof.i:32: arithmetic operation on addresses
+ (read 2 times, propagated 1 times) garbled mix of &{s1}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function f:
diff --git a/tests/value/oracle/struct3.res.oracle b/tests/value/oracle/struct3.res.oracle
index 20c83c1fc97b7e5983a55566c669ea7d3b98d68c..795a309294796edcca100322d47c6aa0466208fb 100644
--- a/tests/value/oracle/struct3.res.oracle
+++ b/tests/value/oracle/struct3.res.oracle
@@ -24,13 +24,10 @@
[eva:alarm] struct3.i:46: Warning:
pointer downcast. assert (unsigned int)(s2.c + (int)s2.c) ≤ 2147483647;
[eva:garbled-mix:write] struct3.i:46: Warning:
- Assigning imprecise value to s2.a.
- The imprecision originates from Arithmetic {struct3.i:46}
+ Assigning imprecise value to s2.a
+ because of arithmetic operation on addresses.
[eva] Recording results for main
[eva] Done for function main
-[eva:garbled-mix:summary] Warning:
- Garbled mix generated during analysis:
- {{ garbled mix of &{s1} (origin: Arithmetic {struct3.i:46}) }}
[eva] struct3.i:42: assertion 'Eva,index_bound' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
diff --git a/tests/value/oracle/va_list2.0.res.oracle b/tests/value/oracle/va_list2.0.res.oracle
index 619211814b41de75cdd428ff271735802110dfd5..2b3a7d3e4a6bb9f37aa3a50764303572b75e81ae 100644
--- a/tests/value/oracle/va_list2.0.res.oracle
+++ b/tests/value/oracle/va_list2.0.res.oracle
@@ -13,12 +13,6 @@
out of bounds read. assert \valid_read(args);
[eva:alarm] va_list2.c:15: Warning:
out of bounds read. assert \valid_read((int *)*args);
-[eva:garbled-mix:write] va_list2.c:15:
- Assigning imprecise value to tmp.
- The imprecision originates from Well
-[eva:garbled-mix:write] va_list2.c:15:
- Assigning imprecise value to i.
- The imprecision originates from Well
[eva] va_list2.c:16:
Frama_C_show_each_i: {{ garbled mix of &{S_0_S___va_params} (origin: Well) }}
[eva:alarm] va_list2.c:20: Warning:
@@ -27,15 +21,9 @@
out of bounds read. assert \valid_read((float *)*args);
[eva:alarm] va_list2.c:20: Warning:
non-finite float value. assert \is_finite(*((float *)*args));
-[eva:garbled-mix:write] va_list2.c:20:
- Assigning imprecise value to tmp_0.
- The imprecision originates from Well
[eva:alarm] va_list2.c:20: Warning:
non-finite float value. assert \is_finite(tmp_0);
(tmp_0 from vararg)
-[eva:garbled-mix:write] va_list2.c:20:
- Assigning imprecise value to f.
- The imprecision originates from Well
[eva] va_list2.c:21:
Frama_C_show_each_f: {{ garbled mix of &{S_0_S___va_params} (origin: Well) }}
[eva] va_list2.c:12: starting to merge loop iterations
@@ -48,6 +36,10 @@
{{ garbled mix of &{S_0_S___va_params; S_1_S___va_params} (origin: Well) }}
[eva] Recording results for main
[eva] Done for function main
+[eva:garbled-mix:summary]
+ Origins of garbled mix generated during analysis:
+ Initial state (read 24 times, propagated 10 times)
+ garbled mix of &{S_0_S___va_params; S_1_S___va_params}
[scope:rm_asserts] removing 1 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
diff --git a/tests/value/oracle_apron/backward_add_ptr.res.oracle b/tests/value/oracle_apron/backward_add_ptr.res.oracle
index 0b3c21f037c9ee69262a15f6e7398ffa44360062..04bf26aed2a3d76fb3e5f7a704d63846dbaab183 100644
--- a/tests/value/oracle_apron/backward_add_ptr.res.oracle
+++ b/tests/value/oracle_apron/backward_add_ptr.res.oracle
@@ -1,28 +1,32 @@
-64c64,67
+58c58,61
< [eva] backward_add_ptr.c:91: Reusing old results for call to gm
---
> [eva] computing for function gm <- main3 <- main.
> Called from backward_add_ptr.c:91.
> [eva] Recording results for gm
> [eva] Done for function gm
-84c87,90
+72c75,78
< [eva] backward_add_ptr.c:110: Reusing old results for call to gm
---
> [eva] computing for function gm <- main3 <- main.
> Called from backward_add_ptr.c:110.
> [eva] Recording results for gm
> [eva] Done for function gm
-96c102,105
+81c87,90
< [eva] backward_add_ptr.c:125: Reusing old results for call to gm
---
> [eva] computing for function gm <- main3 <- main.
> Called from backward_add_ptr.c:125.
> [eva] Recording results for gm
> [eva] Done for function gm
-145c154,157
+118c127,130
< [eva] backward_add_ptr.c:160: Reusing old results for call to gm
---
> [eva] computing for function gm <- main4 <- main.
> Called from backward_add_ptr.c:160.
> [eva] Recording results for gm
> [eva] Done for function gm
+154c166
+< (read 81 times, propagated 20 times) garbled mix of &{a; b; a; b; c}
+---
+> (read 81 times, propagated 28 times) garbled mix of &{a; b; a; b; c}
diff --git a/tests/value/oracle_apron/gauges.res.oracle b/tests/value/oracle_apron/gauges.res.oracle
index f92d9c4624085811acfa7d68741f16f06a0b61c4..e39bbda029892bd78f7dccf1f133ee3e51428468 100644
--- a/tests/value/oracle_apron/gauges.res.oracle
+++ b/tests/value/oracle_apron/gauges.res.oracle
@@ -17,36 +17,36 @@
< [eva:alarm] gauges.c:99: Warning: signed overflow. assert c + 1 ≤ 2147483647;
175d171
< [eva:alarm] gauges.c:140: Warning: signed overflow. assert j + 1 ≤ 2147483647;
-285,286d280
+281,282d276
< [eva:alarm] gauges.c:220: Warning:
< signed overflow. assert -2147483648 ≤ n - 1;
-300,302c294
+296,298c290
< [eva:alarm] gauges.c:240: Warning: signed overflow. assert j + 1 ≤ 2147483647;
< [eva] gauges.c:242:
< Frama_C_show_each: {45; 46; 47; 48; 49; 50; 51}, [0..2147483647]
---
> [eva] gauges.c:242: Frama_C_show_each: {45; 46; 47; 48; 49; 50; 51}, [0..46]
-308,310c300
+304,306c296
< [eva:alarm] gauges.c:251: Warning: signed overflow. assert j + 1 ≤ 2147483647;
< [eva] gauges.c:254:
< Frama_C_show_each: {48; 49; 50; 51; 52; 53; 54}, [0..2147483647]
---
> [eva] gauges.c:254: Frama_C_show_each: {48; 49; 50; 51; 52; 53; 54}, [0..49]
-316d305
+312d301
< [eva:alarm] gauges.c:263: Warning: signed overflow. assert j + 1 ≤ 2147483647;
-318c307
+314c303
< Frama_C_show_each: {-59; -58; -57; -56; -55; -54; -53}, [0..2147483647]
---
> Frama_C_show_each: {-59; -58; -57; -56; -55; -54; -53}, [0..65]
-324d312
+320d308
< [eva:alarm] gauges.c:274: Warning: signed overflow. assert j + 1 ≤ 2147483647;
-326c314
+322c310
< Frama_C_show_each: {-64; -63; -62; -61; -60; -59; -58}, [0..2147483647]
---
> Frama_C_show_each: {-64; -63; -62; -61; -60; -59; -58}, [0..70]
-334d321
+330d317
< [eva:alarm] gauges.c:293: Warning: signed overflow. assert j + 1 ≤ 2147483647;
-336c323
+332c319
< Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647]
---
> Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..598]
diff --git a/tests/value/oracle_bitwise/addition.res.oracle b/tests/value/oracle_bitwise/addition.res.oracle
deleted file mode 100644
index f65148d676c435df46dbec93bc4f3958019e7208..0000000000000000000000000000000000000000
--- a/tests/value/oracle_bitwise/addition.res.oracle
+++ /dev/null
@@ -1,16 +0,0 @@
-123d122
-< The imprecision originates from Arithmetic {addition.i:52}
-162a162
-> {{ garbled mix of &{p1} (origin: Misaligned {addition.i:52}) }}
-163a164
-> {{ garbled mix of &{p2} (origin: Misaligned {addition.i:56}) }}
-186c187
-< p10 ∈ {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}
----
-> p10 ∈ {{ garbled mix of &{p1} }}
-405a407
-> {{ garbled mix of &{p1} (origin: Misaligned {addition.i:52}) }}
-429c431
-< p10 ∈ {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}
----
-> p10 ∈ {{ garbled mix of &{p1} }}
diff --git a/tests/value/oracle_bitwise/bitwise_pointer.0.res.oracle b/tests/value/oracle_bitwise/bitwise_pointer.0.res.oracle
deleted file mode 100644
index 370739039c6f31f1307fdab215ccdd958820f386..0000000000000000000000000000000000000000
--- a/tests/value/oracle_bitwise/bitwise_pointer.0.res.oracle
+++ /dev/null
@@ -1,12 +0,0 @@
-34,36c34
-< [eva:garbled-mix:write] bitwise_pointer.i:18:
-< Assigning imprecise value to p.
-< The imprecision originates from Arithmetic {bitwise_pointer.i:18}
----
-> [eva:garbled-mix:write] bitwise_pointer.i:18: Assigning imprecise value to p.
-41,43c39
-< [eva:garbled-mix:write] bitwise_pointer.i:22:
-< Assigning imprecise value to p1.
-< The imprecision originates from Arithmetic {bitwise_pointer.i:22}
----
-> [eva:garbled-mix:write] bitwise_pointer.i:22: Assigning imprecise value to p1.
diff --git a/tests/value/oracle_bitwise/bitwise_pointer.1.res.oracle b/tests/value/oracle_bitwise/bitwise_pointer.1.res.oracle
deleted file mode 100644
index 370739039c6f31f1307fdab215ccdd958820f386..0000000000000000000000000000000000000000
--- a/tests/value/oracle_bitwise/bitwise_pointer.1.res.oracle
+++ /dev/null
@@ -1,12 +0,0 @@
-34,36c34
-< [eva:garbled-mix:write] bitwise_pointer.i:18:
-< Assigning imprecise value to p.
-< The imprecision originates from Arithmetic {bitwise_pointer.i:18}
----
-> [eva:garbled-mix:write] bitwise_pointer.i:18: Assigning imprecise value to p.
-41,43c39
-< [eva:garbled-mix:write] bitwise_pointer.i:22:
-< Assigning imprecise value to p1.
-< The imprecision originates from Arithmetic {bitwise_pointer.i:22}
----
-> [eva:garbled-mix:write] bitwise_pointer.i:22: Assigning imprecise value to p1.
diff --git a/tests/value/oracle_bitwise/logic_ptr_cast.res.oracle b/tests/value/oracle_bitwise/logic_ptr_cast.res.oracle
deleted file mode 100644
index 60fe515050a5108521f39a3d59b01e51cb848735..0000000000000000000000000000000000000000
--- a/tests/value/oracle_bitwise/logic_ptr_cast.res.oracle
+++ /dev/null
@@ -1,6 +0,0 @@
-8,10c8
-< [eva:garbled-mix:write] logic_ptr_cast.i:8:
-< Assigning imprecise value to p.
-< The imprecision originates from Arithmetic {logic_ptr_cast.i:8}
----
-> [eva:garbled-mix:write] logic_ptr_cast.i:8: Assigning imprecise value to p.
diff --git a/tests/value/oracle_equality/addition.res.oracle b/tests/value/oracle_equality/addition.res.oracle
index 05493bd86cacf8b5cd209c6f697a5afa28c210c5..5a0da48b045e46f9201b4058cfc0010bef15e6cc 100644
--- a/tests/value/oracle_equality/addition.res.oracle
+++ b/tests/value/oracle_equality/addition.res.oracle
@@ -1,18 +1,36 @@
-138,141d137
+129,134d128
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
-168c164
+< [eva:garbled-mix:write] addition.i:61: Warning:
+< Assigning imprecise value to p14 because of misaligned read of addresses.
+141c135,139
< [scope:rm_asserts] removing 9 assertion(s)
---
+> [eva:garbled-mix:summary] Warning:
+> Origins of garbled mix generated during analysis:
+> addition.i:59: misaligned read of addresses
+> (read 1 times, propagated 2 times) garbled mix of &{p1}
> [scope:rm_asserts] removing 7 assertion(s)
-384,387d379
+165c163
+< {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
+---
+> {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
+359,362d356
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
-410c402
+368c362,366
< [scope:rm_asserts] removing 9 assertion(s)
---
+> [eva:garbled-mix:summary] Warning:
+> Origins of garbled mix generated during analysis:
+> addition.i:59: misaligned read of addresses
+> (read 1 times, propagated 2 times) garbled mix of &{p1}
> [scope:rm_asserts] removing 7 assertion(s)
+393c391
+< {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
+---
+> {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
diff --git a/tests/value/oracle_equality/arith_pointer.res.oracle b/tests/value/oracle_equality/arith_pointer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e8d12d536a5435ae4567640619599a9d10b2e3ab
--- /dev/null
+++ b/tests/value/oracle_equality/arith_pointer.res.oracle
@@ -0,0 +1,8 @@
+48c48
+< (read 2 times, propagated 2 times) garbled mix of &{x}
+---
+> (read 3 times, propagated 2 times) garbled mix of &{x}
+161c161
+< (read 2 times, propagated 2 times) garbled mix of &{x}
+---
+> (read 3 times, propagated 2 times) garbled mix of &{x}
diff --git a/tests/value/oracle_equality/assigns.res.oracle b/tests/value/oracle_equality/assigns.res.oracle
index 0f5f7cdfe8d3e4b52e991076bcc82bf5bf9d9539..f423e4eb8cc93ea8dd508d87d6f093838268f3b4 100644
--- a/tests/value/oracle_equality/assigns.res.oracle
+++ b/tests/value/oracle_equality/assigns.res.oracle
@@ -1,6 +1,6 @@
-149,150d148
+154,155d153
< more than 200(1000) locations to update in array. Approximating.
< [kernel] assigns.i:104:
-151a150,151
+156a155,156
> [kernel] assigns.i:104:
> more than 200(1000) locations to update in array. Approximating.
diff --git a/tests/value/oracle_equality/backward_add_ptr.res.oracle b/tests/value/oracle_equality/backward_add_ptr.res.oracle
index 3a6305e610f4b9491eff8fa269924571213a2b3b..1b7ff53fec0b3b7db573cd6fc15fa8834ae8b229 100644
--- a/tests/value/oracle_equality/backward_add_ptr.res.oracle
+++ b/tests/value/oracle_equality/backward_add_ptr.res.oracle
@@ -2,88 +2,28 @@
< [eva] backward_add_ptr.c:26: Frama_C_show_each_only_a: {0; 1}, {{ &a }}, {0}
---
> [eva] backward_add_ptr.c:26: Frama_C_show_each_only_a: {0}, {{ &a }}, {0}
-84c84,87
+72c72,75
< [eva] backward_add_ptr.c:110: Reusing old results for call to gm
---
> [eva] computing for function gm <- main3 <- main.
> Called from backward_add_ptr.c:110.
> [eva] Recording results for gm
> [eva] Done for function gm
-96c99,102
+81c84,87
< [eva] backward_add_ptr.c:125: Reusing old results for call to gm
---
> [eva] computing for function gm <- main3 <- main.
> Called from backward_add_ptr.c:125.
> [eva] Recording results for gm
> [eva] Done for function gm
-107c113
-< (origin: Arithmetic {backward_add_ptr.c:68}) }},
----
-> (origin: Arithmetic Bottom) }},
-142,145c148,152
-< {{ garbled mix of &{b}
-< (origin: Arithmetic {backward_add_ptr.c:68}) }},
-< [0..4294967295]
+118c124,127
< [eva] backward_add_ptr.c:160: Reusing old results for call to gm
---
-> {{ garbled mix of &{b} (origin: Arithmetic Bottom) }}, [0..4294967295]
> [eva] computing for function gm <- main4 <- main.
> Called from backward_add_ptr.c:160.
> [eva] Recording results for gm
> [eva] Done for function gm
-161c168
-< (origin: Arithmetic {backward_add_ptr.c:68}) }},
----
-> (origin: Arithmetic Bottom) }},
-163c170
-< (origin: Arithmetic {backward_add_ptr.c:68}) }}
----
-> (origin: Arithmetic Bottom) }}
-171c178
-< (origin: Arithmetic {backward_add_ptr.c:68}) }}
----
-> (origin: Arithmetic Bottom) }}
-177c184
-< (origin: Arithmetic {backward_add_ptr.c:68}) }},
----
-> (origin: Arithmetic Bottom) }},
-189a197,198
-> {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:33}) }}
-> {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:33}) }}
-200a210
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:106}) }}
-202c212
-< {{ garbled mix of &{c} (origin: Arithmetic {backward_add_ptr.c:115}) }}
+154c163
+< (read 81 times, propagated 20 times) garbled mix of &{a; b; a; b; c}
---
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:107}) }}
-203a214,216
-> {{ garbled mix of &{c} (origin: Arithmetic {backward_add_ptr.c:115}) }}
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:116}) }}
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:121}) }}
-204a218,219
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:122}) }}
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:130}) }}
-205a221
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:136}) }}
-206a223
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:137}) }}
-207a225
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:145}) }}
-208a227,230
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:150}) }}
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:151}) }}
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:156}) }}
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:157}) }}
-209a232,243
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:165}) }}
-> {{ garbled mix of &{b; c} (origin: Arithmetic {backward_add_ptr.c:165}) }}
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:166}) }}
-> {{ garbled mix of &{b; c} (origin: Arithmetic {backward_add_ptr.c:166}) }}
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:171}) }}
-> {{ garbled mix of &{b; c} (origin: Arithmetic {backward_add_ptr.c:171}) }}
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:172}) }}
-> {{ garbled mix of &{b; c} (origin: Arithmetic {backward_add_ptr.c:172}) }}
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:177}) }}
-> {{ garbled mix of &{b; c} (origin: Arithmetic {backward_add_ptr.c:177}) }}
-> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:178}) }}
-> {{ garbled mix of &{b; c} (origin: Arithmetic {backward_add_ptr.c:178}) }}
+> (read 86 times, propagated 26 times) garbled mix of &{a; b; a; b; c}
diff --git a/tests/value/oracle_equality/bitfield.res.oracle b/tests/value/oracle_equality/bitfield.res.oracle
index 9886a5a3b66d5f82e84afc4a5a3b268b67994a12..d8fa5662f8993ea18aae6c740069a2253c9740e2 100644
--- a/tests/value/oracle_equality/bitfield.res.oracle
+++ b/tests/value/oracle_equality/bitfield.res.oracle
@@ -1,4 +1,8 @@
137a138,140
> [eva] bitfield.i:71:
> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
+213c216
+< (read 5 times, propagated 7 times) garbled mix of &{b; ee}
+---
+> (read 6 times, propagated 7 times) garbled mix of &{b; ee}
diff --git a/tests/value/oracle_equality/bitwise_pointer.0.res.oracle b/tests/value/oracle_equality/bitwise_pointer.0.res.oracle
index f04f7077977a5a61ea7d346c6ff6f90a2e4237e4..688b8e07ea0d94b9b3a3e8c2d26e5ff3a5a8f9e6 100644
--- a/tests/value/oracle_equality/bitwise_pointer.0.res.oracle
+++ b/tests/value/oracle_equality/bitwise_pointer.0.res.oracle
@@ -1,8 +1,8 @@
-62c62
+66c66
< x ∈ [0..9]
---
> x ∈ {5}
-75c75
+79c79
< x1 ∈ [0..9]
---
> x1 ∈ {5}
diff --git a/tests/value/oracle_equality/bitwise_pointer.1.res.oracle b/tests/value/oracle_equality/bitwise_pointer.1.res.oracle
index f04f7077977a5a61ea7d346c6ff6f90a2e4237e4..688b8e07ea0d94b9b3a3e8c2d26e5ff3a5a8f9e6 100644
--- a/tests/value/oracle_equality/bitwise_pointer.1.res.oracle
+++ b/tests/value/oracle_equality/bitwise_pointer.1.res.oracle
@@ -1,8 +1,8 @@
-62c62
+66c66
< x ∈ [0..9]
---
> x ∈ {5}
-75c75
+79c79
< x1 ∈ [0..9]
---
> x1 ∈ {5}
diff --git a/tests/value/oracle_equality/context_free.res.oracle b/tests/value/oracle_equality/context_free.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..edf1bab4ce0f782dcf8cacb94936e89dd482ddbb
--- /dev/null
+++ b/tests/value/oracle_equality/context_free.res.oracle
@@ -0,0 +1,4 @@
+95c95
+< Initial state (read 9 times, propagated 5 times)
+---
+> Initial state (read 11 times, propagated 5 times)
diff --git a/tests/value/oracle_equality/empty_struct.6.res.oracle b/tests/value/oracle_equality/empty_struct.6.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a5fdd6006f01b6a3c868dca147b94ac07083a5ae
--- /dev/null
+++ b/tests/value/oracle_equality/empty_struct.6.res.oracle
@@ -0,0 +1,4 @@
+27c27
+< (read 2 times, propagated 3 times) garbled mix of &{gs}
+---
+> (read 3 times, propagated 3 times) garbled mix of &{gs}
diff --git a/tests/value/oracle_equality/gauges.res.oracle b/tests/value/oracle_equality/gauges.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1375772daf32d94c39da70a45a329a0af7e75df1
--- /dev/null
+++ b/tests/value/oracle_equality/gauges.res.oracle
@@ -0,0 +1,4 @@
+716c716
+< (read 14 times, propagated 12 times) garbled mix of &{x; y}
+---
+> (read 20 times, propagated 12 times) garbled mix of &{x; y}
diff --git a/tests/value/oracle_equality/imprecise_invalid_write.res.oracle b/tests/value/oracle_equality/imprecise_invalid_write.res.oracle
index bb982e73d80195bfc94798bd4ae7791b502f93ef..1306d9d6c575eaba355d3aa332df2ba32c5ef554 100644
--- a/tests/value/oracle_equality/imprecise_invalid_write.res.oracle
+++ b/tests/value/oracle_equality/imprecise_invalid_write.res.oracle
@@ -1,3 +1,3 @@
-28a29,30
+27a28,29
> [kernel] imprecise_invalid_write.i:9:
> imprecise size for variable main1 (Undefined sizeof on a function.)
diff --git a/tests/value/oracle_equality/origin.0.res.oracle b/tests/value/oracle_equality/origin.0.res.oracle
index fca55cdcd1617b76c6bd48031be44f3befefd3c2..a12449e315cdcbf000a4adcafec176f044d53066 100644
--- a/tests/value/oracle_equality/origin.0.res.oracle
+++ b/tests/value/oracle_equality/origin.0.res.oracle
@@ -1,9 +1,9 @@
-237,238c237
+246,247c246
< pm2[bits 0 to 15]# ∈ {{ (? *)&a }}%32, bits 16 to 31
< [bits 16 to 31]# ∈ {{ (? *)&b }}%32, bits 0 to 15
---
> pm2 ∈ {{ &a + {-4} ; &b + {-4} }}
-272,273c271
+281,282c280
< pm2[bits 0 to 15]# ∈ {{ (? *)&a }}%32, bits 16 to 31
< [bits 16 to 31]# ∈ {{ (? *)&b }}%32, bits 0 to 15
---
diff --git a/tests/value/oracle_equality/period.res.oracle b/tests/value/oracle_equality/period.res.oracle
index 315304aca0443b62c2263315e5e8e4a5b70abc99..657c13125d1d186b4e4b752cd479fb28e639a08b 100644
--- a/tests/value/oracle_equality/period.res.oracle
+++ b/tests/value/oracle_equality/period.res.oracle
@@ -1,9 +1,10 @@
-89,94d88
+88,92d87
< [eva:alarm] period.c:53: Warning:
< pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
< [eva:garbled-mix:write] period.c:53:
-< Assigning imprecise value to p.
-< The imprecision originates from Arithmetic {period.c:53}
+< Assigning imprecise value to p because of arithmetic operation on addresses.
< [eva:alarm] period.c:54: Warning: out of bounds read. assert \valid_read(p);
-99d92
+101,103d95
+< period.c:53: arithmetic operation on addresses
+< (read 2 times, propagated 1 times) garbled mix of &{g}
< [scope:rm_asserts] removing 1 assertion(s)
diff --git a/tests/value/oracle_equality/va_list2.0.res.oracle b/tests/value/oracle_equality/va_list2.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2907faaa45d2cec4207024217ed66cf9699b41f8
--- /dev/null
+++ b/tests/value/oracle_equality/va_list2.0.res.oracle
@@ -0,0 +1,4 @@
+41c41
+< Initial state (read 24 times, propagated 10 times)
+---
+> Initial state (read 28 times, propagated 10 times)
diff --git a/tests/value/oracle_gauges/bitfield.res.oracle b/tests/value/oracle_gauges/bitfield.res.oracle
index e0125a5db691f59d2cacd6f04887d761975891e2..619b7b85a2389c7c7816e21f58c56851130dcdb0 100644
--- a/tests/value/oracle_gauges/bitfield.res.oracle
+++ b/tests/value/oracle_gauges/bitfield.res.oracle
@@ -1,16 +1,20 @@
137a138,152
> [eva] bitfield.i:71:
> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
> [eva] bitfield.i:73:
> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
> [eva] computing for function leaf <- imprecise_bts_1671 <- main.
> Called from bitfield.i:70.
> [eva] Done for function leaf
> [eva] bitfield.i:71:
> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
> [eva] bitfield.i:73:
> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
+213c228
+< (read 5 times, propagated 7 times) garbled mix of &{b; ee}
+---
+> (read 9 times, propagated 11 times) garbled mix of &{b; ee}
diff --git a/tests/value/oracle_gauges/gauges.res.oracle b/tests/value/oracle_gauges/gauges.res.oracle
index 89bba971700e381aecb42f0a87e0010a27a5a7d7..9d4462e029b227ddad11d18dc38dee160fab8cff 100644
--- a/tests/value/oracle_gauges/gauges.res.oracle
+++ b/tests/value/oracle_gauges/gauges.res.oracle
@@ -54,82 +54,82 @@
---
> [eva] gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
> [eva] gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
-244,245d225
+240,241d221
< [eva:alarm] gauges.c:192: Warning: out of bounds write. assert \valid(p);
< [eva:alarm] gauges.c:193: Warning: out of bounds write. assert \valid(q);
-253,258d232
+249,254d228
< [eva:alarm] gauges.c:202: Warning:
< out of bounds read. assert \valid_read(tmp);
< (tmp from A++)
< [eva:alarm] gauges.c:202: Warning:
< out of bounds read. assert \valid_read(tmp_0);
< (tmp_0 from B++)
-285,286d258
+281,282d254
< [eva:alarm] gauges.c:220: Warning:
< signed overflow. assert -2147483648 ≤ n - 1;
-300,302c272
+296,298c268
< [eva:alarm] gauges.c:240: Warning: signed overflow. assert j + 1 ≤ 2147483647;
< [eva] gauges.c:242:
< Frama_C_show_each: {45; 46; 47; 48; 49; 50; 51}, [0..2147483647]
---
> [eva] gauges.c:242: Frama_C_show_each: {47; 48}, {6}
-308,310c278
+304,306c274
< [eva:alarm] gauges.c:251: Warning: signed overflow. assert j + 1 ≤ 2147483647;
< [eva] gauges.c:254:
< Frama_C_show_each: {48; 49; 50; 51; 52; 53; 54}, [0..2147483647]
---
> [eva] gauges.c:254: Frama_C_show_each: {48; 49; 50; 51; 52; 53; 54}, {6; 7}
-316,318c284
+312,314c280
< [eva:alarm] gauges.c:263: Warning: signed overflow. assert j + 1 ≤ 2147483647;
< [eva] gauges.c:265:
< Frama_C_show_each: {-59; -58; -57; -56; -55; -54; -53}, [0..2147483647]
---
> [eva] gauges.c:265: Frama_C_show_each: {-58; -57}, {9}
-324d289
+320d285
< [eva:alarm] gauges.c:274: Warning: signed overflow. assert j + 1 ≤ 2147483647;
-326c291
+322c287
< Frama_C_show_each: {-64; -63; -62; -61; -60; -59; -58}, [0..2147483647]
---
> Frama_C_show_each: {-64; -63; -62; -61; -60; -59; -58}, {9; 10}
-334d298
+330d294
< [eva:alarm] gauges.c:293: Warning: signed overflow. assert j + 1 ≤ 2147483647;
-336c300
+332c296
< Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647]
---
> Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [99..119]
-398a363,366
+394a359,362
> # gauges:
> V: [{[ p -> {{ &x }}
> i -> {1} ]}]
> s398: λ(0)
-458a427,430
+454a423,426
> # gauges:
> V: [{[ i -> {1} ]}]
> s398: λ([0 .. 1])
> {[ i -> {1} ]}
-517a490,493
+513a486,489
> # gauges:
> V: [{[ i -> {1} ]}]
> s398: λ([0 .. 2])
> {[ i -> {1} ]}
-576a553,556
+572a549,552
> # gauges:
> V: [{[ i -> {1} ]}]
> s398: λ([0 .. 10])
> {[ i -> {1} ]}
-641a622,626
+637a618,622
> # gauges:
> V: [{[ p -> {{ &a }}
> i -> {2} ]}]
> s412: λ(0)
> s411: λ(0)
-702a688,692
+698a684,688
> # gauges:
> V: [{[ i -> {2} ]}]
> s412: λ(0)
> s411: λ([0 .. 1])
> {[ i -> {0} ]}
-704a695,822
+700a691,818
> [eva] gauges.c:325:
> Frama_C_dump_each:
> # cvalue:
@@ -258,9 +258,13 @@
> s411: λ([0 .. +oo])
> {[ i -> {0} ]}
> ==END OF DUMP==
-712a831,832
+708a827,828
> [eva] gauges.c:343: Call to builtin malloc
> [eva] gauges.c:343: Call to builtin malloc
+716c836
+< (read 14 times, propagated 12 times) garbled mix of &{x; y}
+---
+> (read 12 times, propagated 11 times) garbled mix of &{x; y}
765,766c885,886
< A ∈ {{ &A + [0..--],0%4 }}
< B ∈ {{ &B + [0..--],0%4 }}
diff --git a/tests/value/oracle_gauges/va_list2.0.res.oracle b/tests/value/oracle_gauges/va_list2.0.res.oracle
index 028514ddc800f41a22034f68671bf0c604ea9734..70defd3cb22fe585b3ac25d1cbc4a5509d95456b 100644
--- a/tests/value/oracle_gauges/va_list2.0.res.oracle
+++ b/tests/value/oracle_gauges/va_list2.0.res.oracle
@@ -1,4 +1,4 @@
-48a49,60
+36a37,48
> [eva] va_list2.c:16:
> Frama_C_show_each_i:
> {{ garbled mix of &{S_0_S___va_params; S_1_S___va_params} (origin: Well) }}
@@ -11,3 +11,7 @@
> [eva] va_list2.c:21:
> Frama_C_show_each_f:
> {{ garbled mix of &{S_0_S___va_params; S_1_S___va_params} (origin: Well) }}
+41c53
+< Initial state (read 24 times, propagated 10 times)
+---
+> Initial state (read 36 times, propagated 16 times)
diff --git a/tests/value/oracle_octagon/assigns.res.oracle b/tests/value/oracle_octagon/assigns.res.oracle
index 0f5f7cdfe8d3e4b52e991076bcc82bf5bf9d9539..f423e4eb8cc93ea8dd508d87d6f093838268f3b4 100644
--- a/tests/value/oracle_octagon/assigns.res.oracle
+++ b/tests/value/oracle_octagon/assigns.res.oracle
@@ -1,6 +1,6 @@
-149,150d148
+154,155d153
< more than 200(1000) locations to update in array. Approximating.
< [kernel] assigns.i:104:
-151a150,151
+156a155,156
> [kernel] assigns.i:104:
> more than 200(1000) locations to update in array. Approximating.
diff --git a/tests/value/oracle_octagon/bitfield.res.oracle b/tests/value/oracle_octagon/bitfield.res.oracle
index 9886a5a3b66d5f82e84afc4a5a3b268b67994a12..d8fa5662f8993ea18aae6c740069a2253c9740e2 100644
--- a/tests/value/oracle_octagon/bitfield.res.oracle
+++ b/tests/value/oracle_octagon/bitfield.res.oracle
@@ -1,4 +1,8 @@
137a138,140
> [eva] bitfield.i:71:
> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
+213c216
+< (read 5 times, propagated 7 times) garbled mix of &{b; ee}
+---
+> (read 6 times, propagated 7 times) garbled mix of &{b; ee}
diff --git a/tests/value/oracle_octagon/gauges.res.oracle b/tests/value/oracle_octagon/gauges.res.oracle
index a5e47e28258fe4726d31ff83cb80079321750697..1b2c6b235548585fb2d4218526d8c76fbed82258 100644
--- a/tests/value/oracle_octagon/gauges.res.oracle
+++ b/tests/value/oracle_octagon/gauges.res.oracle
@@ -1,7 +1,7 @@
-259,260d258
+255,256d254
< [eva:alarm] gauges.c:201: Warning:
< signed overflow. assert -2147483648 ≤ numNonZero - 1;
-282,286d279
+278,282d275
< [eva] gauges.c:218: Frama_C_show_each:
< [eva] gauges.c:218: Frama_C_show_each:
< [eva] gauges.c:218: Frama_C_show_each:
diff --git a/tests/value/oracle_symblocs/assigns.res.oracle b/tests/value/oracle_symblocs/assigns.res.oracle
index 0f5f7cdfe8d3e4b52e991076bcc82bf5bf9d9539..f423e4eb8cc93ea8dd508d87d6f093838268f3b4 100644
--- a/tests/value/oracle_symblocs/assigns.res.oracle
+++ b/tests/value/oracle_symblocs/assigns.res.oracle
@@ -1,6 +1,6 @@
-149,150d148
+154,155d153
< more than 200(1000) locations to update in array. Approximating.
< [kernel] assigns.i:104:
-151a150,151
+156a155,156
> [kernel] assigns.i:104:
> more than 200(1000) locations to update in array. Approximating.
diff --git a/tests/value/oracle_symblocs/bitwise_pointer.0.res.oracle b/tests/value/oracle_symblocs/bitwise_pointer.0.res.oracle
index f04f7077977a5a61ea7d346c6ff6f90a2e4237e4..688b8e07ea0d94b9b3a3e8c2d26e5ff3a5a8f9e6 100644
--- a/tests/value/oracle_symblocs/bitwise_pointer.0.res.oracle
+++ b/tests/value/oracle_symblocs/bitwise_pointer.0.res.oracle
@@ -1,8 +1,8 @@
-62c62
+66c66
< x ∈ [0..9]
---
> x ∈ {5}
-75c75
+79c79
< x1 ∈ [0..9]
---
> x1 ∈ {5}
diff --git a/tests/value/oracle_symblocs/bitwise_pointer.1.res.oracle b/tests/value/oracle_symblocs/bitwise_pointer.1.res.oracle
index f04f7077977a5a61ea7d346c6ff6f90a2e4237e4..688b8e07ea0d94b9b3a3e8c2d26e5ff3a5a8f9e6 100644
--- a/tests/value/oracle_symblocs/bitwise_pointer.1.res.oracle
+++ b/tests/value/oracle_symblocs/bitwise_pointer.1.res.oracle
@@ -1,8 +1,8 @@
-62c62
+66c66
< x ∈ [0..9]
---
> x ∈ {5}
-75c75
+79c79
< x1 ∈ [0..9]
---
> x1 ∈ {5}