From 795627b7832ee2f2111454fc176fe7cbfba018dd Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Thu, 6 Apr 2023 18:15:24 +0200
Subject: [PATCH] [alias] be explicit about empty alias sets
---
src/plugins/alias/abstract_state.ml | 4 +++-
.../tests/basic/oracle/assignment1.res.oracle | 4 ++++
.../tests/basic/oracle/assignment2.res.oracle | 4 ++++
.../tests/basic/oracle/assignment3.res.oracle | 4 ++++
.../tests/basic/oracle/assignment4.res.oracle | 4 ++++
.../tests/basic/oracle/assignment5.res.oracle | 4 ++++
.../alias/tests/basic/oracle/cast1.res.oracle | 4 ++++
.../basic/oracle/conditional1.res.oracle | 3 +++
.../tests/basic/oracle/function1.res.oracle | 6 ++++++
.../tests/basic/oracle/function2.res.oracle | 11 +++++++++++
.../tests/basic/oracle/function3.res.oracle | 4 ++++
.../tests/basic/oracle/function4.res.oracle | 4 ++++
.../tests/basic/oracle/function5.res.oracle | 4 ++++
.../tests/basic/oracle/globctr.res.oracle | 9 +++++++++
.../alias/tests/basic/oracle/loop.res.oracle | 8 ++++++++
.../tests/basic/oracle/steensgaard.res.oracle | 1 +
.../tests/basic/oracle/switch1.res.oracle | 5 +++++
.../tests/basic/oracle/switch2.res.oracle | 5 +++++
.../tests/basic/oracle/while_for1.res.oracle | 7 +++++++
.../tests/basic/oracle/while_for2.res.oracle | 3 +++
.../tests/basic/oracle/while_for3.res.oracle | 4 ++++
.../fixed_bugs/oracle/union_vmap.res.oracle | 4 ++++
.../tests/offsets/oracle/array1.res.oracle | 4 ++++
.../tests/offsets/oracle/array2.res.oracle | 6 ++++++
.../tests/offsets/oracle/array3.res.oracle | 3 +++
.../tests/offsets/oracle/collapse1.res.oracle | 10 ++++++++++
.../tests/offsets/oracle/collapse2.res.oracle | 8 ++++++++
.../tests/offsets/oracle/collapse3.res.oracle | 8 ++++++++
.../tests/offsets/oracle/nested1.res.oracle | 11 +++++++++++
.../tests/offsets/oracle/nested2.res.oracle | 8 ++++++++
.../offsets/oracle/structure1.res.oracle | 5 +++++
.../offsets/oracle/structure2.res.oracle | 6 ++++++
.../offsets/oracle/structure3.res.oracle | 9 +++++++++
.../offsets/oracle/structure4.res.oracle | 5 +++++
.../offsets/oracle/structure5.res.oracle | 8 ++++++++
.../real_world/oracle/example1.res.oracle | 19 +++++++++++++++++++
.../real_world/oracle/example2.res.oracle | 17 +++++++++++++++++
37 files changed, 232 insertions(+), 1 deletion(-)
diff --git a/src/plugins/alias/abstract_state.ml b/src/plugins/alias/abstract_state.ml
index 1fb606d3893..1dfce6cfd29 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 d9c4c504573..35feff272aa 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 6438b8a5e18..0752c920750 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 198c7753a2f..7c4c81fba2c 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 7c1c4f02990..511454fecf5 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 f54e8937508..694d63e0307 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 c568a7791dc..66df1e6f0e9 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 a2bcc51e7ec..9b38a767a32 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 5856da9a875..0158b97495e 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 e2730b111c1..48b64d74e02 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 1ca2d7367e8..d61cfa89c47 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 0fc294049b7..ee692419b85 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 8510888b059..c496bb34f2e 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 d18490d7bac..17c4dd29081 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 450aa956b42..1d41d498ffd 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 04c2159b213..62e77694dee 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 b6e49fd381f..c1202c16d1d 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 d9a802df5fd..0a1a041476a 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 062e40c3dbc..7115798d025 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 0f4e8cd0888..6c08aec861c 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 f7d9211bc9c..b3c5b194e25 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 d5be4db46ad..57c8847db39 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 9d030dbb3aa..3f8f04ebf18 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 5b40ad5bdd8..d06aacf760b 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 c6b7ce0876b..906a7e049b4 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 f05bf7a178f..6f29399b235 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 c0ff26fc5ba..5aa489b0697 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 d2145438200..cc02a1b6694 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 07c0fc998a1..9e0ad0d28c8 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 ffe8cf311a0..2ca416be7fc 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 bd470dc2d74..ca2b271f23e 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 fcf43a555f0..be92c249a6a 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 fb4e83b000e..cf1fbc3b1b7 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 18808616aed..bf3fc7084f7 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 360201fc53f..135933b7245 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 0ee124fd94d..5ad479692b0 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 9898f2f3a73..a0a1d67eef9 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>
--
GitLab