From ee60a105a4ae36b8adf1f14a5288ff3b0cd8459d Mon Sep 17 00:00:00 2001
From: Tristan Le Gall <tristan.le-gall@cea.fr>
Date: Wed, 18 Jan 2023 11:32:58 +0100
Subject: [PATCH] [alias] functions still WIP
---
src/plugins/alias/analysis.ml | 6 +-
.../tests/basic/oracle/assignment1.res.oracle | 19 +++----
.../tests/basic/oracle/assignment2.res.oracle | 12 ++--
.../tests/basic/oracle/assignment3.res.oracle | 8 +--
.../alias/tests/basic/oracle/cast1.res.oracle | 10 ++--
.../basic/oracle/conditional1.res.oracle | 14 ++---
.../tests/basic/oracle/function1.res.oracle | 32 ++++++-----
.../tests/basic/oracle/while_for1.res.oracle | 56 +++++++++----------
8 files changed, 77 insertions(+), 80 deletions(-)
diff --git a/src/plugins/alias/analysis.ml b/src/plugins/alias/analysis.ml
index b3c4f07ffca..6ef94e63156 100644
--- a/src/plugins/alias/analysis.ml
+++ b/src/plugins/alias/analysis.ml
@@ -234,7 +234,7 @@ let doFunction (kf:kernel_function) =
let final_state : Abstract_state.t option =
try Stmt_table.find return_stmt
with
- Not_found -> failwith "Houston, we have a problem"
+ Not_found -> Options.abort "Houston, we have a problem: %a has no return statement" Kernel_function.pretty kf
in
let summary: Abstract_state.summary =
Abstract_state.make_summary final_state kf
@@ -244,8 +244,8 @@ let doFunction (kf:kernel_function) =
else
begin
(* summary by default *)
- Options.warning "Function %a has no definition (summary empty)"
- Kernel_function.pretty kf;
+ (* Options.warning "Function %a has no definition (summary empty)"
+ * Kernel_function.pretty kf; *)
let summary: Abstract_state.summary =
Abstract_state.make_summary (Some Abstract_state.initial_value) kf
in
diff --git a/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
index 5265a9c8a9a..0fe11e42da1 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
@@ -1,37 +1,36 @@
[kernel] Parsing assignment1.c (with preprocessing)
[alias] Parsing done
[alias] Functions done
-After statement a = b; :
+Before statement a = b; :
<list of may-alias>
-{ a; b } are aliased
<end of list>
-After statement b = c; :
+Before statement b = c; :
<list of may-alias>
-{ a; b; c } are aliased
+{ a; b } are aliased
<end of list>
-After statement *a = 4; :
+Before statement *a = 4; :
<list of may-alias>
{ a; b; c } are aliased
<end of list>
-After statement *c = e; :
+Before statement *c = e; :
<list of may-alias>
{ a; b; c } are aliased
<end of list>
-After statement a = d; :
+Before statement a = d; :
<list of may-alias>
-{ a; b; c; d } are aliased
+{ a; b; c } are aliased
<end of list>
-After statement __retres = 0; :
+Before statement __retres = 0; :
<list of may-alias>
{ a; b; c; d } are aliased
<end of list>
-After statement return __retres; :
+Before statement return __retres; :
<list of may-alias>
{ a; b; c; d } are aliased
<end of list>
diff --git a/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
index aaabce7aebc..232301b92d3 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
@@ -1,27 +1,25 @@
[kernel] Parsing assignment2.c (with preprocessing)
[alias] Parsing done
[alias] Functions done
-After statement *a = b; :
+Before statement *a = b; :
<list of may-alias>
<end of list>
-After statement *c = d; :
+Before statement *c = d; :
<list of may-alias>
<end of list>
-After statement a = c; :
+Before statement a = c; :
<list of may-alias>
-{ a; c } are aliased
-{ b; d } are aliased
<end of list>
-After statement __retres = 0; :
+Before statement __retres = 0; :
<list of may-alias>
{ a; c } are aliased
{ b; d } are aliased
<end of list>
-After statement return __retres; :
+Before statement return __retres; :
<list of may-alias>
{ a; c } are aliased
{ b; d } 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 97a840081bc..a3e45ebfbfd 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
@@ -1,19 +1,19 @@
[kernel] Parsing assignment3.c (with preprocessing)
[alias] Parsing done
[alias] Functions done
-After statement a = & b; :
+Before statement a = & b; :
<list of may-alias>
<end of list>
-After statement *c = b; :
+Before statement *c = b; :
<list of may-alias>
<end of list>
-After statement __retres = 0; :
+Before statement __retres = 0; :
<list of may-alias>
<end of list>
-After statement return __retres; :
+Before statement return __retres; :
<list of may-alias>
<end of list>
diff --git a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
index 5ce038e47f6..6f0872c16e1 100644
--- a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
@@ -1,24 +1,22 @@
[kernel] Parsing cast1.c (with preprocessing)
[alias] Parsing done
[alias] Functions done
-After statement a = (int *)c; :
+Before statement a = (int *)c; :
<list of may-alias>
-{ a; c } are aliased
<end of list>
-After statement d = (float *)b; :
+Before statement d = (float *)b; :
<list of may-alias>
{ a; c } are aliased
-{ b; d } are aliased
<end of list>
-After statement __retres = 0; :
+Before statement __retres = 0; :
<list of may-alias>
{ a; c } are aliased
{ b; d } are aliased
<end of list>
-After statement return __retres; :
+Before statement return __retres; :
<list of may-alias>
{ a; c } are aliased
{ b; d } are aliased
diff --git a/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle b/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
index 0556445f9b9..5ec54307ed6 100644
--- a/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
@@ -1,31 +1,29 @@
[kernel] Parsing conditional1.c (with preprocessing)
[alias] Parsing done
[alias] Functions done
-After statement if (a) a = b; else a = c; :
+Before statement if (a) a = b; else a = c; :
<list of may-alias>
<end of list>
-After statement a = b; :
+Before statement a = b; :
<list of may-alias>
-{ a; b } are aliased
<end of list>
-After statement a = c; :
+Before statement a = c; :
<list of may-alias>
-{ a; c } are aliased
<end of list>
-After statement *a = 4; :
+Before statement *a = 4; :
<list of may-alias>
{ a; b } are aliased
<end of list>
-After statement __retres = 0; :
+Before statement __retres = 0; :
<list of may-alias>
{ a; b } are aliased
<end of list>
-After statement return __retres; :
+Before statement return __retres; :
<list of may-alias>
{ a; b } are aliased
<end of list>
diff --git a/src/plugins/alias/tests/basic/oracle/function1.res.oracle b/src/plugins/alias/tests/basic/oracle/function1.res.oracle
index 2506c255730..46b84b75a40 100644
--- a/src/plugins/alias/tests/basic/oracle/function1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/function1.res.oracle
@@ -1,44 +1,48 @@
[kernel] Parsing function1.c (with preprocessing)
[alias] Parsing done
-[alias] Skiping swap(a,b); (summary not found)
-[alias] Skiping swap(a,b); (summary not found)
-[alias] Skiping swap(c,d); (summary not found)
-[alias] Skiping swap(c,d); (summary not found)
[alias] Functions done
-After statement z = x; :
+Before statement z = x; :
<list of may-alias>
-{ x; z } are aliased
<end of list>
-After statement x = y; :
+Before statement z = x; :
<list of may-alias>
-{ x; y; z } are aliased
<end of list>
-After statement y = z; :
+Before statement x = y; :
+ <list of may-alias>
+{ x; z } are aliased
+<end of list>
+
+Before statement y = z; :
<list of may-alias>
{ x; y; z } are aliased
<end of list>
-After statement swap(a,b); :
+Before statement swap(a,b); :
<list of may-alias>
<end of list>
-After statement swap(c,d); :
+Before statement swap(c,d); :
<list of may-alias>
+{ a; b } are aliased
<end of list>
-After statement __retres = 0; :
+Before statement __retres = 0; :
<list of may-alias>
+{ a; b } are aliased
+{ c; d } are aliased
<end of list>
-After statement return; :
+Before statement return; :
<list of may-alias>
{ x; y; z } are aliased
<end of list>
-After statement return __retres; :
+Before statement return __retres; :
<list of may-alias>
+{ a; b } are aliased
+{ c; d } are aliased
<end of list>
[alias] Analysis complete
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 9383a1891db..9d511ac7569 100644
--- a/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
@@ -4,67 +4,67 @@
[alias] Skipping assignment odata[idx] = 0.5 * idata[idx] (not implemented)
[alias] Skipping assignment odata[idx] = 0.5 * idata[idx] (not implemented)
[alias] Functions done
-After statement while (1) {
- idx = 0;
- while (idx < 10) {
- odata[idx] = 0.5 * idata[idx];
- idx ++;
- }
- } :
+Before statement while (1) {
+ idx = 0;
+ while (idx < 10) {
+ odata[idx] = 0.5 * idata[idx];
+ idx ++;
+ }
+ } :
<list of may-alias>
<end of list>
-After statement idx = 0;
- while (idx < 10) {
- odata[idx] = 0.5 * idata[idx];
- idx ++;
- } :
+Before statement idx = 0;
+ while (idx < 10) {
+ odata[idx] = 0.5 * idata[idx];
+ idx ++;
+ } :
<list of may-alias>
<end of list>
-After statement idx = 0; :
+Before statement idx = 0; :
<list of may-alias>
<end of list>
-After statement idx = 0; :
+Before statement idx = 0; :
<list of may-alias>
<end of list>
-After statement while (idx < 10) {
- odata[idx] = 0.5 * idata[idx];
- idx ++;
- } :
+Before statement while (idx < 10) {
+ odata[idx] = 0.5 * idata[idx];
+ idx ++;
+ } :
<list of may-alias>
<end of list>
-After statement while (idx < 10) {
- odata[idx] = 0.5 * idata[idx];
- idx ++;
- } :
+Before statement while (idx < 10) {
+ odata[idx] = 0.5 * idata[idx];
+ idx ++;
+ } :
<list of may-alias>
<end of list>
-After statement if (! (idx < 10)) break; :
+Before statement if (! (idx < 10)) break; :
<list of may-alias>
<end of list>
-After statement break; :
+Before statement break; :
<list of may-alias>
<end of list>
-After statement odata[idx] = 0.5 * idata[idx]; :
+Before statement odata[idx] = 0.5 * idata[idx]; :
<list of may-alias>
<end of list>
-After statement odata[idx] = 0.5 * idata[idx]; :
+Before statement odata[idx] = 0.5 * idata[idx]; :
<list of may-alias>
<end of list>
-After statement odata[idx] = 0.5 * idata[idx]; :
+Before statement odata[idx] = 0.5 * idata[idx]; :
<list of may-alias>
<end of list>
-After statement idx ++; :
+Before statement idx ++; :
<list of may-alias>
<end of list>
--
GitLab