diff --git a/src/plugins/alias/src/simplified.ml b/src/plugins/alias/src/simplified.ml
index 9575c4b141e0ee5a44cbfcb351d8808c4d31e0c2..f9722a3a84153361f7f8a6cb10121d50feabef65 100644
--- a/src/plugins/alias/src/simplified.ml
+++ b/src/plugins/alias/src/simplified.ml
@@ -46,7 +46,7 @@ let check_cast_compatibility e typ =
~once:true
~source:(fst @@ e.eloc)
~wkey:Options.Warn.unsafe_cast
- "unsafe cast from %a to %a"
+ "unsafe cast from %a to %a; analysis may be unsound"
Printer.pp_typ type_of_e Printer.pp_typ typ
let rec simplify_offset o =
diff --git a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
index 2ff8f37ad868abc5bc0a0450918f0ad672bf07e7..6f28983041a9548ea145586af5b025e6f55815ed 100644
--- a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
@@ -13,11 +13,13 @@
[alias] May-aliases after instruction float *d = (float *)0; are <none>
[alias] May-alias graph after instruction float *d = (float *)0; is <empty>
[alias] analysing instruction: a = (int *)c;
-[alias:unsafe-cast] cast1.c:10: Warning: unsafe cast from float * to int *
+[alias:unsafe-cast] cast1.c:10: Warning:
+ unsafe cast from float * to int *; analysis may be unsound
[alias] May-aliases after instruction a = (int *)c; are { a; c }
[alias] May-alias graph after instruction a = (int *)c; is 0:{ a; c } → 1:{ }
[alias] analysing instruction: d = (float *)b;
-[alias:unsafe-cast] cast1.c:11: Warning: unsafe cast from int * to float *
+[alias:unsafe-cast] cast1.c:11: Warning:
+ unsafe cast from int * to float *; analysis may be unsound
[alias] May-aliases after instruction d = (float *)b; are { a; c } { b; d }
[alias] May-alias graph after instruction d = (float *)b; is
0:{ a; c } → 1:{ } 4:{ b; d } → 5:{ }
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle
index f3a0e1ed6560aab76be3d59636ddaf3d8d6d2ab8..61e807ea83e559e4519cf69b6ad02b5219e05a79 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/origin.res.oracle
@@ -6,14 +6,17 @@
[alias] May-aliases after instruction tmp = & f; are <none>
[alias] May-alias graph after instruction tmp = & f; is 0:{ tmp } → 1:{ f }
[alias] analysing instruction: tmp = (void (*)(void))*((char *)(v.t));
-[alias:unsafe-cast] origin.c:8: Warning: unsafe cast from char to void (*)(void)
-[alias:unsafe-cast] origin.c:8: Warning: unsafe cast from int * to char *
+[alias:unsafe-cast] origin.c:8: Warning:
+ unsafe cast from char to void (*)(void); analysis may be unsound
+[alias:unsafe-cast] origin.c:8: Warning:
+ unsafe cast from int * to char *; analysis may be unsound
[alias] May-aliases after instruction tmp = (void (*)(void))*((char *)(v.t)); are
{ v[0..].t; tmp }
[alias] May-alias graph after instruction tmp = (void (*)(void))*((char *)(v.t));
is 0:{ tmp } → 1:{ f } 4:{ v } -t→ 5:{ } 5:{ } → 0:{ tmp }
[alias] analysing instruction: int g = (int)tmp;
-[alias:unsafe-cast] origin.c:8: Warning: unsafe cast from void (*)(void) to int
+[alias:unsafe-cast] origin.c:8: Warning:
+ unsafe cast from void (*)(void) to int; analysis may be unsound
[alias] May-aliases after instruction int g = (int)tmp; are { v[0..].t; tmp }
[alias] May-alias graph after instruction int g = (int)tmp; is
0:{ tmp } → 1:{ f } 4:{ v } -t→ 5:{ } 5:{ } → 0:{ tmp }
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle
index d2f26b8474aae29aed9625dcdca5b3fbf6430807..a2bd76c05c80833b047d65bf7ccc14832534c631 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/origin_simpl.res.oracle
@@ -1,8 +1,10 @@
[kernel] Parsing origin_simpl.c (with preprocessing)
[alias] analysing function: f
[alias] analysing instruction: tmp = (void *)*((int *)(t));
-[alias:unsafe-cast] origin_simpl.c:9: Warning: unsafe cast from int to void *
-[alias:unsafe-cast] origin_simpl.c:9: Warning: unsafe cast from char * to int *
+[alias:unsafe-cast] origin_simpl.c:9: Warning:
+ unsafe cast from int to void *; analysis may be unsound
+[alias:unsafe-cast] origin_simpl.c:9: Warning:
+ unsafe cast from char * to int *; analysis may be unsound
[alias] May-aliases after instruction tmp = (void *)*((int *)(t)); are
{ t[0..]; tmp }
[alias] May-alias graph after instruction tmp = (void *)*((int *)(t)); is
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle
index 290c2dbe3ecff381c311ba3d005640bee0c2b1fa..4578be9b90595f900b17939cc99db92fcb83c5ed 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle
@@ -6,19 +6,19 @@
[alias] analysing function: f
[alias] analysing instruction: int *q = (int *)(& f);
[alias:unsafe-cast] reduce_by_valid.c:5: Warning:
- unsafe cast from void (*)(void) to int *
+ unsafe cast from void (*)(void) to int *; analysis may be unsound
[alias] May-aliases after instruction int *q = (int *)(& f); are <none>
[alias] May-alias graph after instruction int *q = (int *)(& f); is
0:{ q } → 1:{ f }
[alias] analysing instruction: int *p = (int *)(& f);
[alias:unsafe-cast] reduce_by_valid.c:5: Warning:
- unsafe cast from void (*)(void) to int *
+ unsafe cast from void (*)(void) to int *; analysis may be unsound
[alias] May-aliases after instruction int *p = (int *)(& f); are { q; p }
[alias] May-alias graph after instruction int *p = (int *)(& f); is
0:{ q } → 5:{ f } 4:{ p } → 5:{ f }
[alias] analysing instruction: p = (int *)(& q);
[alias:unsafe-cast] reduce_by_valid.c:6: Warning:
- unsafe cast from int ** to int *
+ unsafe cast from int ** to int *; analysis may be unsound
[alias:incoherent] Warning:
loop on vertex 5 (following unsafe cast?); analysis may be unsound
[alias:incoherent] Warning:
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle
index 14786295a9e7b48d1175d80c040fe1a01f180515..6e3f2b39e12d1f8c65cea91c82debacb92653fac 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/semver.res.oracle
@@ -6,7 +6,8 @@
[alias] Summary of function f:
[alias] analysing function: main
[alias] analysing instruction: f((int *)*("1" + 2));
-[alias:unsafe-cast] semver.c:6: Warning: unsafe cast from char to int *
+[alias:unsafe-cast] semver.c:6: Warning:
+ unsafe cast from char to int *; analysis may be unsound
[alias:unsupported:addr] semver.c:6: Warning:
unsupported feature: explicit pointer address: (int *)*("1" + 2); analysis may be unsound
[alias] May-aliases after instruction f((int *)*("1" + 2)); are <none>
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/tkn-2.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/tkn-2.res.oracle
index 6718bf0c37093b6cb0a8b7222931e426c49fc5d2..35600d0739a0721e456e21efd979fc4a9b5f597f 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/tkn-2.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/tkn-2.res.oracle
@@ -1,7 +1,8 @@
[kernel] Parsing tkn-2.c (with preprocessing)
[alias] analysing function: main
[alias] analysing instruction: a = (int *)(& a);
-[alias:unsafe-cast] tkn-2.c:6: Warning: unsafe cast from int ** to int *
+[alias:unsafe-cast] tkn-2.c:6: Warning:
+ unsafe cast from int ** to int *; analysis may be unsound
[alias] tkn-2.c:6: Warning: ignoring assignment of the form: a = (int *)(& a)
[alias] May-aliases after instruction a = (int *)(& a); are <none>
[alias] May-alias graph after instruction a = (int *)(& a); is
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle
index d26bef0851744c26efe2ff07aac57ceeea0f9932..3c37afd71491354a207c3f83f0d2c4cd509cf2aa 100644
--- a/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/union_vmap.res.oracle
@@ -8,14 +8,14 @@
[alias] Summary of function CPS_SplitWord:
formals: line locals: returns: line state: <none>
[alias:unsafe-cast] union_vmap.c:11: Warning:
- unsafe cast from char const * to char *
+ unsafe cast from char const * to char *; analysis may be unsound
[alias] May-aliases after instruction char *s2 = CPS_SplitWord((char *)"a"); are
<none>
[alias] May-alias graph after instruction char *s2 = CPS_SplitWord((char *)"a");
is 4:{ s2 } → 3:{ }
[alias] analysing instruction: char *s3 = CPS_SplitWord((char *)"b");
[alias:unsafe-cast] union_vmap.c:12: Warning:
- unsafe cast from char const * to char *
+ unsafe cast from char const * to char *; analysis may be unsound
[alias] May-aliases after instruction char *s3 = CPS_SplitWord((char *)"b"); are
<none>
[alias] May-alias graph after instruction char *s3 = CPS_SplitWord((char *)"b");
diff --git a/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle b/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
index 205196a3f3b5e0ed20819922884b49a0e3608704..8de6368366f950eb896184536bdc513deee950f9 100644
--- a/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
@@ -59,7 +59,7 @@
15:{ b } → 16:{ }
[alias] analysing instruction: z1->s = (struct struct_1_t *)tab_y[0];
[alias:unsafe-cast] nested1.c:47: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *
+ unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction z1->s = (struct struct_1_t *)tab_y[0]; are
{ z1->s; tab_y[0..] }
[alias] May-alias graph after instruction z1->s = (struct struct_1_t *)tab_y[0];
@@ -69,7 +69,7 @@
15:{ b } → 16:{ } 17:{ } → 2:{ x1; x2 }
[alias] analysing instruction: z2->s = (struct struct_1_t *)tab_y[1];
[alias:unsafe-cast] nested1.c:48: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *
+ unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction z2->s = (struct struct_1_t *)tab_y[1]; are
{ z1->s; z2->s; tab_y[0..] }
[alias] May-alias graph after instruction z2->s = (struct struct_1_t *)tab_y[1];
@@ -95,7 +95,7 @@
19:{ a } → 14:{ } 20:{ b } → 16:{ }
[alias] analysing instruction: t->t = (struct struct_2_t *)z1;
[alias:unsafe-cast] nested1.c:51: Warning:
- unsafe cast from st_2_t * to struct struct_2_t *
+ unsafe cast from st_2_t * to struct struct_2_t *; analysis may be unsound
[alias] May-aliases after instruction t->t = (struct struct_2_t *)z1; are
{ (t->t)->s; z1->s; z2->s; tab_y[0..] } { t->t; z1 }
{ (t->t)->c; z1->c; a } { z2->c; b }
diff --git a/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle b/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
index c141c4f0975a096c66eaba32f63c726128e27478..8cfb818473b614ba56a17d6c66a13e7806a024cf 100644
--- a/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
@@ -28,7 +28,7 @@
0:{ z1 } → 1:{ } 2:{ t } → 3:{ } 4:{ a } → 5:{ }
[alias] analysing instruction: z1->s[0] = (struct struct_1_t *)(& x1);
[alias:unsafe-cast] nested2.c:42: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *
+ unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction z1->s[0] = (struct struct_1_t *)(& x1); are
<none>
[alias] May-alias graph after instruction z1->s[0] = (struct struct_1_t *)(& x1);
@@ -37,7 +37,7 @@
4:{ a } → 5:{ } 6:{ } → 7:{ } 7:{ } → 8:{ x1 }
[alias] analysing instruction: z1->s[1] = (struct struct_1_t *)(& x2);
[alias:unsafe-cast] nested2.c:43: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *
+ unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction z1->s[1] = (struct struct_1_t *)(& x2); are
<none>
[alias] May-alias graph after instruction z1->s[1] = (struct struct_1_t *)(& x2);
@@ -52,7 +52,7 @@
12:{ a } → 5:{ }
[alias] analysing instruction: t->t = (struct struct_2_t *)z1;
[alias:unsafe-cast] nested2.c:45: Warning:
- unsafe cast from st_2_t * to struct struct_2_t *
+ unsafe cast from st_2_t * to struct struct_2_t *; analysis may be unsound
[alias] May-aliases after instruction t->t = (struct struct_2_t *)z1; are
{ t->t; z1 } { (t->t)->c; z1->c; a } { (t->t)->s; z1->s }
{ (*(t->t))[0..].s; (*z1)[0..].s }
diff --git a/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle
index 668bf60c584a9a158f652be25a79484f51ad5da5..ec9e2cf954ad39bf8f260d9742d651784504a9ac 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle
@@ -22,7 +22,7 @@
0:{ p_x } → 1:{ x } 4:{ p_y } → 5:{ y }
[alias] analysing instruction: p_x = (st_1_t *)p_y;
[alias:unsafe-cast] structure1.c:28: Warning:
- unsafe cast from st_2_t * to st_1_t *
+ unsafe cast from st_2_t * to st_1_t *; analysis may be unsound
[alias] May-aliases after instruction p_x = (st_1_t *)p_y; are { p_x; p_y }
[alias] May-alias graph after instruction p_x = (st_1_t *)p_y; is
0:{ p_x; p_y } → 1:{ x; y }
diff --git a/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle
index 562ebe1bde826d33f6064be99896bbb04f880ae0..494d53e438c9ef59f8f78eb0246b1b0db2364f53 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle
@@ -10,7 +10,7 @@
<empty>
[alias] analysing instruction: st_2_t y = {.s = (struct struct_1_t *)(& x1), .c = 4};
[alias:unsafe-cast] structure2.c:21: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *
+ unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction
st_2_t y = {.s = (struct struct_1_t *)(& x1), .c = 4}; are <none>
[alias] May-alias graph after instruction
@@ -18,7 +18,7 @@
0:{ y } -s→ 1:{ } 1:{ } → 2:{ x1 }
[alias] analysing instruction: y.s = (struct struct_1_t *)(& x2);
[alias:unsafe-cast] structure2.c:23: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *
+ unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction y.s = (struct struct_1_t *)(& x2); are
<none>
[alias] May-alias graph after instruction y.s = (struct struct_1_t *)(& x2); is
diff --git a/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
index eaf97b2e49ddcebdbb90e61cc279d73fb1600556..494f0550054e5102ded232507dcbeb837279ce81 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
@@ -24,7 +24,7 @@
0:{ y1 } → 1:{ x1 } 2:{ z } → 3:{ }
[alias] analysing instruction: z->s = (struct struct_1_t *)y1;
[alias:unsafe-cast] structure4.c:37: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *
+ unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction z->s = (struct struct_1_t *)y1; are
{ z->s; y1 }
[alias] May-alias graph after instruction z->s = (struct struct_1_t *)y1; is
diff --git a/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
index a056387b5c55b6d3a57074d44bbc72e88172fdd0..93f0980905f5396583070a4a86dd29b4cd9967ac 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
@@ -40,7 +40,7 @@
6:{ a } → 7:{ }
[alias] analysing instruction: z->s = (struct struct_1_t *)y1;
[alias:unsafe-cast] structure5.c:41: Warning:
- unsafe cast from st_1_t * to struct struct_1_t *
+ unsafe cast from st_1_t * to struct struct_1_t *; analysis may be unsound
[alias] May-aliases after instruction z->s = (struct struct_1_t *)y1; are
{ z->s; y1 }
[alias] May-alias graph after instruction z->s = (struct struct_1_t *)y1; is
@@ -53,7 +53,7 @@
4:{ t } → 5:{ } 10:{ y1 } → 1:{ x1 } 11:{ a } → 7:{ }
[alias] analysing instruction: t->t = (struct struct_2_t *)z;
[alias:unsafe-cast] structure5.c:43: Warning:
- unsafe cast from st_2_t * to struct struct_2_t *
+ unsafe cast from st_2_t * to struct struct_2_t *; analysis may be unsound
[alias] May-aliases after instruction t->t = (struct struct_2_t *)z; are
{ (t->t)->s; z->s; y1 } { t->t; z } { (t->t)->c; z->c; a }
[alias] May-alias graph after instruction t->t = (struct struct_2_t *)z; is