From 791de41011bbfe69cb33ac96bcb017b9830680e9 Mon Sep 17 00:00:00 2001
From: Tristan Le Gall <tristan.le-gall@cea.fr>
Date: Fri, 23 Dec 2022 22:19:44 +0100
Subject: [PATCH] [alias] added tests
---
src/plugins/alias/abstract_state.ml | 10 ++++++----
src/plugins/alias/abstract_state.mli | 7 +------
src/plugins/alias/tests/basic/assignment1.c | 12 ++++++++++++
src/plugins/alias/tests/basic/assignment2.c | 10 ++++++++++
src/plugins/alias/tests/basic/assignment3.c | 9 +++++++++
.../alias/tests/basic/oracle/assignment1.err.oracle | 0
.../alias/tests/basic/oracle/assignment1.res.oracle | 0
.../alias/tests/basic/oracle/assignment2.err.oracle | 0
.../alias/tests/basic/oracle/assignment2.res.oracle | 0
.../alias/tests/basic/oracle/assignment3.err.oracle | 0
.../alias/tests/basic/oracle/assignment3.res.oracle | 0
11 files changed, 38 insertions(+), 10 deletions(-)
create mode 100644 src/plugins/alias/tests/basic/assignment1.c
create mode 100644 src/plugins/alias/tests/basic/assignment2.c
create mode 100644 src/plugins/alias/tests/basic/assignment3.c
create mode 100644 src/plugins/alias/tests/basic/oracle/assignment1.err.oracle
create mode 100644 src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
create mode 100644 src/plugins/alias/tests/basic/oracle/assignment2.err.oracle
create mode 100644 src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
create mode 100644 src/plugins/alias/tests/basic/oracle/assignment3.err.oracle
create mode 100644 src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
diff --git a/src/plugins/alias/abstract_state.ml b/src/plugins/alias/abstract_state.ml
index 9af3dced6b0..411a14dc38f 100644
--- a/src/plugins/alias/abstract_state.ml
+++ b/src/plugins/alias/abstract_state.ml
@@ -330,9 +330,11 @@ let assignment_x_y (a:t) (x:lval) (y:lval) : t =
let assignment_x_addr_y (a:t) (x:lval) (y:lval) : t=
let v1, a = find_or_create_vertex x a in
let list_v2, a = addr_of y a in
- match list_v2 with
- [v2] -> join a v1 v2
- | _ -> failwith "assignment_x_addr_y not implemented"
+ List.fold_left
+ (fun a_acc v2 -> join a_acc v1 v2)
+ a
+ list_v2
+(* TODO is that correct ?*)
(* assignment x = *y *)
@@ -496,7 +498,7 @@ let initial_value :t =
{graph = G.empty; pending = VMap.empty ; lmap = LMap.empty; vmap = VMap.empty; cmpt = 0}
(** a type for summaries of functions *)
-type summary = t (* final type may be different *)
+type summary = float (* final type may be different *)
diff --git a/src/plugins/alias/abstract_state.mli b/src/plugins/alias/abstract_state.mli
index 2ad7d6c10f4..06744a48102 100644
--- a/src/plugins/alias/abstract_state.mli
+++ b/src/plugins/alias/abstract_state.mli
@@ -46,14 +46,9 @@ val pretty : ?debug:bool -> Format.formatter -> t -> unit
(** dot printer *)
val print_dot : string -> t -> unit
-(** finds the vertex corresponding to a lval *)
+(** finds the vertex corresponding to a lval. May raise Not_found *)
val find_vertex : lval -> t -> G.V.t
-(** finds the vertex corresponding to a lval; if not present creates
- the corresponding node in the graph; the (maybe modifed) graph is
- returned as well *)
-val find_or_create_vertex : lval -> t -> G.V.t * G.t
-
(** Functions for Steensgaard's algorithm *)
val join : t -> G.V.t -> G.V.t -> t
diff --git a/src/plugins/alias/tests/basic/assignment1.c b/src/plugins/alias/tests/basic/assignment1.c
new file mode 100644
index 00000000000..41d177f99d6
--- /dev/null
+++ b/src/plugins/alias/tests/basic/assignment1.c
@@ -0,0 +1,12 @@
+// single pointer assignment
+
+int main () {
+
+ int *a, *b, *c, *d, e;
+ a = b;
+ b = c;
+ *a = 4;
+ *c = e;
+ a = d ;
+ return 0;
+}
diff --git a/src/plugins/alias/tests/basic/assignment2.c b/src/plugins/alias/tests/basic/assignment2.c
new file mode 100644
index 00000000000..dd313a5e763
--- /dev/null
+++ b/src/plugins/alias/tests/basic/assignment2.c
@@ -0,0 +1,10 @@
+// double pointer assignment
+
+int main () {
+
+ int **a, *b, **c, *d;
+ *a = b;
+ *c = d;
+ a = c;
+ return 0;
+}
diff --git a/src/plugins/alias/tests/basic/assignment3.c b/src/plugins/alias/tests/basic/assignment3.c
new file mode 100644
index 00000000000..f38e06e7fb0
--- /dev/null
+++ b/src/plugins/alias/tests/basic/assignment3.c
@@ -0,0 +1,9 @@
+// address assignment
+
+int main () {
+
+ int *a, b, *c;
+ a = &b;
+ *c = b;
+ return 0;
+}
diff --git a/src/plugins/alias/tests/basic/oracle/assignment1.err.oracle b/src/plugins/alias/tests/basic/oracle/assignment1.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/alias/tests/basic/oracle/assignment2.err.oracle b/src/plugins/alias/tests/basic/oracle/assignment2.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/alias/tests/basic/oracle/assignment3.err.oracle b/src/plugins/alias/tests/basic/oracle/assignment3.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
--
GitLab