diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 8d37feb25148d6698b36cb3a35f10a51a3d1da9c..e09243ea9c2a696788354c95601053fd8a269e08 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -187,7 +187,7 @@ struct
let offm' =
match size with
| Int_Base.Top ->
- let orig = Origin.current Origin.Arith in
+ let orig = Origin.current Origin.Misalign_write in
Offsetmap.update_imprecise_everywhere ~validity orig v offm
| Int_Base.Value size ->
assert (Int.ge size Int.zero);
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 2585c74c98c1599bb6c55475e6cd695b76ca1ffd..08fa4d98a93a955bd17f37776e332b8e9bca9a84 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -1849,7 +1849,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let origin =
match origin with
| Some origin -> origin
- | None -> Origin.(current Misalign_read)
+ | None -> Origin.(current Misalign_write)
in
let v = V.topify_with_origin origin v in
(* TODO: check *)
@@ -1872,7 +1872,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let v =
if Int.is_zero (period %~ size) then v
else
- let origin = Origin.(current Misalign_read) in
+ let origin = Origin.(current Misalign_write) in
let v' = V.topify_with_origin origin v in
if not (V.equal v v') then
Lattice_messages.emit_approximation msg_emitter
@@ -2803,14 +2803,14 @@ module Make_bitwise(V: sig
in
`Value (Int_Intervals.fold aux_itv itvs m)
with Error_Top ->
- update_imprecise_everywhere ~validity Origin.unknown v m
+ update_imprecise_everywhere ~validity Origin.(current Misalign_write) v m
let add_binding_ival ~validity ~exact offsets ~size v m =
match size with
| Int_Base.Value size ->
update ~validity ~exact ~offsets ~size v m
| Int_Base.Top ->
- update_imprecise_everywhere ~validity Origin.unknown v m
+ update_imprecise_everywhere ~validity Origin.(current Misalign_write) v m
let fold_itv ?direction ~entire f itv m acc =
let f' itv (v, _, _) acc = f itv v acc in
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index c1520c9d3baaac926b2c658815c19c86866c3729..422fc364d378f93c2cfa452560972958ea929cd2 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -22,18 +22,21 @@
type kind =
| Misalign_read
+ | Misalign_write
| Leaf
| Merge
| Arith
let kind_rank = function
| Misalign_read -> 0
- | Leaf -> 1
- | Merge -> 2
- | Arith -> 3
+ | Misalign_write -> 1
+ | Leaf -> 2
+ | Merge -> 3
+ | Arith -> 4
let kind_label = function
- | Misalign_read -> "Misaligned"
+ | Misalign_read -> "Misaligned read"
+ | Misalign_write -> "Misaligned write"
| Leaf -> "Library function"
| Merge -> "Merge"
| Arith -> "Arithmetic"
@@ -102,6 +105,7 @@ let descr = function
| Origin { kind } ->
match kind with
| Misalign_read -> "misaligned read of addresses"
+ | Misalign_write -> "misaligned write of addresses"
| Leaf -> "assigns clause on addresses"
| Merge -> "imprecise merge of addresses"
| Arith -> "arithmetic operation on addresses"
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index 506c020b29df8a5c42bcb7ca7e8a780c285c0be4..a5d1ce6566cad15266083eafe041f6de6f5bf328 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/src/kernel_services/abstract_interp/origin.mli
@@ -28,6 +28,7 @@ include Datatype.S
type kind =
| Misalign_read (* Misaligned read of addresses *)
+ | Misalign_write (* Misaligned write of addresses *)
| Leaf (* Interpretation of assigns clause *)
| Merge (* Imprecise merge of addresses *)
| Arith (* Arithmetic operation on addresses *)
diff --git a/tests/builtins/oracle/alloc.1.res.oracle b/tests/builtins/oracle/alloc.1.res.oracle
index 77bfca7bbb74e166fbde9bb07f945257115aeb0c..3ce9953a7b83089a4d07f17bbecd883f451dca85 100644
--- a/tests/builtins/oracle/alloc.1.res.oracle
+++ b/tests/builtins/oracle/alloc.1.res.oracle
@@ -39,7 +39,7 @@
[eva:final-states] Values at end of function main_abs:
NULL[rbits 2048 to 4103] ∈
{{ garbled mix of &{__malloc_main_abs_l50}
- (origin: Misaligned {alloc.c:54}) }}
+ (origin: Misaligned write {alloc.c:54}) }}
__fc_heap_status ∈ [--..--]
q ∈ {{ &__malloc_main_abs_l50 }}
r ∈ {{ NULL + [256..509] ; &__malloc_main_abs_l50 }}
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index 1ad813d673e5c5dc6276df115ec2a8b78663aed0..d5857d6a3780f56d151fe939579bfa1bfc81ef4d 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -273,7 +273,7 @@
p ∈ {{ &x }}
c1 ∈ {{ (char)&x }}
c2# ∈ {{ (? *)&x }}%32, bits 0 to 7
- c3 ∈ {{ garbled mix of &{x} (origin: Misaligned {imprecise.c:68}) }}
+ c3 ∈ {{ garbled mix of &{x} (origin: Misaligned read {imprecise.c:68}) }}
[eva:final-states] Values at end of function garbled_mix_null:
NULL[rbits 800 to 1607] ∈ [--..--] or ESCAPINGADDR
p_gm_null ∈ [100..197]
@@ -317,11 +317,12 @@
vy ∈ {1} or UNINITIALIZED
[eva:final-states] Values at end of function write_garbled:
NULL[rbits 800 to 1607] ∈
- {{ garbled mix of &{j; k} (origin: Misaligned {imprecise.c:22}) }}
+ {{ garbled mix of &{j; k}
+ (origin: Misaligned write {imprecise.c:22}) }}
i ∈ {1}
j ∈ {{ NULL + [1..197] ; (int)&j ; &k + [0..16] }}
k[0..4] ∈
- {{ garbled mix of &{j; k} (origin: Misaligned {imprecise.c:22}) }}
+ {{ garbled mix of &{j; k} (origin: Misaligned write {imprecise.c:22}) }}
p ∈ {{ NULL + [100..197] ; &j ; &k + [0..16] }}
[eva:final-states] Values at end of function main:
NULL[rbits 800 to 1607] ∈ [--..--] or ESCAPINGADDR
@@ -820,7 +821,7 @@
p ∈ {{ &x }}
c1 ∈ {{ (char)&x }}
c2# ∈ {{ (? *)&x }}%32, bits 0 to 7
- c3 ∈ {{ garbled mix of &{x} (origin: Misaligned {imprecise.c:68}) }}
+ c3 ∈ {{ garbled mix of &{x} (origin: Misaligned read {imprecise.c:68}) }}
[eva:final-states] Values at end of function garbled_mix_null:
NULL[rbits 800 to 1607] ∈ [--..--] or ESCAPINGADDR
p_gm_null ∈ [100..197]
@@ -861,11 +862,12 @@
vy ∈ {1} or UNINITIALIZED
[eva:final-states] Values at end of function write_garbled:
NULL[rbits 800 to 1607] ∈
- {{ garbled mix of &{j; k} (origin: Misaligned {imprecise.c:22}) }}
+ {{ garbled mix of &{j; k}
+ (origin: Misaligned write {imprecise.c:22}) }}
i ∈ {1}
j ∈ {{ NULL + [1..197] ; (int)&j ; &k + [0..16] }}
k[0..4] ∈
- {{ garbled mix of &{j; k} (origin: Misaligned {imprecise.c:22}) }}
+ {{ garbled mix of &{j; k} (origin: Misaligned write {imprecise.c:22}) }}
p ∈ {{ NULL + [100..197] ; &j ; &k + [0..16] }}
[eva:final-states] Values at end of function main:
NULL[rbits 800 to 1607] ∈ [--..--] or ESCAPINGADDR
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 47fb30443a6614c1dabe8e0aada9ca7fb56d4183..6fe4eedb72486a27ebdc2582a036bea66c8573cd 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -576,7 +576,7 @@
v2.x ∈ {5}
.y ∈ {7}
{.p; .padding[0..23]} ∈ {0}
- v3 ∈ {{ garbled mix of &{v1} (origin: Misaligned {memcpy.c:87}) }}
+ v3 ∈ {{ garbled mix of &{v1} (origin: Misaligned read {memcpy.c:87}) }}
v4.x ∈ [--..--]
.y ∈ {{ (int)&t }}
{.p; .padding[0..23]} ∈ [--..--]
diff --git a/tests/builtins/oracle/memset.res.oracle b/tests/builtins/oracle/memset.res.oracle
index d5217c400ffa1354b17d7e7da04b7d37f3f7ff11..a6115d361b6b54206f7f038fd794ce01df915472 100644
--- a/tests/builtins/oracle/memset.res.oracle
+++ b/tests/builtins/oracle/memset.res.oracle
@@ -113,7 +113,8 @@
t3[0..9] ∈ {0}
[10..99]# ∈ {0; 17} repeated %8
t4[0..99] ∈ {0}
- t5[0..99] ∈ {{ garbled mix of &{t1} (origin: Misaligned {memset.c:41}) }}
+ t5[0..99] ∈
+ {{ garbled mix of &{t1} (origin: Misaligned read {memset.c:41}) }}
t6[0..9] ∈ {0}
[10..13]# ∈ {0; 34} repeated %8
[14..99] ∈ {0}
@@ -168,7 +169,8 @@
t3[0..9] ∈ {0}
[10..99]# ∈ {0; 17} repeated %8
t4[0..99] ∈ {0}
- t5[0..99] ∈ {{ garbled mix of &{t1} (origin: Misaligned {memset.c:41}) }}
+ t5[0..99] ∈
+ {{ garbled mix of &{t1} (origin: Misaligned read {memset.c:41}) }}
t6[0..9] ∈ {0}
[10..13]# ∈ {0; 34} repeated %8
[14..99] ∈ {0}
diff --git a/tests/value/oracle/addition.res.oracle b/tests/value/oracle/addition.res.oracle
index 1c7f73326fa47bb6b3b920c19f8baa452dde6daa..394936b8b9df05a61b4935cb721c0e66380efa36 100644
--- a/tests/value/oracle/addition.res.oracle
+++ b/tests/value/oracle/addition.res.oracle
@@ -159,8 +159,10 @@
p10 ∈ {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}
p11 ∈ [-2147483648..0],0%4
p12 ∈ {{ garbled mix of &{p1; p2} (origin: Arithmetic {addition.i:56}) }}
- p13 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
- p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
+ p13 ∈
+ {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
+ p14 ∈
+ {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
p15 ∈ {-1}
p16 ∈ {2949122}
p17 ∈ {-2147483648; 0}
@@ -385,8 +387,10 @@
p10 ∈ {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}
p11 ∈ [-2147483648..0],0%4
p12 ∈ {{ garbled mix of &{p1; p2} (origin: Arithmetic {addition.i:56}) }}
- p13 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
- p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
+ p13 ∈
+ {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
+ p14 ∈
+ {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
p15 ∈ {-1}
p16 ∈ {2; 2949122; 3014658}
p17 ∈ {-2147483648; 0}
diff --git a/tests/value/oracle/assigns_from.res.oracle b/tests/value/oracle/assigns_from.res.oracle
index 55b41ae8a07167bd77b0ccba4956bae60544cb17..be60cecebede8380f7df749aecdd254fe0bcc968 100644
--- a/tests/value/oracle/assigns_from.res.oracle
+++ b/tests/value/oracle/assigns_from.res.oracle
@@ -373,17 +373,17 @@
base_a ∈ {17}
a_0.addr ∈
{{ garbled mix of &{base_a; base_b}
- (origin: Misaligned {assigns_from.i:215}) }}
+ (origin: Misaligned read {assigns_from.i:215}) }}
.i ∈
{{ garbled mix of &{base_a; base_b}
- (origin: Misaligned {assigns_from.i:215}) }} or UNINITIALIZED
+ (origin: Misaligned read {assigns_from.i:215}) }} or UNINITIALIZED
base_b ∈ {11}
b.addr ∈
{{ garbled mix of &{base_a; base_b}
- (origin: Misaligned {assigns_from.i:215}) }}
+ (origin: Misaligned read {assigns_from.i:215}) }}
.i ∈
{{ garbled mix of &{base_a; base_b}
- (origin: Misaligned {assigns_from.i:215}) }} or UNINITIALIZED
+ (origin: Misaligned read {assigns_from.i:215}) }} or UNINITIALIZED
[eva:final-states] Values at end of function main2:
a[0..2] ∈ {0}
[3] ∈ {2}
diff --git a/tests/value/oracle/bitfield.res.oracle b/tests/value/oracle/bitfield.res.oracle
index 3751001cbba46ff03930675e67332c3686863ee2..cae0f2d2936a0ef67c6846b8e569f6073fa67bb2 100644
--- a/tests/value/oracle/bitfield.res.oracle
+++ b/tests/value/oracle/bitfield.res.oracle
@@ -111,25 +111,25 @@
[eva] Done for function leaf
[eva] bitfield.i:71:
Frama_C_show_each:
- {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
[eva] bitfield.i:73:
Frama_C_show_each:
- .next ∈ {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ .next ∈ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
.bitf ∈ {0}
.[bits 65 to 95] ∈
- {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
[eva] bitfield.i:69: starting to merge loop iterations
[eva] computing for function leaf <- imprecise_bts_1671 <- main.
Called from bitfield.i:70.
[eva] Done for function leaf
[eva] bitfield.i:71:
Frama_C_show_each:
- {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
[eva:alarm] bitfield.i:72: Warning:
out of bounds write. assert \valid(&c->bitf);
[eva] bitfield.i:73:
Frama_C_show_each:
- {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
[eva:alarm] bitfield.i:74: Warning:
out of bounds read. assert \valid_read(&c->next.next);
[eva] computing for function leaf <- imprecise_bts_1671 <- main.
@@ -187,8 +187,8 @@
G ∈ {1}
H ∈ {0}
b ∈ {0}
- c ∈ {{ garbled mix of &{b; ee} (origin: Misaligned {bitfield.i:70}) }}
- ee ∈ {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ c ∈ {{ garbled mix of &{b; ee} (origin: Misaligned read {bitfield.i:70}) }}
+ ee ∈ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
foo ∈ [--..--]
y.v0_3 ∈ [--..--]
.v4 ∈ {0}
@@ -229,8 +229,9 @@
r ∈ {1}
[eva:final-states] Values at end of function imprecise_bts_1671:
b ∈ {0}
- c ∈ {{ garbled mix of &{b; ee} (origin: Misaligned {bitfield.i:70}) }}
- ee ∈ {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ c ∈
+ {{ garbled mix of &{b; ee} (origin: Misaligned read {bitfield.i:70}) }}
+ ee ∈ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
[eva:final-states] Values at end of function logic:
y.v0_3 ∈ [--..--]
.v4 ∈ {0}
@@ -280,8 +281,9 @@
G ∈ {1}
H ∈ {0}
b ∈ {0}
- c ∈ {{ garbled mix of &{b; ee} (origin: Misaligned {bitfield.i:70}) }}
- ee ∈ {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+ c ∈
+ {{ garbled mix of &{b; ee} (origin: Misaligned read {bitfield.i:70}) }}
+ ee ∈ {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
y.v0_3 ∈ [--..--]
.v4 ∈ {0}
.v5_31 ∈ [--..--]
diff --git a/tests/value/oracle/label.res.oracle b/tests/value/oracle/label.res.oracle
index 6a5cb87b4b44d709668bdb9cbec106ab20f35a5d..4b44fa1adfa728e27f6f9d97a39125ec045b12c2 100644
--- a/tests/value/oracle/label.res.oracle
+++ b/tests/value/oracle/label.res.oracle
@@ -22,7 +22,7 @@
a ∈ {{ &d + {4} }}
b ∈ {1; 2}
i ∈ {4}
- p ∈ {{ garbled mix of &{a; b} (origin: Misaligned {label.i:18}) }}
+ p ∈ {{ garbled mix of &{a; b} (origin: Misaligned read {label.i:18}) }}
q ∈ {{ &a }}
[from] Computing for function main
[from] Done for function main
diff --git a/tests/value/oracle/not_ct_array_arg.res.oracle b/tests/value/oracle/not_ct_array_arg.res.oracle
index bc4b35bcb5822c058be586eea8fc6709cfdad55d..560745bc9b332a6c91f73d247be11f3fdde05bd8 100644
--- a/tests/value/oracle/not_ct_array_arg.res.oracle
+++ b/tests/value/oracle/not_ct_array_arg.res.oracle
@@ -35,10 +35,11 @@
tc ∈ {{ NULL ; &S_tc[0] }}
S_tc[0..1][0..9] ∈ [--..--]
S_tb[bits 0 to 31] ∈
- {{ garbled mix of &{tb} (origin: Misaligned {not_ct_array_arg.i:12}) }}
+ {{ garbled mix of &{tb}
+ (origin: Misaligned write {not_ct_array_arg.i:12}) }}
[bits 32 to ..] ∈
{{ garbled mix of &{tb}
- (origin: Misaligned {not_ct_array_arg.i:12}) }} or UNINITIALIZED
+ (origin: Misaligned write {not_ct_array_arg.i:12}) }} or UNINITIALIZED
==END OF DUMP==
[eva:alarm] not_ct_array_arg.i:14: Warning:
out of bounds write. assert \valid(&(*(tc + 1))[1]);
@@ -56,10 +57,11 @@
[1][1] ∈ {3}
[1][2..9] ∈ [--..--]
S_tb[bits 0 to 31] ∈
- {{ garbled mix of &{tb} (origin: Misaligned {not_ct_array_arg.i:12}) }}
+ {{ garbled mix of &{tb}
+ (origin: Misaligned write {not_ct_array_arg.i:12}) }}
[bits 32 to ..] ∈
{{ garbled mix of &{tb}
- (origin: Misaligned {not_ct_array_arg.i:12}) }} or UNINITIALIZED
+ (origin: Misaligned write {not_ct_array_arg.i:12}) }} or UNINITIALIZED
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/value/oracle/origin.0.res.oracle b/tests/value/oracle/origin.0.res.oracle
index a0c837faa9e45d2e9593b57280248b8b6eab5d90..e93befd14488bc1553a17bdd7359fd79315a146c 100644
--- a/tests/value/oracle/origin.0.res.oracle
+++ b/tests/value/oracle/origin.0.res.oracle
@@ -146,7 +146,7 @@
Assigning imprecise value to qm2 because of misaligned read of addresses.
[eva] origin.i:55:
Frama_C_show_each:
- {{ garbled mix of &{a; b} (origin: Misaligned {origin.i:54}) }}
+ {{ garbled mix of &{a; b} (origin: Misaligned read {origin.i:54}) }}
[eva:alarm] origin.i:56: Warning: out of bounds write. assert \valid(qm2);
[eva:alarm] origin.i:56: Warning:
pointer downcast. assert (unsigned int)(&a) ≤ 2147483647;
@@ -228,9 +228,9 @@
pa2 ∈ {{ garbled mix of &{ta2} (origin: Arithmetic {origin.i:19}) }}
qa2 ∈ {{ &ta2 + [0..36] ; &tta2 + [0..36] }}
ta2[0..9] ∈
- {{ garbled mix of &{aa2} (origin: Misaligned {origin.i:21}) }}
+ {{ garbled mix of &{aa2} (origin: Misaligned write {origin.i:21}) }}
tta2[0..9] ∈
- {{ garbled mix of &{aa2} (origin: Misaligned {origin.i:21}) }}
+ {{ garbled mix of &{aa2} (origin: Misaligned write {origin.i:21}) }}
[eva:final-states] Values at end of function origin_arithmetic_3:
pa3 ∈ {{ &ta3 + [0..36] }}
ta3[0..9] ∈ [--..--]
@@ -269,10 +269,10 @@
{{ garbled mix of &{b} (origin: Merge {origin.i:106}) }}
ta1[0..9] ∈ {0}
ta2[0..9] ∈
- {{ garbled mix of &{aa2} (origin: Misaligned {origin.i:21}) }}
+ {{ garbled mix of &{aa2} (origin: Misaligned write {origin.i:21}) }}
ta3[0..9] ∈ [--..--]
tta2[0..9] ∈
- {{ garbled mix of &{aa2} (origin: Misaligned {origin.i:21}) }}
+ {{ garbled mix of &{aa2} (origin: Misaligned write {origin.i:21}) }}
l1 ∈ [--..--]
l2 ∈ [--..--]
l3 ∈ [--..--]
diff --git a/tests/value/oracle/origin.1.res.oracle b/tests/value/oracle/origin.1.res.oracle
index 4ca39e2f9666e88e958c97026512fbabd8a99cb5..f9c473570c4ed0ed91b4da38d351db512e6bfbf2 100644
--- a/tests/value/oracle/origin.1.res.oracle
+++ b/tests/value/oracle/origin.1.res.oracle
@@ -83,7 +83,7 @@
r.c ∈ [--..--]
.[bits 8 to 15] ∈ UNINITIALIZED
.i ∈ [--..--]
- .p ∈ {{ garbled mix of &{x} (origin: Misaligned {origin.i:126}) }}
+ .p ∈ {{ garbled mix of &{x} (origin: Misaligned read {origin.i:126}) }}
.t[0][bits 0 to 7] ∈
{{ garbled mix of &{y} (origin: Merge {origin.i:129}) }}
.t[0][bits 8 to 15]# ∈ {{ NULL ; (? *)&y }}%32, bits 24 to 31
diff --git a/tests/value/oracle/period.res.oracle b/tests/value/oracle/period.res.oracle
index e949e737f124893354288c4ed3865a65d6396b74..3f7cc6e99f50ff733afed56c83c82de26a529a36 100644
--- a/tests/value/oracle/period.res.oracle
+++ b/tests/value/oracle/period.res.oracle
@@ -103,7 +103,8 @@
[scope:rm_asserts] removing 1 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
- g[0..9] ∈ {{ garbled mix of &{vg} (origin: Misaligned {period.c:55}) }}
+ g[0..9] ∈
+ {{ garbled mix of &{vg} (origin: Misaligned write {period.c:55}) }}
Frama_C_periodic_t_320[0] ∈ {1}
[1..3] ∈ {0}
[4] ∈ {24}
diff --git a/tests/value/oracle_equality/addition.res.oracle b/tests/value/oracle_equality/addition.res.oracle
index 4527d4b279a58e63549f59ca9aef3f2765335771..5a0da48b045e46f9201b4058cfc0010bef15e6cc 100644
--- a/tests/value/oracle_equality/addition.res.oracle
+++ b/tests/value/oracle_equality/addition.res.oracle
@@ -13,16 +13,16 @@
> addition.i:59: misaligned read of addresses
> (read 1 times, propagated 2 times) garbled mix of &{p1}
> [scope:rm_asserts] removing 7 assertion(s)
-163c161
-< p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
+165c163
+< {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
---
-> p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
-357,360d354
+> {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
+359,362d356
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
-366c360,364
+368c362,366
< [scope:rm_asserts] removing 9 assertion(s)
---
> [eva:garbled-mix:summary] Warning:
@@ -30,7 +30,7 @@
> addition.i:59: misaligned read of addresses
> (read 1 times, propagated 2 times) garbled mix of &{p1}
> [scope:rm_asserts] removing 7 assertion(s)
-389c387
-< p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
+393c391
+< {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
---
-> p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
+> {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
diff --git a/tests/value/oracle_equality/bitfield.res.oracle b/tests/value/oracle_equality/bitfield.res.oracle
index cfff35a117cceb9cdbac66aca878b2a19735854b..d8fa5662f8993ea18aae6c740069a2253c9740e2 100644
--- a/tests/value/oracle_equality/bitfield.res.oracle
+++ b/tests/value/oracle_equality/bitfield.res.oracle
@@ -1,7 +1,7 @@
137a138,140
> [eva] bitfield.i:71:
> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
213c216
< (read 5 times, propagated 7 times) garbled mix of &{b; ee}
---
diff --git a/tests/value/oracle_gauges/bitfield.res.oracle b/tests/value/oracle_gauges/bitfield.res.oracle
index e84586701d0d94c7fe0b6eeef82d99fb3522fe2c..619b7b85a2389c7c7816e21f58c56851130dcdb0 100644
--- a/tests/value/oracle_gauges/bitfield.res.oracle
+++ b/tests/value/oracle_gauges/bitfield.res.oracle
@@ -1,19 +1,19 @@
137a138,152
> [eva] bitfield.i:71:
> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
> [eva] bitfield.i:73:
> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
> [eva] computing for function leaf <- imprecise_bts_1671 <- main.
> Called from bitfield.i:70.
> [eva] Done for function leaf
> [eva] bitfield.i:71:
> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
> [eva] bitfield.i:73:
> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
213c228
< (read 5 times, propagated 7 times) garbled mix of &{b; ee}
---
diff --git a/tests/value/oracle_octagon/bitfield.res.oracle b/tests/value/oracle_octagon/bitfield.res.oracle
index cfff35a117cceb9cdbac66aca878b2a19735854b..d8fa5662f8993ea18aae6c740069a2253c9740e2 100644
--- a/tests/value/oracle_octagon/bitfield.res.oracle
+++ b/tests/value/oracle_octagon/bitfield.res.oracle
@@ -1,7 +1,7 @@
137a138,140
> [eva] bitfield.i:71:
> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {bitfield.i:70}) }}
+> {{ garbled mix of &{b} (origin: Misaligned read {bitfield.i:70}) }}
213c216
< (read 5 times, propagated 7 times) garbled mix of &{b; ee}
---