diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index fb933d6a9ec59f05f1e0053a2635a198095286ac..43c783b2d54858680544ee538a36f4d8b63d72ac 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -94,6 +94,16 @@ let pretty_as_reason fmt org =
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"
+ | Leaf -> "assigns clause on addresses"
+ | Merge -> "imprecise merge of addresses"
+ | Arith -> "arithmetic operation on addresses"
+
let join t1 t2 =
if t1 == t2 then t1 else
match t1, t2 with
@@ -121,9 +131,10 @@ module History = State_builder.Hashtbl (Hashtbl) (History_Data) (History_Info)
let clear () = Id.reset (); History.clear ()
let register_write bases t =
- if not (is_unknown t) then
+ if is_unknown t then false else
let change (w, r, b) = w+1, r, Base.SetLattice.join b bases in
- ignore (History.memo ~change (fun _ -> 1, 0, bases) t)
+ let count, _, _ = History.memo ~change (fun _ -> 1, 0, bases) t in
+ count < 2 && is_current t
let register_read bases t =
if not (is_unknown t || is_current t) then
@@ -144,15 +155,9 @@ let pretty_origin fmt origin =
match origin with
| Unknown -> Format.fprintf fmt "Unknown origin"
| Well -> Format.fprintf fmt "Initial state"
- | Origin { kind; loc; } ->
- let kind =
- match kind with
- | Misalign_read -> "misaligned read of addresses"
- | Leaf -> "interpretation of assigns clause"
- | Merge -> "imprecise merge of addresses"
- | Arith -> "arithmetic operation on addresses"
- in
- Format.fprintf fmt "%a: %s" Cil_datatype.Location.pretty loc kind
+ | Origin { loc } ->
+ Format.fprintf fmt "%a: %s"
+ Cil_datatype.Location.pretty loc (descr origin)
let pretty_history fmt =
let list = get_history () in
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index 8aa75691e3705745cad49fc25fe57bfe4ac9bda9..5cf9f85698374cc848950d7abd8af4813e72fd49 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/src/kernel_services/abstract_interp/origin.mli
@@ -47,12 +47,17 @@ val pretty_as_reason: Format.formatter -> t -> unit
(** Pretty-print [because of <origin>] if the origin is not {!Unknown}, or
nothing otherwise *)
+val descr: t -> string
+
val join: t -> t -> t
val is_included: t -> t -> bool
(** Records the write of an imprecise value of the given bases,
- with the given origin. *)
-val register_write: Base.SetLattice.t -> t -> unit
+ 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 be emitted. *)
+val register_write: Base.SetLattice.t -> t -> bool
(** Records the read of an imprecise value of the given bases,
with the given origin. *)
diff --git a/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle b/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle
index 7cfe3e4ea5cf0dc4afe4fc3594f5fc056a737886..47e5fcec857fbf529aa684071565deb0082297fb 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:
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
index 3f979f64eee7dcf4b8b564eef4827775fde806ff..08f2e3d48be45da60c0ae9459b7afc2b39e005a6 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
@@ -36,47 +36,31 @@ let unbottomize = function
(* Garbled mix warnings *)
(* ---------------------------------------------------------------------- *)
-(* 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
- | Locations.Location_Bytes.Top (topparam, origin) ->
- Origin.register_write 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_unknown origin) then
- Format.fprintf fmt
- "@ @[The imprecision@ originates@ from@ %a@]"
- Origin.pretty org)
- origin
- Eva_utils.pp_callstack
- | Locations.Location_Bytes.Map _ -> ()
-
-let offsetmap_contains_imprecision offs =
- let exception Got_imprecise of Cvalue.V.t in
- 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_imprecise_value lval value =
+ match value with
+ | Locations.Location_Bytes.Top (bases, origin) ->
+ if Origin.register_write bases origin then
+ Self.warning ~wkey:Self.wkey_garbled_mix_write ~once:true ~current:true
+ "@[Assigning imprecise value to %a@ because of %s.@]%t"
+ Printer.pp_lval lval (Origin.descr origin)
+ Eva_utils.pp_callstack
+ | _ -> ()
+
+let warn_imprecise_location loc =
+ match loc.Locations.loc with
+ | Locations.Location_Bits.Top (Base.SetLattice.Top, orig) ->
+ Self.fatal ~current:true
+ "@[writing at a completely unknown address@ because of %s.@]@\nAborting."
+ (Origin.descr orig)
+ | _ -> ()
-let warn_right_imprecision lval loc offsetmap =
- match offsetmap_contains_imprecision offsetmap with
- | Some v -> warn_right_exp_imprecision lval loc v
- | None -> ()
+let warn_imprecise_write lval loc value =
+ warn_imprecise_location loc;
+ warn_imprecise_value lval value
+let warn_imprecise_offsm_write lval offsm =
+ let warn v = warn_imprecise_value lval (Cvalue.V_Or_Uninitialized.get_v v) in
+ Cvalue.V_Offsetmap.iter_on_values warn offsm
(* ---------------------------------------------------------------------- *)
(* Assumptions *)
@@ -136,26 +120,15 @@ 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_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
@@ -183,7 +156,7 @@ 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;
- warn_right_imprecision left_lval left_loc offsetmap;
+ warn_imprecise_offsm_write left_lval offsetmap;
`Value
(paste_offsetmap ~exact:true
~from:offsetmap ~dst_loc:left_loc.Locations.loc ~size state)
@@ -243,6 +216,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
diff --git a/src/plugins/eva/engine/transfer_specification.ml b/src/plugins/eva/engine/transfer_specification.ml
index 8f9c92b08ecbbdee659d82b99ae0d8e0eb8ea08f..eda7c02d067e4e93673eeda97269043ee84ae50f 100644
--- a/src/plugins/eva/engine/transfer_specification.ml
+++ b/src/plugins/eva/engine/transfer_specification.ml
@@ -314,12 +314,12 @@ module Make
begin
match cvalue with
| Top (bases, origin) ->
- Origin.register_write bases origin;
- 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)
+ 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)
| _ -> ()
end
in
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..d8fbec93f6a55d50d7bd4c804afc9b29b796c593 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,16 @@
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] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function sum:
ret ∈
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 c669384d558d9e53f391d5d674a38ab006c03d04..55f26985dfe052afb8beee70b695b23c87f304a6 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,8 +20,7 @@
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
diff --git a/tests/builtins/oracle/alloc.0.res.oracle b/tests/builtins/oracle/alloc.0.res.oracle
index 3ef4276dae84fa303cf368b3375377e8ac2e783b..7ce75e72f2118a378e84e5ca5e3a13f8e7e6ec51 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
diff --git a/tests/builtins/oracle/alloc.1.res.oracle b/tests/builtins/oracle/alloc.1.res.oracle
index d2683593c4b609727030a1db6ff6813ea4a0f654..7633c770d7101f16479f5b2848e9463500ce44eb 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;
diff --git a/tests/builtins/oracle/imprecise-malloc-free.res.oracle b/tests/builtins/oracle/imprecise-malloc-free.res.oracle
index 2d02014061a0fa9b8a3b45c488f4446d6f17f178..7134efd0323fd61d6cebbd58fa02929b0c856620 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.
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index bc169708e5bc2c84ecf6d7b2538ebbd7611b688d..ec7cb60e6e250de7e3d20234f69876cd67fd2b20 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
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 33c2b065e84e1ebeca1dd761494c51b4ad737116..eada478d3483b4a57cb4a6abb30025c87ef5e96b 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -100,6 +100,9 @@
[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:
@@ -107,6 +110,9 @@
[eva] memcpy.c:87: function memcpy: precondition 'separation' got status valid.
[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 +124,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.
diff --git a/tests/builtins/oracle/memset.res.oracle b/tests/builtins/oracle/memset.res.oracle
index a71515ecdbf65f033962389a94fb5e9028f811f4..5777e0557a9ffc796b54a09eb851df2b61f02dad 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.
diff --git a/tests/builtins/oracle/strchr.res.oracle b/tests/builtins/oracle/strchr.res.oracle
index e9cfcd8c7928de0aa61c8d1c8cf267de2e8dc1bd..ffbebfd90e0f629e11045f9b18f3ead6506ec7fd 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
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_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_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/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 3ba20ecccb33c4fff3665b5704762f6f99ecceee..04ffb0d077bb56f347f3db8d9e4dfaf8f22ff2d4 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 {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
diff --git a/tests/float/oracle/nonlin.1.res.oracle b/tests/float/oracle/nonlin.1.res.oracle
index abf87dfd56f40b0b5f15055984806be4a1dd9a8f..54cd152e82f21b5e75ea73f7a715a804f8a72f45 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 {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
diff --git a/tests/float/oracle/nonlin.2.res.oracle b/tests/float/oracle/nonlin.2.res.oracle
index be3781ef63b137fbda4ff7983167a55a0c3506f4..9ae60320eb162865fb9e2dfe8d15991d5b1056e9 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 {nonlin.c:98}
+ 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.
diff --git a/tests/float/oracle/nonlin.3.res.oracle b/tests/float/oracle/nonlin.3.res.oracle
index 9dc49e265e73612ccec64e417c29496e01c76608..17b03c98f92314bff3fe61bb303196e9eefb2872 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 {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
diff --git a/tests/float/oracle/nonlin.4.res.oracle b/tests/float/oracle/nonlin.4.res.oracle
index 84cee1a2044c5f85c0b3b24846705a722c95725c..33877fa4e0891cf6f0918b35f8dc656feda4c369 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 {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
diff --git a/tests/float/oracle/nonlin.5.res.oracle b/tests/float/oracle/nonlin.5.res.oracle
index 00141d61eada6cb3661557df81f8703f1a17d6e1..66c509fd9b8fef46e8dd64ddeadb67f0bf563877 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 {nonlin.c:98}
+ 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.
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/spawn_h.res.oracle b/tests/libc/oracle/spawn_h.res.oracle
index 01e765f74b0657f98adf4531504ffc36c9823a12..4b4c978087e9754cede4451980d1dae737d7f9d0 100644
--- a/tests/libc/oracle/spawn_h.res.oracle
+++ b/tests/libc/oracle/spawn_h.res.oracle
@@ -8,9 +8,6 @@
Called from spawn_h.c:36.
[eva] using specification for function getopt
[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 +145,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
diff --git a/tests/value/oracle/addition.res.oracle b/tests/value/oracle/addition.res.oracle
index cac259e96f2175dd68ab9ba81d78b1b0e2df7de3..1c7f73326fa47bb6b3b920c19f8baa452dde6daa 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,34 +107,31 @@
[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]
diff --git a/tests/value/oracle/arith_pointer.res.oracle b/tests/value/oracle/arith_pointer.res.oracle
index c2b913baa6d38552337372466542bae6d0cdb9a9..d8c8908c4b6586ae2f6baa6b01cca727b28032c3 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}) }}
@@ -117,8 +113,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 +124,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 +133,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}) }}
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/backward_add_ptr.res.oracle b/tests/value/oracle/backward_add_ptr.res.oracle
index d55109dbd308d126b923440c8325fa80ab08a693..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:
diff --git a/tests/value/oracle/behaviors1.res.oracle b/tests/value/oracle/behaviors1.res.oracle
index 980bd317335a3fc4d47b65acd11b2e391f2e1c3b..c434339fdecb7a85c1faef91c8aaa1b4215613e3 100644
--- a/tests/value/oracle/behaviors1.res.oracle
+++ b/tests/value/oracle/behaviors1.res.oracle
@@ -306,21 +306,9 @@
Called from behaviors1.i:473.
[eva] using specification for function f
[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] 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
diff --git a/tests/value/oracle/bitfield.res.oracle b/tests/value/oracle/bitfield.res.oracle
index 45acf78958063456e7bd3d636503dc555b6f337a..3b980d881cf63089d57219cca678788e03fa5090 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
@@ -115,9 +115,6 @@
.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}
[eva] bitfield.i:69: starting to merge loop iterations
[eva] computing for function leaf <- imprecise_bts_1671 <- main.
Called from bitfield.i:70.
diff --git a/tests/value/oracle/bitwise_pointer.0.res.oracle b/tests/value/oracle/bitwise_pointer.0.res.oracle
index c45fec9776b8c8ee44359a0cbb5211514ab29f2e..aa3a3f4a6a294519cff95e18f53878fc7c85bdc7 100644
--- a/tests/value/oracle/bitwise_pointer.0.res.oracle
+++ b/tests/value/oracle/bitwise_pointer.0.res.oracle
@@ -32,15 +32,13 @@
[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
diff --git a/tests/value/oracle/bitwise_pointer.1.res.oracle b/tests/value/oracle/bitwise_pointer.1.res.oracle
index c45fec9776b8c8ee44359a0cbb5211514ab29f2e..aa3a3f4a6a294519cff95e18f53878fc7c85bdc7 100644
--- a/tests/value/oracle/bitwise_pointer.1.res.oracle
+++ b/tests/value/oracle/bitwise_pointer.1.res.oracle
@@ -32,15 +32,13 @@
[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
diff --git a/tests/value/oracle/context_free.res.oracle b/tests/value/oracle/context_free.res.oracle
index ded8a88ce5e55edf2670cfc8359f746cb22b25e7..ffee5073affe361f3df6aa1b3baa894953b95853 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:
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..de456405cd98bad14e79ef22e9aa5c1c924883e3 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:
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..88263f19b58274baed0cb0b4ce28206a3abe4b8a 100644
--- a/tests/value/oracle/empty_struct.6.res.oracle
+++ b/tests/value/oracle/empty_struct.6.res.oracle
@@ -9,9 +9,6 @@
Called from empty_struct.c:99.
[eva] using specification for function f
[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
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/gauges.res.oracle b/tests/value/oracle/gauges.res.oracle
index 050ed73c53ad6db810ce0e3f0b9c795c17b33450..ce2c46bcca8652340104e25017c95045abc3dad6 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);
diff --git a/tests/value/oracle/imprecise_invalid_write.res.oracle b/tests/value/oracle/imprecise_invalid_write.res.oracle
index 3edbb6d07b05abbb8a627315a7e04d341fcd40ee..3b45112de2a37cad0bd4d80efe85f58d07634ff4 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:
diff --git a/tests/value/oracle/initialized.res.oracle b/tests/value/oracle/initialized.res.oracle
index d7b4af3ec6e4bc9398250cf52ce0acc4a026ff7e..1e822fd04fadadcd9e7fc2f60b1057b75e3cb553 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:
diff --git a/tests/value/oracle/label.res.oracle b/tests/value/oracle/label.res.oracle
index 7634f9cc0083b4c837f6a2435f8269b29c667ea5..6a5cb87b4b44d709668bdb9cbec106ab20f35a5d 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 ======
diff --git a/tests/value/oracle/leaf.res.oracle b/tests/value/oracle/leaf.res.oracle
index 7ccd5e0302a676eb3ee7293c6683d039208b0eca..d966184b444f1e6e55c2678426d0e103d88c926c 100644
--- a/tests/value/oracle/leaf.res.oracle
+++ b/tests/value/oracle/leaf.res.oracle
@@ -40,9 +40,6 @@
Called from leaf.i:50.
[eva] using specification for function f_int_star_int
[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}
@@ -50,9 +47,6 @@
Called from leaf.i:55.
[eva] using specification for function f_int_star_int_star_int
[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 }}
@@ -92,9 +86,6 @@
Called from leaf.i:68.
[eva] using specification for function f_st_star_cint_st_star_cint
[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
@@ -102,9 +93,6 @@
Called from leaf.i:69.
[eva] using specification for function f_st_star_int_st_star_int
[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
diff --git a/tests/value/oracle/leaf2.res.oracle b/tests/value/oracle/leaf2.res.oracle
index 3f486d154c0c0f64d200520942925f611f485b1d..5de89a4124f3730f3cb7fca1093681bd40c29c3a 100644
--- a/tests/value/oracle/leaf2.res.oracle
+++ b/tests/value/oracle/leaf2.res.oracle
@@ -15,14 +15,8 @@
Called from leaf2.i:6.
[eva] using specification for function f
[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] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/library.res.oracle b/tests/value/oracle/library.res.oracle
index 3a3a113d63804454659655d9caeb4b00194905de..01756f25fda5661297a36cda69ec139a857140c8 100644
--- a/tests/value/oracle/library.res.oracle
+++ b/tests/value/oracle/library.res.oracle
@@ -87,9 +87,6 @@
Called from library.i:31.
[eva] using specification for function f_star_int
[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);
@@ -113,9 +110,6 @@
Called from library.i:41.
[eva] using specification for function i
[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);
@@ -129,9 +123,6 @@
Called from library.i:45.
[eva] using specification for function k
[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
diff --git a/tests/value/oracle/logic.res.oracle b/tests/value/oracle/logic.res.oracle
index f88f05e9117129bb86b043b56223a54f5c3c6475..cc514176b48a155bf2b67d375b61cbad018df839 100644
--- a/tests/value/oracle/logic.res.oracle
+++ b/tests/value/oracle/logic.res.oracle
@@ -416,9 +416,6 @@
[eva] computing for function abs <- int_abs <- main.
Called from logic.c:411.
[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}) }}
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/origin.0.res.oracle b/tests/value/oracle/origin.0.res.oracle
index 21313b3be754e82c6d4c9570db9f1ae65208e409..463ecd82baa00bef9d69d4a929427c293e46f394 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
@@ -132,23 +129,18 @@
Called from origin.i:100.
[eva] using specification for function gp
[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}) }}
@@ -184,8 +176,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:
diff --git a/tests/value/oracle/origin.1.res.oracle b/tests/value/oracle/origin.1.res.oracle
index 2d7eae48a93c4432e4dac6e0f18275b4fdc43432..23f2017157dd55ca36d768e50a104ca4b1bff071 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,11 +70,8 @@
[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] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/period.res.oracle b/tests/value/oracle/period.res.oracle
index cca040e6158d8cb00ae2ab1bb22e787b08bec17a..bae921f2c83017e3d0a579fd5e57968d107db2cc 100644
--- a/tests/value/oracle/period.res.oracle
+++ b/tests/value/oracle/period.res.oracle
@@ -83,14 +83,12 @@
[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;
diff --git a/tests/value/oracle/reduce_by_valid.res.oracle b/tests/value/oracle/reduce_by_valid.res.oracle
index dcea93719575ad63fc979a58b76af32c6ed72407..f74f2e91178601fd3731ee7c6db79b7e5c836b99 100644
--- a/tests/value/oracle/reduce_by_valid.res.oracle
+++ b/tests/value/oracle/reduce_by_valid.res.oracle
@@ -146,9 +146,6 @@
Called from reduce_by_valid.i:272.
[eva] using specification for function garbled_mix
[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}
@@ -171,9 +168,6 @@
[eva] computing for function garbled_mix <- main12 <- main.
Called from reduce_by_valid.i:290.
[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
diff --git a/tests/value/oracle/shift.0.res.oracle b/tests/value/oracle/shift.0.res.oracle
index 562d983b174befd7c03e21242eff3454dc89f7eb..0303ded6de4929bc22a0eae3ef2230863830238f 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,9 +57,6 @@
[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 {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 72a6309593ae7fc0b0ddc681de9f5b4444f2f062..2caaba30888d19cb802a92693305b2cb39762f6a 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,9 +49,6 @@
[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 {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/sizeof.res.oracle b/tests/value/oracle/sizeof.res.oracle
index e9b64cb2ded5b0d9df7a1b6e5661cfc40e6f782e..9efb1b55c2d57c801e5e056dee0d78d42f817408 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;
diff --git a/tests/value/oracle/struct3.res.oracle b/tests/value/oracle/struct3.res.oracle
index 2ab398ecfda2225ff7f334606d192913e00d704a..795a309294796edcca100322d47c6aa0466208fb 100644
--- a/tests/value/oracle/struct3.res.oracle
+++ b/tests/value/oracle/struct3.res.oracle
@@ -24,8 +24,8 @@
[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] struct3.i:42: assertion 'Eva,index_bound' got final status invalid.
diff --git a/tests/value/oracle/va_list2.0.res.oracle b/tests/value/oracle/va_list2.0.res.oracle
index 619211814b41de75cdd428ff271735802110dfd5..49e0e8774567b880a14053405a6e14e7c690d7b5 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
diff --git a/tests/value/oracle_apron/backward_add_ptr.res.oracle b/tests/value/oracle_apron/backward_add_ptr.res.oracle
index bb1de4dbb864285a682d25c0502c0c4081b82f4c..ef19a912e467e231b3a3b3f3b80a52bb43737247 100644
--- a/tests/value/oracle_apron/backward_add_ptr.res.oracle
+++ b/tests/value/oracle_apron/backward_add_ptr.res.oracle
@@ -1,32 +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
-187c199
+154c166
< (propagated 20 times, read 86 times) garbled mix of bases {a; b; a; b; c}
---
> (propagated 28 times, read 90 times) garbled mix of bases {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..3829c4158e264ac75da7160ef40f37f47f4f8a8a 100644
--- a/tests/value/oracle_apron/gauges.res.oracle
+++ b/tests/value/oracle_apron/gauges.res.oracle
@@ -17,48 +17,48 @@
< [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]
-778c765
+774c761
< n ∈ [-2147483648..99]
---
> n ∈ [-2147483547..99]
-781c768
+777c764
< i ∈ [0..2147483647]
---
> i ∈ [10..2147483647]
-817c804
+813c800
< i ∈ [0..2147483647]
---
> i ∈ [0..21]
diff --git a/tests/value/oracle_equality/addition.res.oracle b/tests/value/oracle_equality/addition.res.oracle
index 03d182adfb81dd998ef8839447b2aa8c18b1e813..fe592057b7b43420c1d46e1bd52ac8c79a47bac6 100644
--- a/tests/value/oracle_equality/addition.res.oracle
+++ b/tests/value/oracle_equality/addition.res.oracle
@@ -1,38 +1,42 @@
-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;
-144c140
-< The imprecision originates from Misaligned {addition.i:61}
----
-> The imprecision originates from Misaligned {addition.i:59}
-154,157c150,151
+< [eva:garbled-mix:write] addition.i:61: Warning:
+< Assigning imprecise value to p14 because of misaligned read of addresses.
+144,146c138
< (propagated 1 times, read 1 times) garbled mix of bases {p1}
< addition.i:61: misaligned read of addresses
< (propagated 1 times, read 1 times) garbled mix of bases {p1}
+---
+> (propagated 2 times, read 2 times) garbled mix of bases {p1}
+167c159,161
< [scope:rm_asserts] removing 9 assertion(s)
---
> (propagated 2 times, read 2 times) garbled mix of bases {p1}
> [scope:rm_asserts] removing 7 assertion(s)
-179c173
+189c183
< p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
---
> p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
-373,376d366
+383,386d376
< [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;
-385,388c375,376
+395,397c385
< (propagated 1 times, read 1 times) garbled mix of bases {p1}
< addition.i:61: misaligned read of addresses
< (propagated 1 times, read 1 times) garbled mix of bases {p1}
+---
+> (propagated 2 times, read 2 times) garbled mix of bases {p1}
+418c406,408
< [scope:rm_asserts] removing 9 assertion(s)
---
> (propagated 2 times, read 2 times) garbled mix of bases {p1}
> [scope:rm_asserts] removing 7 assertion(s)
-411c399
+441c431
< 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 7c9150e449e866e7d5fb7b5e3aaec59dc29d1289..38834abac9b8f039c5f0b3972dcb5d0f4e393e21 100644
--- a/tests/value/oracle_equality/backward_add_ptr.res.oracle
+++ b/tests/value/oracle_equality/backward_add_ptr.res.oracle
@@ -2,28 +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
-145c151,154
+118c124,127
< [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
-187c196
+154c163
< (propagated 20 times, read 86 times) garbled mix of bases {a; b; a; b; c}
---
> (propagated 26 times, read 94 times) garbled mix of bases {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..46eace6fb725925449aeaf5c01f6ed18b2bd7a09 100644
--- a/tests/value/oracle_equality/bitfield.res.oracle
+++ b/tests/value/oracle_equality/bitfield.res.oracle
@@ -1,4 +1,4 @@
-137a138,140
+134a135,137
> [eva] bitfield.i:71:
> Frama_C_show_each:
> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
diff --git a/tests/value/oracle_equality/bitwise_pointer.0.res.oracle b/tests/value/oracle_equality/bitwise_pointer.0.res.oracle
index f04f7077977a5a61ea7d346c6ff6f90a2e4237e4..0b286b812681ed3e8f9d9d2f5b2797ec78fa9df4 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
+60c60
< x ∈ [0..9]
---
> x ∈ {5}
-75c75
+73c73
< 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..0b286b812681ed3e8f9d9d2f5b2797ec78fa9df4 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
+60c60
< x ∈ [0..9]
---
> x ∈ {5}
-75c75
+73c73
< x1 ∈ [0..9]
---
> x1 ∈ {5}
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/library.res.oracle b/tests/value/oracle_equality/library.res.oracle
index 60b76d8270d110e07713fc18e2042192a380e59e..7ce2a4b0636c541b94a46f6ac3100e7660b079b8 100644
--- a/tests/value/oracle_equality/library.res.oracle
+++ b/tests/value/oracle_equality/library.res.oracle
@@ -1,4 +1,4 @@
-124,127d123
+118,121d117
< [eva:alarm] library.i:44: Warning:
< non-finite float value. assert \is_finite(*pf);
< [eva:alarm] library.i:44: Warning:
diff --git a/tests/value/oracle_equality/origin.0.res.oracle b/tests/value/oracle_equality/origin.0.res.oracle
index fca55cdcd1617b76c6bd48031be44f3befefd3c2..abe35687d18afa5ad7b79629a2d8594868b20ce1 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
+229,230c229
< 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
+264,265c263
< 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..72c7991e2b3468da18583defce107fc497b4bb5a 100644
--- a/tests/value/oracle_equality/period.res.oracle
+++ b/tests/value/oracle_equality/period.res.oracle
@@ -1,9 +1,8 @@
-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
+97d91
< [scope:rm_asserts] removing 1 assertion(s)
diff --git a/tests/value/oracle_gauges/bitfield.res.oracle b/tests/value/oracle_gauges/bitfield.res.oracle
index e0125a5db691f59d2cacd6f04887d761975891e2..c47829e652e4b743152bbfca46d27650bab2fc3e 100644
--- a/tests/value/oracle_gauges/bitfield.res.oracle
+++ b/tests/value/oracle_gauges/bitfield.res.oracle
@@ -1,4 +1,4 @@
-137a138,152
+134a135,149
> [eva] bitfield.i:71:
> Frama_C_show_each:
> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
diff --git a/tests/value/oracle_gauges/gauges.res.oracle b/tests/value/oracle_gauges/gauges.res.oracle
index 89bba971700e381aecb42f0a87e0010a27a5a7d7..1c645040cca978977f74a4d24ffac408484a6416 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,51 +258,51 @@
> 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
-765,766c885,886
+761,762c881,882
< A ∈ {{ &A + [0..--],0%4 }}
< B ∈ {{ &B + [0..--],0%4 }}
---
> A ∈ {{ &A + [0..36],0%4 }}
> B ∈ {{ &B + [0..36],0%4 }}
-778c898
+774c894
< n ∈ [-2147483648..99]
---
> n ∈ [-2147483547..99]
-784c904
+780c900
< i ∈ {45; 46; 47; 48; 49; 50; 51}
---
> i ∈ {45; 46; 47; 48}
-790c910
+786c906
< i ∈ {-59; -58; -57; -56; -55; -54; -53}
---
> i ∈ {-58; -57; -56; -55; -54; -53}
-810c930
+806c926
< p ∈ {{ &u + [0..--],0%4 }}
---
> p ∈ {{ &u + [0..400],0%4 }}
-812c932
+808c928
< k ∈ [0..2147483647]
---
> k ∈ [0..390]
-817c937
+813c933
< i ∈ [0..2147483647]
---
> i ∈ [0..21]
-828,829c948,950
+824,825c944,946
< [1..9] ∈ {4; 5; 6; 7; 8; 9} or UNINITIALIZED
< p ∈ {{ &y + [4..40],0%4 }}
---
> [1..6] ∈ {4; 5; 6; 7; 8; 9} or UNINITIALIZED
> [7..9] ∈ UNINITIALIZED
> p ∈ {{ &y[7] }}
-840c961
+836c957
< p ∈ {{ &T + [--..396],0%4 }}
---
> p ∈ {{ &T + [-4..396],0%4 }}
-845,849c966
+841,845c962
< n ∈ {0}
< arr[0] ∈ {0}
< [1] ∈ {-1}
@@ -310,19 +310,19 @@
< p ∈ {{ &arr + [12..--],0%4 }}
---
> NON TERMINATING FUNCTION
-952a1070
+948a1066
> [from] Non-terminating function main8_aux (no dependencies)
-975,976c1093,1094
+971,972c1089,1090
< p FROM p; A; B; n; p; A[0..9]; B[0..9] (and SELF)
< \result FROM p; A; B; n; p; A[0..9]; B[0..9]
---
> p FROM p; A; B; n; p; A[0..8]; B[0..8] (and SELF)
> \result FROM p; A; B; n; p; A[0..8]; B[0..8]
-1020c1138
+1016c1134
< NO EFFECTS
---
> NON TERMINATING - NO EFFECTS
-1054c1172
+1050c1168
< p; A[0..9]; B[0..9]
---
> p; A[0..8]; B[0..8]
diff --git a/tests/value/oracle_gauges/va_list2.0.res.oracle b/tests/value/oracle_gauges/va_list2.0.res.oracle
index 028514ddc800f41a22034f68671bf0c604ea9734..80fc106a63e0bc09c6ccf89c3f85ddb2cca12acd 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) }}
diff --git a/tests/value/oracle_octagon/bitfield.res.oracle b/tests/value/oracle_octagon/bitfield.res.oracle
index 9886a5a3b66d5f82e84afc4a5a3b268b67994a12..46eace6fb725925449aeaf5c01f6ed18b2bd7a09 100644
--- a/tests/value/oracle_octagon/bitfield.res.oracle
+++ b/tests/value/oracle_octagon/bitfield.res.oracle
@@ -1,4 +1,4 @@
-137a138,140
+134a135,137
> [eva] bitfield.i:71:
> Frama_C_show_each:
> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
diff --git a/tests/value/oracle_octagon/gauges.res.oracle b/tests/value/oracle_octagon/gauges.res.oracle
index a5e47e28258fe4726d31ff83cb80079321750697..5b5cc28292675e05f4c652053a6c451c8d8744d1 100644
--- a/tests/value/oracle_octagon/gauges.res.oracle
+++ b/tests/value/oracle_octagon/gauges.res.oracle
@@ -1,17 +1,17 @@
-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:
< [eva:alarm] gauges.c:220: Warning:
< signed overflow. assert -2147483648 ≤ n - 1;
-767c760
+763c756
< numNonZero ∈ [-2147483648..8]
---
> numNonZero ∈ {-1}
-778c771
+774c767
< n ∈ [-2147483648..99]
---
> n ∈ {-1}
diff --git a/tests/value/oracle_symblocs/bitwise_pointer.0.res.oracle b/tests/value/oracle_symblocs/bitwise_pointer.0.res.oracle
index f04f7077977a5a61ea7d346c6ff6f90a2e4237e4..0b286b812681ed3e8f9d9d2f5b2797ec78fa9df4 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
+60c60
< x ∈ [0..9]
---
> x ∈ {5}
-75c75
+73c73
< 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..0b286b812681ed3e8f9d9d2f5b2797ec78fa9df4 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
+60c60
< x ∈ [0..9]
---
> x ∈ {5}
-75c75
+73c73
< x1 ∈ [0..9]
---
> x1 ∈ {5}
diff --git a/tests/value/oracle_symblocs/library.res.oracle b/tests/value/oracle_symblocs/library.res.oracle
index 60b76d8270d110e07713fc18e2042192a380e59e..7ce2a4b0636c541b94a46f6ac3100e7660b079b8 100644
--- a/tests/value/oracle_symblocs/library.res.oracle
+++ b/tests/value/oracle_symblocs/library.res.oracle
@@ -1,4 +1,4 @@
-124,127d123
+118,121d117
< [eva:alarm] library.i:44: Warning:
< non-finite float value. assert \is_finite(*pf);
< [eva:alarm] library.i:44: Warning: