diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml
index cd0302182f097efe009c8ea7585809ed908c4857..aa3c9b484b35e309d6343b8bffbfbefdd658254a 100644
--- a/src/kernel_services/abstract_interp/cvalue.ml
+++ b/src/kernel_services/abstract_interp/cvalue.ml
@@ -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..8d37feb25148d6698b36cb3a35f10a51a3d1da9c 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.Arith 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 616bf360823a9acb126f675464f84b7f8ac3d425..a30181b5f0acf78466546d0b0525df9ec98db076 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -287,16 +287,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
diff --git a/src/kernel_services/abstract_interp/map_lattice.ml b/src/kernel_services/abstract_interp/map_lattice.ml
index 7a64bce7a05c21606a7fe6076943933e596c80fd..62bb89ef6cddb8192951f297deaadd932b7f2f2e 100644
--- a/src/kernel_services/abstract_interp/map_lattice.ml
+++ b/src/kernel_services/abstract_interp/map_lattice.ml
@@ -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)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index d13cf425dbb84394334b07e3077475482cce443e..0b88644948d8017cb4c40384c3591101ac45a011 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
@@ -1849,7 +1849,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let origin =
match origin with
| Some origin -> origin
- | None -> Origin.(current K_Misalign_read)
+ | None -> Origin.(current Misalign_read)
in
let v = V.topify_with_origin origin v in
(* TODO: check *)
@@ -1872,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_read) in
let v' = V.topify_with_origin origin v in
if not (V.equal v v') then
Lattice_messages.emit_approximation msg_emitter
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index 4f2c87688de45ace925b3a4e2ff0ca158b33cae9..c3c4b4e1ac47a2492699f46d98ac869ac2ed2def 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -21,258 +21,94 @@
(**************************************************************************)
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
+ | Leaf
+ | Merge
+ | Arith
+
+let kind_rank = function
+ | Misalign_read -> 0
+ | Leaf -> 1
+ | Merge -> 2
+ | Arith -> 3
+
+let kind_label = function
+ | Misalign_read -> "Misaligned"
+ | 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
-let well = Well
-
-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 ())
+module Id = State_builder.Counter (struct let name = "Origin.Id" end)
-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 current kind =
+ let id = Id.next () in
+ let loc = Cil.CurrentLoc.get () in
+ Origin { kind; loc; id; }
+let well = Well
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 is_top 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 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 (Prototype)
let pretty_as_reason fmt org =
- if not (is_top org) then
- Format.fprintf fmt " because of %a" pretty 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
-
-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 *)
- 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))
+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
+let is_included = equal
(* Well and Unknown origins have no location information.
Leaf origins are also imprecise, because we may create tons of those,
that get reduced to precise values by the specifications of the function. *)
let is_precise = function
- | Well | Unknown | Leaf _ -> false
- | Misalign_read _ | Merge _ | Arith _ -> true
-
+ | Unknown | Well -> false
+ | Origin { kind } -> kind <> Leaf
(*
Local Variables:
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index 13af0bf55aaa849624b1e10a68d583cc6d7b6a48..572f9d586946995be6faf4ae7f92e72dd7d8a2c0 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/src/kernel_services/abstract_interp/origin.mli
@@ -28,43 +28,26 @@
ie. a numeric value that contains bits extracted from at least one
pointer, and that are not the result of a translation *)
-
-(** 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
-
-include Datatype.S with type t = origin
-
+include Datatype.S
type kind =
- | K_Misalign_read
- | K_Leaf
- | K_Merge
- | K_Arith
+ | Misalign_read
+ | Leaf
+ | Merge
+ | Arith
-val current: kind -> origin
+val current: kind -> t
(** This is automatically extracted from [Cil.CurrentLoc] *)
-val well: origin
-(** Creates a well origin. *)
+val well: t
+val top: t
+val is_top: t -> bool
val pretty_as_reason: Format.formatter -> t -> unit
(** Pretty-print [because of <origin>] if the origin is not {!Unknown}, or
nothing otherwise *)
-val top: t
-val is_top: t -> bool
-
-val bottom: t
-
val join: t -> t -> t
-val link: t -> t -> t
-val meet: t -> t -> t
-val narrow: t -> t -> t
-
val is_included: t -> t -> bool
val is_precise: t -> bool
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index 9cfa63a0dc9bdeb2a69c7f92614b36e039790f2f..fc5a2d67965fb489ed50e687ea75e65f15e56f80 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -596,7 +596,7 @@ let frama_c_memset state actuals =
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
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 96c9680ea4b2dab373d1c3ef0f45d8451e8ee2f8..efb382209ebc308a4db702b55202f52ddb07650f 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -129,7 +129,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..c669384d558d9e53f391d5d674a38ab006c03d04 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
@@ -36,7 +36,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/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 9354818cac31b53111b4fa4ed36dd05b396818c7..33c2b065e84e1ebeca1dd761494c51b4ad737116 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -568,7 +568,7 @@
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/float/oracle/nonlin.0.res.oracle b/tests/float/oracle/nonlin.0.res.oracle
index 3c25cbe9a7e7af49f5712d3551e3f897e2695832..3ba20ecccb33c4fff3665b5704762f6f99ecceee 100644
--- a/tests/float/oracle/nonlin.0.res.oracle
+++ b/tests/float/oracle/nonlin.0.res.oracle
@@ -244,7 +244,7 @@
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
+ The imprecision originates from Arithmetic {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -299,7 +299,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..abf87dfd56f40b0b5f15055984806be4a1dd9a8f 100644
--- a/tests/float/oracle/nonlin.1.res.oracle
+++ b/tests/float/oracle/nonlin.1.res.oracle
@@ -263,7 +263,7 @@
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
+ The imprecision originates from Arithmetic {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -326,7 +326,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..be3781ef63b137fbda4ff7983167a55a0c3506f4 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -246,7 +246,7 @@
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
+ The imprecision originates from Arithmetic {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -300,7 +300,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..9dc49e265e73612ccec64e417c29496e01c76608 100644
--- a/tests/float/oracle/nonlin.3.res.oracle
+++ b/tests/float/oracle/nonlin.3.res.oracle
@@ -244,7 +244,7 @@
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
+ The imprecision originates from Arithmetic {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -299,7 +299,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..84cee1a2044c5f85c0b3b24846705a722c95725c 100644
--- a/tests/float/oracle/nonlin.4.res.oracle
+++ b/tests/float/oracle/nonlin.4.res.oracle
@@ -263,7 +263,7 @@
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
+ The imprecision originates from Arithmetic {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -326,7 +326,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..00141d61eada6cb3661557df81f8703f1a17d6e1 100644
--- a/tests/float/oracle/nonlin.5.res.oracle
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -246,7 +246,7 @@
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
+ The imprecision originates from Arithmetic {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -300,7 +300,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/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index 59925bcb9eb92e8536134c8ff904f55dacb491f5..1b2258ac3dd8070c2a6b0238ec9b15a848fab49c 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -178,7 +178,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 +193,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/value/oracle/arith_pointer.res.oracle b/tests/value/oracle/arith_pointer.res.oracle
index 2397783f775ed506dd5127623508426785d8e2c2..c2b913baa6d38552337372466542bae6d0cdb9a9 100644
--- a/tests/value/oracle/arith_pointer.res.oracle
+++ b/tests/value/oracle/arith_pointer.res.oracle
@@ -150,11 +150,9 @@
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
diff --git a/tests/value/oracle/shift.0.res.oracle b/tests/value/oracle/shift.0.res.oracle
index bb1cdf0553127b21f9ad900a7b60b2580fc218de..562d983b174befd7c03e21242eff3454dc89f7eb 100644
--- a/tests/value/oracle/shift.0.res.oracle
+++ b/tests/value/oracle/shift.0.res.oracle
@@ -60,7 +60,7 @@
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
+ The imprecision originates from Arithmetic {shift.i:52}
[eva:alarm] shift.i:58: Warning:
unsigned overflow. assert 2U << 31 ≤ 4294967295;
[eva] Recording results for main
diff --git a/tests/value/oracle/shift.1.res.oracle b/tests/value/oracle/shift.1.res.oracle
index 601488698eb84a19f1a5ff51d8cd97c3ac787d0e..72a6309593ae7fc0b0ddc681de9f5b4444f2f062 100644
--- a/tests/value/oracle/shift.1.res.oracle
+++ b/tests/value/oracle/shift.1.res.oracle
@@ -52,7 +52,7 @@
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
+ The imprecision originates from Arithmetic {shift.i:52}
[eva] Recording results for main
[eva] Done for function main
[eva] shift.i:35: assertion 'Eva,shift' got final status invalid.
diff --git a/tests/value/oracle_bitwise/addition.res.oracle b/tests/value/oracle_bitwise/addition.res.oracle
index f65148d676c435df46dbec93bc4f3958019e7208..b130cd926c7d029c2913fb5d6517fc2730334c41 100644
--- a/tests/value/oracle_bitwise/addition.res.oracle
+++ b/tests/value/oracle_bitwise/addition.res.oracle
@@ -1,16 +1,6 @@
-123d122
-< The imprecision originates from Arithmetic {addition.i:52}
-162a162
+162a163
> {{ garbled mix of &{p1} (origin: Misaligned {addition.i:52}) }}
-163a164
+163a165
> {{ 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
+405a408
> {{ 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
index 370739039c6f31f1307fdab215ccdd958820f386..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/tests/value/oracle_bitwise/bitwise_pointer.0.res.oracle
+++ b/tests/value/oracle_bitwise/bitwise_pointer.0.res.oracle
@@ -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
index 370739039c6f31f1307fdab215ccdd958820f386..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/tests/value/oracle_bitwise/bitwise_pointer.1.res.oracle
+++ b/tests/value/oracle_bitwise/bitwise_pointer.1.res.oracle
@@ -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
index 60fe515050a5108521f39a3d59b01e51cb848735..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/tests/value/oracle_bitwise/logic_ptr_cast.res.oracle
+++ b/tests/value/oracle_bitwise/logic_ptr_cast.res.oracle
@@ -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..e379631a78c496c6d3d9a9d71dec00337be4c89b 100644
--- a/tests/value/oracle_equality/addition.res.oracle
+++ b/tests/value/oracle_equality/addition.res.oracle
@@ -3,10 +3,18 @@
< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
+144c140
+< The imprecision originates from Misaligned {addition.i:61}
+---
+> The imprecision originates from Misaligned {addition.i:59}
168c164
< [scope:rm_asserts] removing 9 assertion(s)
---
> [scope:rm_asserts] removing 7 assertion(s)
+190c186
+< p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
+---
+> p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
384,387d379
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
@@ -16,3 +24,7 @@
< [scope:rm_asserts] removing 9 assertion(s)
---
> [scope:rm_asserts] removing 7 assertion(s)
+433c425
+< p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
+---
+> p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
diff --git a/tests/value/oracle_equality/backward_add_ptr.res.oracle b/tests/value/oracle_equality/backward_add_ptr.res.oracle
index 3a6305e610f4b9491eff8fa269924571213a2b3b..0e1d24af5ce879ee4dedaebb2b79e8c9cb5c425c 100644
--- a/tests/value/oracle_equality/backward_add_ptr.res.oracle
+++ b/tests/value/oracle_equality/backward_add_ptr.res.oracle
@@ -16,65 +16,41 @@
> 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]
+145c151,154
< [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
+189a199,200
> {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:33}) }}
> {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:33}) }}
-200a210
+200a212
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:106}) }}
-202c212
+202c214
< {{ garbled mix of &{c} (origin: Arithmetic {backward_add_ptr.c:115}) }}
---
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:107}) }}
-203a214,216
+203a216,218
> {{ 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
+204a220,221
> {{ 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
+205a223
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:136}) }}
-206a223
+206a225
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:137}) }}
-207a225
+207a227
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:145}) }}
-208a227,230
+208a229,232
> {{ 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
+209a234,245
> {{ 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}) }}