diff --git a/src/plugins/alias/abstract_state.ml b/src/plugins/alias/abstract_state.ml
index 1fb606d3893ee084b0f123eeda4e3d49f2bed07c..1dfce6cfd292570d307a8d1cc9b345f1e07721f9 100644
--- a/src/plugins/alias/abstract_state.ml
+++ b/src/plugins/alias/abstract_state.ml
@@ -263,7 +263,9 @@ let print_aliases fmt (x:t) =
if LSet.cardinal aliases >= 2 then Some aliases else None
in
let alias_sets = VMap.filter_map alias_set_of_vertex x.vmap in
- VMap.iter print_alias_set alias_sets
+ if VMap.is_empty alias_sets
+ then Format.fprintf fmt "<none>"
+ else VMap.iter print_alias_set alias_sets
(** invariants of type t must be true before and after each functon call *)
let assert_invariants (x:t) : unit =
diff --git a/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
index d9c4c50457394c00c1f75827d74ea3455aadce76..35feff272aa3d7f264918b020b9a8c8c2f79f1ae 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
@@ -3,15 +3,19 @@
[alias] analysing instruction: int *a = (int *)0;
[alias:unsafe-cast] assignment1.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *a = (int *)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] assignment1.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: int *c = (int *)0;
[alias:unsafe-cast] assignment1.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *c = (int *)0;
+ <none>
[alias] analysing instruction: int *d = (int *)0;
[alias:unsafe-cast] assignment1.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *d = (int *)0;
+ <none>
[alias] analysing instruction: a = b;
[alias] May-aliases at the end of instruction: a = b;
{a, b} are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
index 6438b8a5e18e97cc8b28782fd21268c72afdd317..0752c920750aa7cc1708d76b0d48ce8bdb8cc271 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
@@ -3,15 +3,19 @@
[alias] analysing instruction: int **a = (int **)0;
[alias:unsafe-cast] assignment2.c:8: Warning: unsafe cast from int to int **
[alias] May-aliases at the end of instruction: int **a = (int **)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] assignment2.c:8: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: int **c = (int **)0;
[alias:unsafe-cast] assignment2.c:8: Warning: unsafe cast from int to int **
[alias] May-aliases at the end of instruction: int **c = (int **)0;
+ <none>
[alias] analysing instruction: int *d = (int *)0;
[alias:unsafe-cast] assignment2.c:8: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *d = (int *)0;
+ <none>
[alias] analysing instruction: *a = b;
[alias] May-aliases at the end of instruction: *a = b;
{*a, b} are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
index 198c7753a2fe4bd733c91b14cbe52646a333ff54..7c4c81fba2ceaa36adad750f55dfc17066abae95 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
@@ -3,13 +3,17 @@
[alias] analysing instruction: int *a = (int *)0;
[alias:unsafe-cast] assignment3.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *a = (int *)0;
+ <none>
[alias] analysing instruction: int b = 0;
[alias] May-aliases at the end of instruction: int b = 0;
+ <none>
[alias] analysing instruction: int *c = (int *)0;
[alias:unsafe-cast] assignment3.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *c = (int *)0;
+ <none>
[alias] analysing instruction: a = & b;
[alias] May-aliases at the end of instruction: a = & b;
+ <none>
[alias] analysing instruction: c = & b;
[alias] May-aliases at the end of instruction: c = & b;
{a, c} are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/assignment4.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment4.res.oracle
index 7c1c4f02990fa5f236a2b317c24ffb248a81e7ea..511454fecf5e28a330ed48ca4978924fd10e96d8 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment4.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment4.res.oracle
@@ -3,15 +3,19 @@
[alias] analysing instruction: int **a = (int **)0;
[alias:unsafe-cast] assignment4.c:8: Warning: unsafe cast from int to int **
[alias] May-aliases at the end of instruction: int **a = (int **)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] assignment4.c:8: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: int **c = (int **)0;
[alias:unsafe-cast] assignment4.c:8: Warning: unsafe cast from int to int **
[alias] May-aliases at the end of instruction: int **c = (int **)0;
+ <none>
[alias] analysing instruction: int *d = (int *)0;
[alias:unsafe-cast] assignment4.c:8: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *d = (int *)0;
+ <none>
[alias] analysing instruction: *a = b;
[alias] May-aliases at the end of instruction: *a = b;
{*a, b} are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/assignment5.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment5.res.oracle
index f54e8937508c15e80dec22fdb213f8301c180159..694d63e03079929da6ea16a2b5c345d13651cca5 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment5.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment5.res.oracle
@@ -3,15 +3,19 @@
[alias] analysing instruction: int ***a = (int ***)0;
[alias:unsafe-cast] assignment5.c:7: Warning: unsafe cast from int to int ***
[alias] May-aliases at the end of instruction: int ***a = (int ***)0;
+ <none>
[alias] analysing instruction: int **b = (int **)0;
[alias:unsafe-cast] assignment5.c:7: Warning: unsafe cast from int to int **
[alias] May-aliases at the end of instruction: int **b = (int **)0;
+ <none>
[alias] analysing instruction: int *c = (int *)0;
[alias:unsafe-cast] assignment5.c:7: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *c = (int *)0;
+ <none>
[alias] analysing instruction: int *d = (int *)0;
[alias:unsafe-cast] assignment5.c:7: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *d = (int *)0;
+ <none>
[alias] analysing instruction: *a = b;
[alias] May-aliases at the end of instruction: *a = b;
{*a, b} are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
index c568a7791dce1d06f669710c3649a1b307be12be..66df1e6f0e9f771057e1cf9672412510bfff0285 100644
--- a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
@@ -3,15 +3,19 @@
[alias] analysing instruction: int *a = (int *)0;
[alias:unsafe-cast] cast1.c:8: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *a = (int *)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] cast1.c:8: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: float *c = (float *)0;
[alias:unsafe-cast] cast1.c:9: Warning: unsafe cast from int to float *
[alias] May-aliases at the end of instruction: float *c = (float *)0;
+ <none>
[alias] analysing instruction: float *d = (float *)0;
[alias:unsafe-cast] cast1.c:9: Warning: unsafe cast from int to float *
[alias] May-aliases at the end of instruction: float *d = (float *)0;
+ <none>
[alias] analysing instruction: a = (int *)c;
[alias:unsafe-cast] cast1.c:10: Warning: unsafe cast from float * to int *
[alias] May-aliases at the end of instruction: a = (int *)c;
diff --git a/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle b/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
index a2bcc51e7ecacd448aca31eb0288ee096094366a..9b38a767a32e9e3ca1843afef5847dae0b043cb1 100644
--- a/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
@@ -3,12 +3,15 @@
[alias] analysing instruction: int *a = (int *)0;
[alias:unsafe-cast] conditional1.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *a = (int *)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] conditional1.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: int *c = (int *)0;
[alias:unsafe-cast] conditional1.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *c = (int *)0;
+ <none>
[alias] analysing instruction: a = b;
[alias] May-aliases at the end of instruction: a = b;
{a, b} are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/function1.res.oracle b/src/plugins/alias/tests/basic/oracle/function1.res.oracle
index 5856da9a875a376e544fff383104dd8a68a2496d..0158b97495e72ed4e904d1200351b0f5af6b2ed4 100644
--- a/src/plugins/alias/tests/basic/oracle/function1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function1.res.oracle
@@ -3,20 +3,25 @@
[alias] analysing instruction: int *a = (int *)0;
[alias:unsafe-cast] function1.c:16: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *a = (int *)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] function1.c:16: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: int *c = (int *)0;
[alias:unsafe-cast] function1.c:16: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *c = (int *)0;
+ <none>
[alias] analysing instruction: int *d = (int *)0;
[alias:unsafe-cast] function1.c:16: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *d = (int *)0;
+ <none>
[alias] analysing instruction: swap(a,b);
[alias] analysing function: swap
[alias] analysing instruction: int *z = (int *)0;
[alias:unsafe-cast] function1.c:7: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *z = (int *)0;
+ <none>
[alias] analysing instruction: z = x;
[alias] May-aliases at the end of instruction: z = x;
{x, z} are aliased
@@ -44,5 +49,6 @@
[alias] analysing function: swap
[alias] analysing instruction: int *z = (int *)0;
[alias] May-aliases at the end of instruction: int *z = (int *)0;
+ <none>
[alias] May-aliases at the end of function swap:
{x, y, z} are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/function2.res.oracle b/src/plugins/alias/tests/basic/oracle/function2.res.oracle
index e2730b111c1f03ebb0d6910b4eebd8f46358b3d6..48b64d74e02e63624068e8a1424b1c87698adcb9 100644
--- a/src/plugins/alias/tests/basic/oracle/function2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function2.res.oracle
@@ -75,23 +75,32 @@
[alias] analysing instruction: int *a = (int *)0;
[alias:unsafe-cast] function2.c:14: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *a = (int *)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] function2.c:14: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: a = my_malloc(2);
[alias] analysing function: my_malloc
[alias] analysing instruction: int *res = (int *)0;
[alias:unsafe-cast] function2.c:7: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *res = (int *)0;
+ <none>
[alias] analysing instruction: res = (int *)malloc((size_t)size);
[alias] May-aliases at the end of instruction: res = (int *)malloc((size_t)size);
+ <none>
[alias] May-aliases at the end of function my_malloc:
+ <none>
[alias] May-aliases at the end of instruction: a = my_malloc(2);
+ <none>
[alias] analysing instruction: b = my_malloc(3);
[alias] May-aliases at the end of instruction: b = my_malloc(3);
+ <none>
[alias] analysing instruction: __retres = 0;
[alias] May-aliases at the end of instruction: __retres = 0;
+ <none>
[alias] May-aliases at the end of function main:
+ <none>
[alias] analysing function: malloc
[alias] May-aliases at the end of function malloc:
<Bot>
@@ -116,7 +125,9 @@
[alias] analysing function: my_malloc
[alias] analysing instruction: int *res = (int *)0;
[alias] May-aliases at the end of instruction: int *res = (int *)0;
+ <none>
[alias] May-aliases at the end of function my_malloc:
+ <none>
[alias] analysing function: nrand48
[alias] May-aliases at the end of function nrand48:
<Bot>
diff --git a/src/plugins/alias/tests/basic/oracle/function3.res.oracle b/src/plugins/alias/tests/basic/oracle/function3.res.oracle
index 1ca2d7367e852b8933c89f920f09051bb02d42d3..d61cfa89c476c823865e5ae9a80dcc44a78bbbb6 100644
--- a/src/plugins/alias/tests/basic/oracle/function3.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function3.res.oracle
@@ -19,15 +19,19 @@
[alias] analysing instruction: int *a = (int *)0;
[alias:unsafe-cast] function3.c:19: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *a = (int *)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] function3.c:19: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: int *c = (int *)0;
[alias:unsafe-cast] function3.c:19: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *c = (int *)0;
+ <none>
[alias] analysing instruction: int *d = (int *)0;
[alias:unsafe-cast] function3.c:19: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *d = (int *)0;
+ <none>
[alias] analysing instruction: f1(a,b);
[alias] May-aliases at the end of instruction: f1(a,b);
{a, b} are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/function4.res.oracle b/src/plugins/alias/tests/basic/oracle/function4.res.oracle
index 0fc294049b7fea572a854fef404f6013620f5c60..ee692419b85e2d65eff2ede09e180a37643bc529 100644
--- a/src/plugins/alias/tests/basic/oracle/function4.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function4.res.oracle
@@ -1,15 +1,19 @@
[kernel] Parsing function4.c (with preprocessing)
[alias] analysing function: addr
[alias] May-aliases at the end of function addr:
+ <none>
[alias] analysing function: main
[alias] analysing instruction: int *a = (int *)0;
[alias:unsafe-cast] function4.c:11: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *a = (int *)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] function4.c:11: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: int c = 0;
[alias] May-aliases at the end of instruction: int c = 0;
+ <none>
[alias] analysing instruction: a = addr(& c);
[alias] May-aliases at the end of instruction: a = addr(& c);
{a, &c} are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/function5.res.oracle b/src/plugins/alias/tests/basic/oracle/function5.res.oracle
index 8510888b05902e1aa75cb21943778e320c76db5c..c496bb34f2ea5ad2bca169618e518b2f981d70ff 100644
--- a/src/plugins/alias/tests/basic/oracle/function5.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function5.res.oracle
@@ -2,6 +2,7 @@
[alias] analysing function: choice
[alias] analysing instruction: int c = 0;
[alias] May-aliases at the end of instruction: int c = 0;
+ <none>
[alias] analysing instruction: __retres = x;
[alias] May-aliases at the end of instruction: __retres = x;
{x, __retres} are aliased
@@ -14,12 +15,15 @@
[alias] analysing instruction: int *a = (int *)0;
[alias:unsafe-cast] function5.c:16: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *a = (int *)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] function5.c:16: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: int *c = (int *)0;
[alias:unsafe-cast] function5.c:16: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *c = (int *)0;
+ <none>
[alias] analysing instruction: c = choice(a,b);
[alias] May-aliases at the end of instruction: c = choice(a,b);
{a, b, c} are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/globctr.res.oracle b/src/plugins/alias/tests/basic/oracle/globctr.res.oracle
index d18490d7bac02d9b06190fab61dabe3e33093def..17c4dd29081011c15de3336ec754e6484c321e1c 100644
--- a/src/plugins/alias/tests/basic/oracle/globctr.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/globctr.res.oracle
@@ -2,20 +2,29 @@
[alias] analysing function: f
[alias] analysing instruction: int y = 0;
[alias] May-aliases at the end of instruction: int y = 0;
+ <none>
[alias] analysing instruction: *x = y;
[alias] May-aliases at the end of instruction: *x = y;
+ <none>
[alias] May-aliases at the end of function f:
+ <none>
[alias] analysing function: main
[alias] analysing instruction: int *a = (int *)0;
[alias:unsafe-cast] globctr.c:8: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *a = (int *)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] globctr.c:8: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: f(a);
[alias] May-aliases at the end of instruction: f(a);
+ <none>
[alias] analysing instruction: f(b);
[alias] May-aliases at the end of instruction: f(b);
+ <none>
[alias] analysing instruction: __retres = 0;
[alias] May-aliases at the end of instruction: __retres = 0;
+ <none>
[alias] May-aliases at the end of function main:
+ <none>
diff --git a/src/plugins/alias/tests/basic/oracle/loop.res.oracle b/src/plugins/alias/tests/basic/oracle/loop.res.oracle
index 450aa956b42dcc72c2e543dac736e8d41140feb0..1d41d498ffd21c1772fc41a593513fc6ff400939 100644
--- a/src/plugins/alias/tests/basic/oracle/loop.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/loop.res.oracle
@@ -2,18 +2,26 @@
[alias] analysing function: main
[alias] analysing instruction: int l[1] = {0};
[alias] May-aliases at the end of instruction: int l[1] = {0};
+ <none>
[alias] analysing instruction: int *n_0 = & l[1];
[alias] May-aliases at the end of instruction: int *n_0 = & l[1];
+ <none>
[alias] analysing instruction: n_0 = & l[1] + 0;
[alias] May-aliases at the end of instruction: n_0 = & l[1] + 0;
+ <none>
[alias] analysing instruction: int w = 0;
[alias] May-aliases at the end of instruction: int w = 0;
+ <none>
[alias] analysing instruction: l[0] = *(& l[1] + 0);
[alias] May-aliases at the end of instruction: l[0] = *(& l[1] + 0);
+ <none>
[alias] analysing instruction: int l[1] = {0};
[alias] May-aliases at the end of instruction: int l[1] = {0};
+ <none>
[alias] analysing instruction: int *n_0 = & l[1];
[alias] May-aliases at the end of instruction: int *n_0 = & l[1];
+ <none>
[alias:no-return] loop.c:4: Warning:
function main does not return; analysis may be unsound
[alias] May-aliases at the end of function main:
+ <none>
diff --git a/src/plugins/alias/tests/basic/oracle/steensgaard.res.oracle b/src/plugins/alias/tests/basic/oracle/steensgaard.res.oracle
index 04c2159b213ea59357eaa951182324fc22fc4062..62e77694dee4e71ae277497d3cb4c4a4a72cb84f 100644
--- a/src/plugins/alias/tests/basic/oracle/steensgaard.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/steensgaard.res.oracle
@@ -2,6 +2,7 @@
[alias] analysing function: main
[alias] analysing instruction: a = & x;
[alias] May-aliases at the end of instruction: a = & x;
+ <none>
[alias] analysing instruction: b = & y;
[alias] May-aliases at the end of instruction: b = & y;
{*b, y} are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/switch1.res.oracle b/src/plugins/alias/tests/basic/oracle/switch1.res.oracle
index b6e49fd381fe697804583c01399cef8fb9df795b..c1202c16d1d3b93ea83c1a2911453676ddd5bd63 100644
--- a/src/plugins/alias/tests/basic/oracle/switch1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/switch1.res.oracle
@@ -3,17 +3,22 @@
[alias] analysing instruction: int *a = (int *)0;
[alias:unsafe-cast] switch1.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *a = (int *)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] switch1.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: int *c = (int *)0;
[alias:unsafe-cast] switch1.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *c = (int *)0;
+ <none>
[alias] analysing instruction: int *d = (int *)0;
[alias:unsafe-cast] switch1.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *d = (int *)0;
+ <none>
[alias] analysing instruction: int e = 0;
[alias] May-aliases at the end of instruction: int e = 0;
+ <none>
[alias] analysing instruction: case 1: a = d;
[alias] May-aliases at the end of instruction: case 1: a = d;
{a, d} are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/switch2.res.oracle b/src/plugins/alias/tests/basic/oracle/switch2.res.oracle
index d9a802df5fdbd53792aa8e1249b7d5ae98fd41ec..0a1a041476a6897f282d50acacff595ac70c1686 100644
--- a/src/plugins/alias/tests/basic/oracle/switch2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/switch2.res.oracle
@@ -3,17 +3,22 @@
[alias] analysing instruction: int *a = (int *)0;
[alias:unsafe-cast] switch2.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *a = (int *)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] switch2.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: int *c = (int *)0;
[alias:unsafe-cast] switch2.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *c = (int *)0;
+ <none>
[alias] analysing instruction: int *d = (int *)0;
[alias:unsafe-cast] switch2.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *d = (int *)0;
+ <none>
[alias] analysing instruction: int e = 0;
[alias] May-aliases at the end of instruction: int e = 0;
+ <none>
[alias] analysing instruction: case 1: a = d;
[alias] May-aliases at the end of instruction: case 1: a = d;
{a, d} are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle b/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
index 062e40c3dbc1d4169dfe9bf2ed440e7d6d32948c..7115798d02599035b7ecb026b1cad4f51cbb6160 100644
--- a/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
@@ -75,17 +75,24 @@
[alias] analysing instruction: int *s = (int *)0;
[alias:unsafe-cast] while_for1.c:8: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *s = (int *)0;
+ <none>
[alias] analysing instruction: int idx = 0;
[alias] May-aliases at the end of instruction: int idx = 0;
+ <none>
[alias] analysing instruction: s = (int *)malloc((size_t)idx);
[alias] May-aliases at the end of instruction: s = (int *)malloc((size_t)idx);
+ <none>
[alias] analysing instruction: idx ++;
[alias] May-aliases at the end of instruction: idx ++;
+ <none>
[alias] analysing instruction: s = (int *)malloc((size_t)idx);
[alias] May-aliases at the end of instruction: s = (int *)malloc((size_t)idx);
+ <none>
[alias] analysing instruction: __retres = 0;
[alias] May-aliases at the end of instruction: __retres = 0;
+ <none>
[alias] May-aliases at the end of function main:
+ <none>
[alias] analysing function: malloc
[alias] May-aliases at the end of function malloc:
<Bot>
diff --git a/src/plugins/alias/tests/basic/oracle/while_for2.res.oracle b/src/plugins/alias/tests/basic/oracle/while_for2.res.oracle
index 0f4e8cd08889a5510d4a50af09e22926c563bf5f..6c08aec861c4ae6f6ed83cf2022d32aa772ac855 100644
--- a/src/plugins/alias/tests/basic/oracle/while_for2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/while_for2.res.oracle
@@ -3,12 +3,15 @@
[alias] analysing instruction: int *a = (int *)0;
[alias:unsafe-cast] while_for2.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *a = (int *)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] while_for2.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: int *c = (int *)0;
[alias:unsafe-cast] while_for2.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *c = (int *)0;
+ <none>
[alias] analysing instruction: a = b;
[alias] May-aliases at the end of instruction: a = b;
{a, b} are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/while_for3.res.oracle b/src/plugins/alias/tests/basic/oracle/while_for3.res.oracle
index f7d9211bc9cdd4e029ce808077cc67253683cfad..b3c5b194e251934b65b315089ea03d1dac3fbcb3 100644
--- a/src/plugins/alias/tests/basic/oracle/while_for3.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/while_for3.res.oracle
@@ -3,14 +3,18 @@
[alias] analysing instruction: int *a = (int *)0;
[alias:unsafe-cast] while_for3.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *a = (int *)0;
+ <none>
[alias] analysing instruction: int *b = (int *)0;
[alias:unsafe-cast] while_for3.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *b = (int *)0;
+ <none>
[alias] analysing instruction: int *c = (int *)0;
[alias:unsafe-cast] while_for3.c:6: Warning: unsafe cast from int to int *
[alias] May-aliases at the end of instruction: int *c = (int *)0;
+ <none>
[alias] analysing instruction: int i = 0;
[alias] May-aliases at the end of instruction: int i = 0;
+ <none>
[alias] analysing instruction: a = b;
[alias] May-aliases at the end of instruction: a = b;
{a, b} are aliased
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 d5be4db46ad7c6ea28106e171c9cc0abc18636ab..57c8847db399d2c5af1bbc3d21ad0e71d1a16b43 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
@@ -3,13 +3,16 @@
[alias] analysing instruction: char *s2 = CPS_SplitWord((char *)"a");
[alias] analysing function: CPS_SplitWord
[alias] May-aliases at the end of function CPS_SplitWord:
+ <none>
[alias:unsafe-cast] union_vmap.c:11: Warning:
unsafe cast from char const * to char *
[alias] May-aliases at the end of instruction: char *s2 = CPS_SplitWord((char *)"a");
+ <none>
[alias] analysing instruction: char *s3 = CPS_SplitWord((char *)"b");
[alias:unsafe-cast] union_vmap.c:12: Warning:
unsafe cast from char const * to char *
[alias] May-aliases at the end of instruction: char *s3 = CPS_SplitWord((char *)"b");
+ <none>
[alias] analysing instruction: *key = s3;
[alias] May-aliases at the end of instruction: *key = s3;
{*key, s3} are aliased
@@ -20,3 +23,4 @@
{*key, s2, s3} are aliased
[alias] analysing function: CPS_SplitWord
[alias] May-aliases at the end of function CPS_SplitWord:
+ <none>
diff --git a/src/plugins/alias/tests/offsets/oracle/array1.res.oracle b/src/plugins/alias/tests/offsets/oracle/array1.res.oracle
index 9d030dbb3aa2cc915634ea334352e20670349c1c..3f8f04ebf187d0c1c68ae02ce2c0bb3e8c5821f9 100644
--- a/src/plugins/alias/tests/offsets/oracle/array1.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/array1.res.oracle
@@ -2,12 +2,16 @@
[alias] analysing function: main
[alias] analysing instruction: tab[0] = 0;
[alias] May-aliases at the end of instruction: tab[0] = 0;
+ <none>
[alias] analysing instruction: tab[1] = 1;
[alias] May-aliases at the end of instruction: tab[1] = 1;
+ <none>
[alias] analysing instruction: tab[2] = tab[1] + 1;
[alias] May-aliases at the end of instruction: tab[2] = tab[1] + 1;
+ <none>
[alias] analysing instruction: int *x = & tab[1];
[alias] May-aliases at the end of instruction: int *x = & tab[1];
+ <none>
[alias] analysing instruction: int *y = & tab[2];
[alias] May-aliases at the end of instruction: int *y = & tab[2];
{x, y} are aliased
diff --git a/src/plugins/alias/tests/offsets/oracle/array2.res.oracle b/src/plugins/alias/tests/offsets/oracle/array2.res.oracle
index 5b40ad5bdd892799a73d464e1f79a541ed9a4a57..d06aacf760b6ab340576e0c8ba4df75e97017bce 100644
--- a/src/plugins/alias/tests/offsets/oracle/array2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/array2.res.oracle
@@ -2,12 +2,18 @@
[alias] analysing function: main
[alias] analysing instruction: mat[0][0] = 0;
[alias] May-aliases at the end of instruction: mat[0][0] = 0;
+ <none>
[alias] analysing instruction: mat[0][1] = 1;
[alias] May-aliases at the end of instruction: mat[0][1] = 1;
+ <none>
[alias] analysing instruction: *x = mat[1];
[alias] May-aliases at the end of instruction: *x = mat[1];
+ <none>
[alias] analysing instruction: *y = *(*(x + 0));
[alias] May-aliases at the end of instruction: *y = *(*(x + 0));
+ <none>
[alias] analysing instruction: __retres = 0;
[alias] May-aliases at the end of instruction: __retres = 0;
+ <none>
[alias] May-aliases at the end of function main:
+ <none>
diff --git a/src/plugins/alias/tests/offsets/oracle/array3.res.oracle b/src/plugins/alias/tests/offsets/oracle/array3.res.oracle
index c6b7ce0876b86c80f30f5658a33167f562860303..906a7e049b409c9e75efbe8befafb77ff7305033 100644
--- a/src/plugins/alias/tests/offsets/oracle/array3.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/array3.res.oracle
@@ -75,11 +75,14 @@
[alias] analysing instruction: int *x = malloc((unsigned long)4 * sizeof(int));
[alias] May-aliases at the end of instruction: int *x =
malloc((unsigned long)4 * sizeof(int));
+ <none>
[alias] analysing instruction: int *y = malloc((unsigned long)4 * sizeof(int));
[alias] May-aliases at the end of instruction: int *y =
malloc((unsigned long)4 * sizeof(int));
+ <none>
[alias] analysing instruction: x = mat[0];
[alias] May-aliases at the end of instruction: x = mat[0];
+ <none>
[alias] analysing instruction: y = mat[1];
[alias] May-aliases at the end of instruction: y = mat[1];
{x, y} are aliased
diff --git a/src/plugins/alias/tests/offsets/oracle/collapse1.res.oracle b/src/plugins/alias/tests/offsets/oracle/collapse1.res.oracle
index f05bf7a178f46be89dd946cbaa738a3ac57a36a4..6f29399b235beffe6bb4ed138a6da9b148af4f03 100644
--- a/src/plugins/alias/tests/offsets/oracle/collapse1.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/collapse1.res.oracle
@@ -2,20 +2,30 @@
[alias] analysing function: main
[alias] analysing instruction: tab[0] = 0;
[alias] May-aliases at the end of instruction: tab[0] = 0;
+ <none>
[alias] analysing instruction: tab[1] = 1;
[alias] May-aliases at the end of instruction: tab[1] = 1;
+ <none>
[alias] analysing instruction: tab[2] = tab[1] + 1;
[alias] May-aliases at the end of instruction: tab[2] = tab[1] + 1;
+ <none>
[alias] analysing instruction: int x = 0;
[alias] May-aliases at the end of instruction: int x = 0;
+ <none>
[alias] analysing instruction: int i = 0;
[alias] May-aliases at the end of instruction: int i = 0;
+ <none>
[alias] analysing instruction: x = tab[i];
[alias] May-aliases at the end of instruction: x = tab[i];
+ <none>
[alias] analysing instruction: i ++;
[alias] May-aliases at the end of instruction: i ++;
+ <none>
[alias] analysing instruction: x = tab[i];
[alias] May-aliases at the end of instruction: x = tab[i];
+ <none>
[alias] analysing instruction: __retres = 0;
[alias] May-aliases at the end of instruction: __retres = 0;
+ <none>
[alias] May-aliases at the end of function main:
+ <none>
diff --git a/src/plugins/alias/tests/offsets/oracle/collapse2.res.oracle b/src/plugins/alias/tests/offsets/oracle/collapse2.res.oracle
index c0ff26fc5ba6107174a7e8310ee137eb031bd9c7..5aa489b069740ccced73907814066a7acf73343e 100644
--- a/src/plugins/alias/tests/offsets/oracle/collapse2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/collapse2.res.oracle
@@ -2,16 +2,24 @@
[alias] analysing function: main
[alias] analysing instruction: mat[0][0] = 0;
[alias] May-aliases at the end of instruction: mat[0][0] = 0;
+ <none>
[alias] analysing instruction: mat[0][1] = 1;
[alias] May-aliases at the end of instruction: mat[0][1] = 1;
+ <none>
[alias] analysing instruction: int i = 2;
[alias] May-aliases at the end of instruction: int i = 2;
+ <none>
[alias] analysing instruction: mat[1][i] = i;
[alias] May-aliases at the end of instruction: mat[1][i] = i;
+ <none>
[alias] analysing instruction: i ++;
[alias] May-aliases at the end of instruction: i ++;
+ <none>
[alias] analysing instruction: mat[1][i] = 2;
[alias] May-aliases at the end of instruction: mat[1][i] = 2;
+ <none>
[alias] analysing instruction: __retres = 0;
[alias] May-aliases at the end of instruction: __retres = 0;
+ <none>
[alias] May-aliases at the end of function main:
+ <none>
diff --git a/src/plugins/alias/tests/offsets/oracle/collapse3.res.oracle b/src/plugins/alias/tests/offsets/oracle/collapse3.res.oracle
index d21454382007b918bbaf3f2491d7d4b78d2dc1f7..cc02a1b6694dc7c598c495002cf75ff9cc902c17 100644
--- a/src/plugins/alias/tests/offsets/oracle/collapse3.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/collapse3.res.oracle
@@ -2,16 +2,24 @@
[alias] analysing function: main
[alias] analysing instruction: mat[0][0] = 0;
[alias] May-aliases at the end of instruction: mat[0][0] = 0;
+ <none>
[alias] analysing instruction: mat[0][1] = 1;
[alias] May-aliases at the end of instruction: mat[0][1] = 1;
+ <none>
[alias] analysing instruction: int i = 2;
[alias] May-aliases at the end of instruction: int i = 2;
+ <none>
[alias] analysing instruction: mat[i][1] = i;
[alias] May-aliases at the end of instruction: mat[i][1] = i;
+ <none>
[alias] analysing instruction: i ++;
[alias] May-aliases at the end of instruction: i ++;
+ <none>
[alias] analysing instruction: mat[i][1] = 2;
[alias] May-aliases at the end of instruction: mat[i][1] = 2;
+ <none>
[alias] analysing instruction: __retres = 0;
[alias] May-aliases at the end of instruction: __retres = 0;
+ <none>
[alias] May-aliases at the end of function main:
+ <none>
diff --git a/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle b/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
index 07c0fc998a1e5c4eea793c98a03384ee689d9149..9e0ad0d28c8720906f81018b35f67215ea1aad64 100644
--- a/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/nested1.res.oracle
@@ -74,26 +74,37 @@
[alias] analysing function: main
[alias] analysing instruction: st_1_t x1 = {.a = 0, .b = 1};
[alias] May-aliases at the end of instruction: st_1_t x1 = {.a = 0, .b = 1};
+ <none>
[alias] analysing instruction: st_1_t x2 = {.a = 1, .b = 2};
[alias] May-aliases at the end of instruction: st_1_t x2 = {.a = 1, .b = 2};
+ <none>
[alias] analysing instruction: tab_y[0] = & x1;
[alias] May-aliases at the end of instruction: tab_y[0] = & x1;
+ <none>
[alias] analysing instruction: tab_y[1] = & x2;
[alias] May-aliases at the end of instruction: tab_y[1] = & x2;
+ <none>
[alias] analysing instruction: st_2_t *z1 = malloc(sizeof(st_2_t));
[alias] May-aliases at the end of instruction: st_2_t *z1 = malloc(sizeof(st_2_t));
+ <none>
[alias] analysing instruction: st_2_t *z2 = malloc(sizeof(st_2_t));
[alias] May-aliases at the end of instruction: st_2_t *z2 = malloc(sizeof(st_2_t));
+ <none>
[alias] analysing instruction: st_3_t *t = malloc(sizeof(st_3_t));
[alias] May-aliases at the end of instruction: st_3_t *t = malloc(sizeof(st_3_t));
+ <none>
[alias] analysing instruction: int *a = malloc(sizeof(int));
[alias] May-aliases at the end of instruction: int *a = malloc(sizeof(int));
+ <none>
[alias] analysing instruction: int *b = malloc(sizeof(int));
[alias] May-aliases at the end of instruction: int *b = malloc(sizeof(int));
+ <none>
[alias] analysing instruction: *a = 0;
[alias] May-aliases at the end of instruction: *a = 0;
+ <none>
[alias] analysing instruction: *b = 5;
[alias] May-aliases at the end of instruction: *b = 5;
+ <none>
[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 *
diff --git a/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle b/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
index ffe8cf311a0c7ca4f0e770d2ac8c08662e273b31..2ca416be7fcc58a0b3a5d4f53d702a6c2e8a33f6 100644
--- a/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/nested2.res.oracle
@@ -74,24 +74,32 @@
[alias] analysing function: main
[alias] analysing instruction: st_1_t x1 = {.a = 0, .b = 1};
[alias] May-aliases at the end of instruction: st_1_t x1 = {.a = 0, .b = 1};
+ <none>
[alias] analysing instruction: st_1_t x2 = {.a = 2, .b = 3};
[alias] May-aliases at the end of instruction: st_1_t x2 = {.a = 2, .b = 3};
+ <none>
[alias] analysing instruction: st_2_t *z1 = malloc(sizeof(st_2_t));
[alias] May-aliases at the end of instruction: st_2_t *z1 = malloc(sizeof(st_2_t));
+ <none>
[alias] analysing instruction: st_3_t *t = malloc(sizeof(st_3_t));
[alias] May-aliases at the end of instruction: st_3_t *t = malloc(sizeof(st_3_t));
+ <none>
[alias] analysing instruction: int *a = malloc(sizeof(int));
[alias] May-aliases at the end of instruction: int *a = malloc(sizeof(int));
+ <none>
[alias] analysing instruction: *a = 0;
[alias] May-aliases at the end of instruction: *a = 0;
+ <none>
[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 *
[alias] May-aliases at the end of instruction: z1->s[0] = (struct struct_1_t *)(& x1);
+ <none>
[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 *
[alias] May-aliases at the end of instruction: z1->s[1] = (struct struct_1_t *)(& x2);
+ <none>
[alias] analysing instruction: z1->c = a;
[alias] May-aliases at the end of instruction: z1->c = a;
{z1->c, a} are aliased
diff --git a/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle
index bd470dc2d74aa30ca56876844fc1e90f198dd7da..ca2b271f23e48976dc0d28761119518bb79aa494 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure1.res.oracle
@@ -2,14 +2,19 @@
[alias] analysing function: main
[alias] analysing instruction: st_1_t x = {.a = 0, .b = 1};
[alias] May-aliases at the end of instruction: st_1_t x = {.a = 0, .b = 1};
+ <none>
[alias] analysing instruction: st_2_t y = {.a = 3, .c = 4};
[alias] May-aliases at the end of instruction: st_2_t y = {.a = 3, .c = 4};
+ <none>
[alias] analysing instruction: st_1_t *p_x = & x;
[alias] May-aliases at the end of instruction: st_1_t *p_x = & x;
+ <none>
[alias] analysing instruction: st_2_t *p_y = & y;
[alias] May-aliases at the end of instruction: st_2_t *p_y = & y;
+ <none>
[alias] analysing instruction: p_x->a = 3;
[alias] May-aliases at the end of instruction: p_x->a = 3;
+ <none>
[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 *
diff --git a/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle
index fcf43a555f05ad715c13fd1f3dce8ef1af1e1876..be92c249a6a4d301225db90be612b1d3d1d190f8 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure2.res.oracle
@@ -2,18 +2,24 @@
[alias] analysing function: main
[alias] analysing instruction: st_1_t x1 = {.a = 0, .b = 1};
[alias] May-aliases at the end of instruction: st_1_t x1 = {.a = 0, .b = 1};
+ <none>
[alias] analysing instruction: st_1_t x2 = {.a = 1, .b = 2};
[alias] May-aliases at the end of instruction: st_1_t x2 = {.a = 1, .b = 2};
+ <none>
[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 *
[alias] May-aliases at the end of instruction: st_2_t y =
{.s = (struct struct_1_t *)(& x1),
.c = 4};
+ <none>
[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 *
[alias] May-aliases at the end of instruction: y.s = (struct struct_1_t *)(& x2);
+ <none>
[alias] analysing instruction: __retres = 0;
[alias] May-aliases at the end of instruction: __retres = 0;
+ <none>
[alias] May-aliases at the end of function main:
+ <none>
diff --git a/src/plugins/alias/tests/offsets/oracle/structure3.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure3.res.oracle
index fb4e83b000e5ab7ea509fcb7b3ad67ba57c7a1fd..cf1fbc3b1b7ca7de1dc455b1bfbf60b9392cdce6 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure3.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure3.res.oracle
@@ -2,8 +2,10 @@
[alias] analysing function: main
[alias] analysing instruction: st_1_t x1 = {.a = 0, .b = 1};
[alias] May-aliases at the end of instruction: st_1_t x1 = {.a = 0, .b = 1};
+ <none>
[alias] analysing instruction: st_1_t x2 = {.a = 1, .b = 2};
[alias] May-aliases at the end of instruction: st_1_t x2 = {.a = 1, .b = 2};
+ <none>
[alias] analysing instruction: st_2_t y1 =
{.s = (struct struct_1_t *)(& x1), .c = 3};
[alias:unsafe-cast] structure3.c:31: Warning:
@@ -11,6 +13,7 @@
[alias] May-aliases at the end of instruction: st_2_t y1 =
{.s = (struct struct_1_t *)(& x1),
.c = 3};
+ <none>
[alias] analysing instruction: st_2_t y2 =
{.s = (struct struct_1_t *)(& x2), .c = 4};
[alias:unsafe-cast] structure3.c:32: Warning:
@@ -18,18 +21,24 @@
[alias] May-aliases at the end of instruction: st_2_t y2 =
{.s = (struct struct_1_t *)(& x2),
.c = 4};
+ <none>
[alias] analysing instruction: st_3_t z = {.t = (struct struct_2_t *)(& y1), .d = 5};
[alias:unsafe-cast] structure3.c:33: Warning:
unsafe cast from st_2_t * to struct struct_2_t *
[alias] May-aliases at the end of instruction: st_3_t z =
{.t = (struct struct_2_t *)(& y1),
.d = 5};
+ <none>
[alias] analysing instruction: z.t = (struct struct_2_t *)(& y2);
[alias:unsafe-cast] structure3.c:35: Warning:
unsafe cast from st_2_t * to struct struct_2_t *
[alias] May-aliases at the end of instruction: z.t = (struct struct_2_t *)(& y2);
+ <none>
[alias] analysing instruction: y1.c = z.d;
[alias] May-aliases at the end of instruction: y1.c = z.d;
+ <none>
[alias] analysing instruction: __retres = 0;
[alias] May-aliases at the end of instruction: __retres = 0;
+ <none>
[alias] May-aliases at the end of function main:
+ <none>
diff --git a/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
index 18808616aed443ca0757d66a35df2dce7c6c664a..bf3fc7084f7821d19ff0e9b677bc63f42495533f 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure4.res.oracle
@@ -74,14 +74,19 @@
[alias] analysing function: main
[alias] analysing instruction: st_1_t x1 = {.a = 0, .b = 1};
[alias] May-aliases at the end of instruction: st_1_t x1 = {.a = 0, .b = 1};
+ <none>
[alias] analysing instruction: st_1_t x2 = {.a = 1, .b = 2};
[alias] May-aliases at the end of instruction: st_1_t x2 = {.a = 1, .b = 2};
+ <none>
[alias] analysing instruction: st_1_t *y1 = malloc(sizeof(st_1_t));
[alias] May-aliases at the end of instruction: st_1_t *y1 = malloc(sizeof(st_1_t));
+ <none>
[alias] analysing instruction: st_2_t *z = malloc(sizeof(st_2_t));
[alias] May-aliases at the end of instruction: st_2_t *z = malloc(sizeof(st_2_t));
+ <none>
[alias] analysing instruction: y1 = & x1;
[alias] May-aliases at the end of instruction: y1 = & x1;
+ <none>
[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 *
diff --git a/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle b/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
index 360201fc53f81a2a8c7d797316d6567c327a5b6c..135933b7245a0f248da15f28478b4eb927b0c549 100644
--- a/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
+++ b/src/plugins/alias/tests/offsets/oracle/structure5.res.oracle
@@ -74,20 +74,28 @@
[alias] analysing function: main
[alias] analysing instruction: st_1_t x1 = {.a = 0, .b = 1};
[alias] May-aliases at the end of instruction: st_1_t x1 = {.a = 0, .b = 1};
+ <none>
[alias] analysing instruction: st_1_t x2 = {.a = 1, .b = 2};
[alias] May-aliases at the end of instruction: st_1_t x2 = {.a = 1, .b = 2};
+ <none>
[alias] analysing instruction: st_1_t *y1 = malloc(sizeof(st_1_t));
[alias] May-aliases at the end of instruction: st_1_t *y1 = malloc(sizeof(st_1_t));
+ <none>
[alias] analysing instruction: st_2_t *z = malloc(sizeof(st_2_t));
[alias] May-aliases at the end of instruction: st_2_t *z = malloc(sizeof(st_2_t));
+ <none>
[alias] analysing instruction: st_3_t *t = malloc(sizeof(st_3_t));
[alias] May-aliases at the end of instruction: st_3_t *t = malloc(sizeof(st_3_t));
+ <none>
[alias] analysing instruction: int *a = malloc(sizeof(int));
[alias] May-aliases at the end of instruction: int *a = malloc(sizeof(int));
+ <none>
[alias] analysing instruction: *a = 0;
[alias] May-aliases at the end of instruction: *a = 0;
+ <none>
[alias] analysing instruction: y1 = & x1;
[alias] May-aliases at the end of instruction: y1 = & x1;
+ <none>
[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 *
diff --git a/src/plugins/alias/tests/real_world/oracle/example1.res.oracle b/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
index 0ee124fd94df8c60dd7bdc70eef87bf0715e4d11..5ad479692b0d440ba109f0ae6c0061af3d0eeb7c 100644
--- a/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
+++ b/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
@@ -164,9 +164,12 @@
[alias] analysing function: swap
[alias] analysing instruction: *n = 0;
[alias] May-aliases at the end of instruction: *n = 0;
+ <none>
[alias] analysing instruction: (*n) ++;
[alias] May-aliases at the end of instruction: (*n) ++;
+ <none>
[alias] May-aliases at the end of function swap:
+ <none>
[alias] May-aliases at the end of instruction: swap(tmp->n1);
{x, tmp} are aliased
[alias] analysing instruction: idata = tmp->t2[*(tmp->n2)];
@@ -178,6 +181,7 @@
[alias:no-return] example1.c:29: Warning:
function f1 does not return; analysis may be unsound
[alias] May-aliases at the end of function f1:
+ <none>
[alias] analysing function: f2
[alias] analysing instruction: ty *tmp = x;
[alias] May-aliases at the end of instruction: ty *tmp = x;
@@ -213,6 +217,7 @@
[alias:no-return] example1.c:53: Warning:
function f2 does not return; analysis may be unsound
[alias] May-aliases at the end of function f2:
+ <none>
[alias] analysing function: fabs
[alias] May-aliases at the end of function fabs:
<Bot>
@@ -309,30 +314,43 @@
[alias] analysing function: main
[alias] analysing instruction: a = (ty *)malloc(sizeof(ty));
[alias] May-aliases at the end of instruction: a = (ty *)malloc(sizeof(ty));
+ <none>
[alias] analysing instruction: b = (ty *)malloc(sizeof(ty));
[alias] May-aliases at the end of instruction: b = (ty *)malloc(sizeof(ty));
+ <none>
[alias] analysing instruction: i = 0;
[alias] May-aliases at the end of instruction: i = 0;
+ <none>
[alias] analysing instruction: a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));
[alias] May-aliases at the end of instruction: a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));
+ <none>
[alias] analysing instruction: a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));
[alias] May-aliases at the end of instruction: a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));
+ <none>
[alias] analysing instruction: i ++;
[alias] May-aliases at the end of instruction: i ++;
+ <none>
[alias] analysing instruction: a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));
[alias] May-aliases at the end of instruction: a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));
+ <none>
[alias] analysing instruction: a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));
[alias] May-aliases at the end of instruction: a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));
+ <none>
[alias] analysing instruction: a->n1 = (int *)malloc(sizeof(int));
[alias] May-aliases at the end of instruction: a->n1 = (int *)malloc(sizeof(int));
+ <none>
[alias] analysing instruction: a->n2 = (int *)malloc(sizeof(int));
[alias] May-aliases at the end of instruction: a->n2 = (int *)malloc(sizeof(int));
+ <none>
[alias] analysing instruction: *(a->n1) = 1;
[alias] May-aliases at the end of instruction: *(a->n1) = 1;
+ <none>
[alias] analysing instruction: *(a->n2) = 1;
[alias] May-aliases at the end of instruction: *(a->n2) = 1;
+ <none>
[alias] analysing instruction: i = 0;
[alias] May-aliases at the end of instruction: i = 0;
+ <none>
[alias] analysing instruction: b->t1[i] = a->t1[i];
[alias] May-aliases at the end of instruction: b->t1[i] = a->t1[i];
{a->t1[0], b->t1[0]} are aliased
@@ -514,6 +532,7 @@
<Bot>
[alias] analysing function: swap
[alias] May-aliases at the end of function swap:
+ <none>
[alias] analysing function: system
[alias] May-aliases at the end of function system:
<Bot>
diff --git a/src/plugins/alias/tests/real_world/oracle/example2.res.oracle b/src/plugins/alias/tests/real_world/oracle/example2.res.oracle
index 9898f2f3a73ec2aebe5f4f7bf9ba3670a2fe1f7a..a0a1d67eef9efa46a6856491001f57e866685d0a 100644
--- a/src/plugins/alias/tests/real_world/oracle/example2.res.oracle
+++ b/src/plugins/alias/tests/real_world/oracle/example2.res.oracle
@@ -167,9 +167,12 @@
[alias] analysing function: swap
[alias] analysing instruction: *n = 0;
[alias] May-aliases at the end of instruction: *n = 0;
+ <none>
[alias] analysing instruction: (*n) ++;
[alias] May-aliases at the end of instruction: (*n) ++;
+ <none>
[alias] May-aliases at the end of function swap:
+ <none>
[alias] May-aliases at the end of instruction: swap(tmp->n1);
{x, tmp} are aliased
[alias] analysing instruction: i ++;
@@ -327,30 +330,43 @@
[alias] analysing function: main
[alias] analysing instruction: a = (ty *)malloc(sizeof(ty));
[alias] May-aliases at the end of instruction: a = (ty *)malloc(sizeof(ty));
+ <none>
[alias] analysing instruction: b = (ty *)malloc(sizeof(ty));
[alias] May-aliases at the end of instruction: b = (ty *)malloc(sizeof(ty));
+ <none>
[alias] analysing instruction: i = 0;
[alias] May-aliases at the end of instruction: i = 0;
+ <none>
[alias] analysing instruction: a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));
[alias] May-aliases at the end of instruction: a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));
+ <none>
[alias] analysing instruction: a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));
[alias] May-aliases at the end of instruction: a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));
+ <none>
[alias] analysing instruction: i ++;
[alias] May-aliases at the end of instruction: i ++;
+ <none>
[alias] analysing instruction: a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));
[alias] May-aliases at the end of instruction: a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));
+ <none>
[alias] analysing instruction: a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));
[alias] May-aliases at the end of instruction: a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));
+ <none>
[alias] analysing instruction: a->n1 = (int *)malloc(sizeof(int));
[alias] May-aliases at the end of instruction: a->n1 = (int *)malloc(sizeof(int));
+ <none>
[alias] analysing instruction: a->n2 = (int *)malloc(sizeof(int));
[alias] May-aliases at the end of instruction: a->n2 = (int *)malloc(sizeof(int));
+ <none>
[alias] analysing instruction: *(a->n1) = 1;
[alias] May-aliases at the end of instruction: *(a->n1) = 1;
+ <none>
[alias] analysing instruction: *(a->n2) = 1;
[alias] May-aliases at the end of instruction: *(a->n2) = 1;
+ <none>
[alias] analysing instruction: i = 0;
[alias] May-aliases at the end of instruction: i = 0;
+ <none>
[alias] analysing instruction: b->t1[i] = a->t1[i];
[alias] May-aliases at the end of instruction: b->t1[i] = a->t1[i];
{a->t1[0], b->t1[0]} are aliased
@@ -532,6 +548,7 @@
<Bot>
[alias] analysing function: swap
[alias] May-aliases at the end of function swap:
+ <none>
[alias] analysing function: system
[alias] May-aliases at the end of function system:
<Bot>