From 51abcafbb8efb50c78f3325aed1959bade93649d Mon Sep 17 00:00:00 2001
From: Tristan Le Gall <tristan.le-gall@cea.fr>
Date: Sat, 31 Dec 2022 10:47:54 +0100
Subject: [PATCH] [alias] adding functions for arithmetic operation analysis

---
 src/plugins/alias/abstract_state.ml           |  19 +
 src/plugins/alias/abstract_state.mli          |   5 +
 src/plugins/alias/analysis.ml                 |  13 +-
 .../tests/basic/oracle/assignment1.res.oracle |  37 +-
 .../tests/basic/oracle/assignment2.res.oracle |  27 +-
 .../tests/basic/oracle/assignment3.res.oracle |  22 +-
 .../alias/tests/basic/oracle/cast1.res.oracle |  22 +-
 .../basic/oracle/conditional1.res.oracle      |  32 +-
 .../tests/basic/oracle/while_for1.res.oracle  |  58 +++
 src/plugins/alias/tests/basic/while_for1.c    |  16 +
 .../real_world/oracle/example1.res.oracle     | 455 ++++++++++--------
 11 files changed, 448 insertions(+), 258 deletions(-)
 create mode 100644 src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
 create mode 100644 src/plugins/alias/tests/basic/while_for1.c

diff --git a/src/plugins/alias/abstract_state.ml b/src/plugins/alias/abstract_state.ml
index 267d5afe1a8..9cb243cc4ac 100644
--- a/src/plugins/alias/abstract_state.ml
+++ b/src/plugins/alias/abstract_state.ml
@@ -507,6 +507,25 @@ let union  (a1:t) (a2:t) :t =
 let initial_value :t =
   {graph = G.empty; pending = VMap.empty ; lmap = LMap.empty; vmap = VMap.empty; cmpt = 0}
 
+
+let make_top (x:t) : t =
+  if x.graph = G.empty
+  then x
+  else
+    let g = G.add_edge (G.add_vertex G.empty 0) 0 0 in
+    (* collect all lval of the initial set *)
+    let set_lv = ref LSet.empty in
+    let lmap =
+      LMap.mapi
+        (fun lv _ -> set_lv := LSet.add lv !set_lv ; 0)
+        x.lmap
+    in
+    let vmap =
+      VMap.add 0 !set_lv VMap.empty
+    in
+    let p = VMap.add 0 VSet.empty VMap.empty in
+    {graph = g ; pending = p ; lmap = lmap ; vmap = vmap ; cmpt = 1}
+
 (** a type for summaries of functions *)
 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 7434ccee56f..8e25aa9ea12 100644
--- a/src/plugins/alias/abstract_state.mli
+++ b/src/plugins/alias/abstract_state.mli
@@ -83,5 +83,10 @@ val union : t -> t -> t
 (** empty graph *)
 val initial_value : t
 
+(** make_top merge all nodes of the graph; the resulting graph has
+   only 1 vertex, 1 edge (loop); every lval of the origial graph are
+   associated to this vertex *)
+val make_top : t -> t
+
 (** Type denoting summaries of functions *)
 type summary
diff --git a/src/plugins/alias/analysis.ml b/src/plugins/alias/analysis.ml
index 02d239da4fd..90133d62fe9 100644
--- a/src/plugins/alias/analysis.ml
+++ b/src/plugins/alias/analysis.ml
@@ -47,9 +47,9 @@ module Make_table(H: Hashtbl.S)(V: sig type t val size :int end) : InternalTable
   let add = H.add tbl
   let find = H.find tbl
   let pretty fmt print_key print_value =
-    Format.fprintf fmt "[@[<hov 2>";
-    H.iter (fun k v -> Format.fprintf fmt "(%a -> %a)@." print_key k print_value v) tbl;
-    Format.fprintf fmt "@]]@."
+    Format.fprintf fmt "@[<hov 2>";
+    H.iter (fun k v -> Format.fprintf fmt "After statement %a :@. @[<2>%a@] @." print_key k print_value v) tbl;
+    Format.fprintf fmt "@]@."
   let clear () = H.clear tbl
 end
 
@@ -110,6 +110,13 @@ struct
     | (_, (Var _, NoOffset), SizeOfStr _) -> a
     | (_, (Var _, NoOffset), AlignOf _) -> a
     | (_, (Var _, NoOffset), AlignOfE _) -> a
+    (* arithmetic operations: either do nothing (normal arithmetic) or returns top (pointer arithmetic) *)
+    | (Some a, (Var _, NoOffset), UnOp (_, _,tt)) ->
+       begin
+         match tt with
+           TPtr _ -> Options.warning "" ; Some (Abstract_state.make_top a)
+         | _ -> Some a 
+       end
     (* cast : TODO check type *)
     | (_, _ , CastE (_,exp)) -> do_assignment a lv exp
     | (Some a, (Var v1, NoOffset), AddrOf lv2) ->
diff --git a/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
index 84722b55d8e..d58abf402f9 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment1.res.oracle
@@ -1,33 +1,40 @@
 [kernel] Parsing assignment1.c (with preprocessing)
 [alias] Parsing done
 [alias] Functions done
-[(a = b; -> <list of may-alias>
+After statement a = b; :
+ <list of may-alias>
 { a; b } are aliased
 <end of list>
-)
-(b = c; -> <list of may-alias>
+ 
+After statement b = c; :
+ <list of may-alias>
 { a; b; c } are aliased
 <end of list>
-)
-(*a = 4; -> <list of may-alias>
+ 
+After statement *a = 4; :
+ <list of may-alias>
 { a; b; c } are aliased
 <end of list>
-)
-(*c = e; -> <list of may-alias>
+ 
+After statement *c = e; :
+ <list of may-alias>
 { a; b; c } are aliased
 <end of list>
-)
-(a = d; -> <list of may-alias>
+ 
+After statement a = d; :
+ <list of may-alias>
 { a; b; c; d } are aliased
 <end of list>
-)
-(__retres = 0; -> <list of may-alias>
+ 
+After statement __retres = 0; :
+ <list of may-alias>
 { a; b; c; d } are aliased
 <end of list>
-)
-(return __retres; -> <list of may-alias>
+ 
+After statement return __retres; :
+ <list of may-alias>
 { a; b; c; d } are aliased
 <end of list>
-)
-]
+ 
+
 [alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
index 28a43067cab..c84a067cd85 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment2.res.oracle
@@ -1,26 +1,31 @@
 [kernel] Parsing assignment2.c (with preprocessing)
 [alias] Parsing done
 [alias] Functions done
-[(*a = b; -> <list of may-alias>
+After statement *a = b; :
+ <list of may-alias>
 <end of list>
-)
-(*c = d; -> <list of may-alias>
+ 
+After statement *c = d; :
+ <list of may-alias>
 <end of list>
-)
-(a = c; -> <list of may-alias>
+ 
+After statement a = c; :
+ <list of may-alias>
 { a; c } are aliased
 { b; d } are aliased
 <end of list>
-)
-(__retres = 0; -> <list of may-alias>
+ 
+After statement __retres = 0; :
+ <list of may-alias>
 { a; c } are aliased
 { b; d } are aliased
 <end of list>
-)
-(return __retres; -> <list of may-alias>
+ 
+After statement return __retres; :
+ <list of may-alias>
 { a; c } are aliased
 { b; d } are aliased
 <end of list>
-)
-]
+ 
+
 [alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle b/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
index 57188563342..0561d9e9ab9 100644
--- a/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/assignment3.res.oracle
@@ -1,17 +1,21 @@
 [kernel] Parsing assignment3.c (with preprocessing)
 [alias] Parsing done
 [alias] Functions done
-[(a = & b; -> <list of may-alias>
+After statement a = & b; :
+ <list of may-alias>
 <end of list>
-)
-(*c = b; -> <list of may-alias>
+ 
+After statement *c = b; :
+ <list of may-alias>
 <end of list>
-)
-(__retres = 0; -> <list of may-alias>
+ 
+After statement __retres = 0; :
+ <list of may-alias>
 <end of list>
-)
-(return __retres; -> <list of may-alias>
+ 
+After statement return __retres; :
+ <list of may-alias>
 <end of list>
-)
-]
+ 
+
 [alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
index 9cddb6d9596..c695eede8c7 100644
--- a/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/cast1.res.oracle
@@ -1,24 +1,28 @@
 [kernel] Parsing cast1.c (with preprocessing)
 [alias] Parsing done
 [alias] Functions done
-[(a = (int *)c; -> <list of may-alias>
+After statement a = (int *)c; :
+ <list of may-alias>
 { a; c } are aliased
 <end of list>
-)
-(d = (float *)b; -> <list of may-alias>
+ 
+After statement d = (float *)b; :
+ <list of may-alias>
 { a; c } are aliased
 { b; d } are aliased
 <end of list>
-)
-(__retres = 0; -> <list of may-alias>
+ 
+After statement __retres = 0; :
+ <list of may-alias>
 { a; c } are aliased
 { b; d } are aliased
 <end of list>
-)
-(return __retres; -> <list of may-alias>
+ 
+After statement return __retres; :
+ <list of may-alias>
 { a; c } are aliased
 { b; d } are aliased
 <end of list>
-)
-]
+ 
+
 [alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle b/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
index 467e542ed60..562ababaeb9 100644
--- a/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/conditional1.res.oracle
@@ -1,28 +1,34 @@
 [kernel] Parsing conditional1.c (with preprocessing)
 [alias] Parsing done
 [alias] Functions done
-[(if (a) a = b; else a = c; -> <list of may-alias>
+After statement if (a) a = b; else a = c; :
+ <list of may-alias>
 <end of list>
-)
-(a = b; -> <list of may-alias>
+ 
+After statement a = b; :
+ <list of may-alias>
 { a; b } are aliased
 <end of list>
-)
-(a = c; -> <list of may-alias>
+ 
+After statement a = c; :
+ <list of may-alias>
 { a; c } are aliased
 <end of list>
-)
-(*a = 4; -> <list of may-alias>
+ 
+After statement *a = 4; :
+ <list of may-alias>
 { a; b; c } are aliased
 <end of list>
-)
-(__retres = 0; -> <list of may-alias>
+ 
+After statement __retres = 0; :
+ <list of may-alias>
 { a; b; c } are aliased
 <end of list>
-)
-(return __retres; -> <list of may-alias>
+ 
+After statement return __retres; :
+ <list of may-alias>
 { a; b; c } 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
new file mode 100644
index 00000000000..1caec764e7f
--- /dev/null
+++ b/src/plugins/alias/tests/basic/oracle/while_for1.res.oracle
@@ -0,0 +1,58 @@
+[kernel] Parsing while_for1.c (with preprocessing)
+[alias] Parsing done
+[alias] Skipping assignment odata[idx] = 0.5 * idata[idx] (not implemented)
+[alias] Skipping assignment odata[idx] = 0.5 * idata[idx] (not implemented)
+[alias] Skipping assignment idx = idx + 1 (not implemented)
+[alias] Skipping assignment idx = idx + 1 (not implemented)
+[alias] Functions done
+After 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 ++;
+                } :
+ <list of may-alias>
+<end of list>
+ 
+After statement idx = 0; :
+ <list of may-alias>
+<end of list>
+ 
+After statement while (idx < 10) {
+                  odata[idx] = 0.5 * idata[idx];
+                  idx ++;
+                } :
+ <list of may-alias>
+<end of list>
+ 
+After statement if (! (idx < 10)) break; :
+ <list of may-alias>
+<end of list>
+ 
+After statement break; :
+ <list of may-alias>
+<end of list>
+ 
+After statement odata[idx] = 0.5 * idata[idx]; :
+ <list of may-alias>
+<end of list>
+ 
+After statement odata[idx] = 0.5 * idata[idx]; :
+ <list of may-alias>
+<end of list>
+ 
+After statement idx ++; :
+ <list of may-alias>
+<end of list>
+ 
+
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/basic/while_for1.c b/src/plugins/alias/tests/basic/while_for1.c
new file mode 100644
index 00000000000..f4f11923afb
--- /dev/null
+++ b/src/plugins/alias/tests/basic/while_for1.c
@@ -0,0 +1,16 @@
+// control structure and arrays
+
+int main ()
+{
+  double idata [10];
+  double odata [10];
+  int idx;
+
+  while (1) {
+
+    for (idx = 0; idx < 10; idx++) {
+      odata[idx] = 0.5*idata[idx];
+    }
+  }
+  return 0;
+}
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 c853457b81c..aadb1b539b6 100644
--- a/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
+++ b/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
@@ -57,289 +57,348 @@
 [alias] Skipping assignment *n = *n + 1 (not implemented)
 [alias] Skipping assignment *n = *n + 1 (not implemented)
 [alias] Functions done
-[(b->t1[i] = a->t1[i]; -> <list of may-alias>
+After statement b->t1[i] = a->t1[i]; :
+ <list of may-alias>
 <end of list>
-)
-(idx = 0; -> <list of may-alias>
+ 
+After statement idx = 0; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(b->t2[i] = a->t2[i]; -> <list of may-alias>
+ 
+After statement b->t2[i] = a->t2[i]; :
+ <list of may-alias>
 <end of list>
-)
-(while (idx < 10) {
-   *(odata + idx) = (double)3 * *(idata + idx) + (double)1;
-   idx ++;
- } -> <list of may-alias>
+ 
+After statement while (idx < 10) {
+                  *(odata + idx) = (double)3 * *(idata + idx) + (double)1;
+                  idx ++;
+                } :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(if (*n == 1) *n = 0; else (*n) ++; -> <list of may-alias>
+ 
+After statement if (*n == 1) *n = 0; else (*n) ++; :
+ <list of may-alias>
 <end of list>
-)
-(i ++; -> <list of may-alias>
+ 
+After statement i ++; :
+ <list of may-alias>
 <end of list>
-)
-(*n = 0; -> <list of may-alias>
+ 
+After statement *n = 0; :
+ <list of may-alias>
 <end of list>
-)
-(b->n1 = a->n1; -> <list of may-alias>
+ 
+After statement b->n1 = a->n1; :
+ <list of may-alias>
 <end of list>
-)
-(if (! (idx < 10)) break; -> <list of may-alias>
+ 
+After statement if (! (idx < 10)) break; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-((*n) ++; -> <list of may-alias>
+ 
+After statement (*n) ++; :
+ <list of may-alias>
 <end of list>
-)
-(b->n2 = a->n2; -> <list of may-alias>
+ 
+After statement b->n2 = a->n2; :
+ <list of may-alias>
 <end of list>
-)
-(break; -> <list of may-alias>
+ 
+After statement break; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(f1(a); -> <list of may-alias>
+ 
+After statement f1(a); :
+ <list of may-alias>
 <end of list>
-)
-(*(odata + idx) = (double)3 * *(idata + idx) + (double)1; -> <list of may-alias>
+ 
+After statement *(odata + idx) = (double)3 * *(idata + idx) + (double)1; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(f2(b); -> <list of may-alias>
+ 
+After statement f2(b); :
+ <list of may-alias>
 <end of list>
-)
-(*(odata + idx) = (double)3 * *(idata + idx) + (double)1; -> <list of may-alias>
+ 
+After statement *(odata + idx) = (double)3 * *(idata + idx) + (double)1; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(__retres = 0; -> <list of may-alias>
+ 
+After statement __retres = 0; :
+ <list of may-alias>
 <end of list>
-)
-(idx ++; -> <list of may-alias>
+ 
+After statement idx ++; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(ty *tmp = x; -> <list of may-alias>
+ 
+After statement ty *tmp = x; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(swap(tmp->n2); -> <list of may-alias>
+ 
+After statement swap(tmp->n2); :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(idata = (double *)malloc((unsigned long)10 * sizeof(double)); -> <list of may-alias>
+ 
+After statement idata = (double *)malloc((unsigned long)10 * sizeof(double)); :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(return; -> <list of may-alias>
-<end of list>
-)
-(while (1) {
-   idata = tmp->t2[*(tmp->n2)];
-   odata = tmp->t1[*(tmp->n1)];
-   idx = 0;
-   while (idx < 10) {
-     {
-       double tmp_1;
-       tmp_1 = sin(*(idata + idx));
-       *(odata + idx) = 0.5 * tmp_1;
-     }
-     idx ++;
-   }
-   swap(tmp->n1);
- } -> <list of may-alias>
+ 
+After statement return; :
+ <list of may-alias>
+<end of list>
+ 
+After statement while (1) {
+                  idata = tmp->t2[*(tmp->n2)];
+                  odata = tmp->t1[*(tmp->n1)];
+                  idx = 0;
+                  while (idx < 10) {
+                    {
+                      double tmp_1;
+                      tmp_1 = sin(*(idata + idx));
+                      *(odata + idx) = 0.5 * tmp_1;
+                    }
+                    idx ++;
+                  }
+                  swap(tmp->n1);
+                } :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(idata = tmp->t2[*(tmp->n2)];
- odata = tmp->t1[*(tmp->n1)];
- idx = 0;
- while (idx < 10) {
-   {
-     double tmp_1;
-     tmp_1 = sin(*(idata + idx));
-     *(odata + idx) = 0.5 * tmp_1;
-   }
-   idx ++;
- }
- swap(tmp->n1); -> <list of may-alias>
+ 
+After statement idata = tmp->t2[*(tmp->n2)];
+                odata = tmp->t1[*(tmp->n1)];
+                idx = 0;
+                while (idx < 10) {
+                  {
+                    double tmp_1;
+                    tmp_1 = sin(*(idata + idx));
+                    *(odata + idx) = 0.5 * tmp_1;
+                  }
+                  idx ++;
+                }
+                swap(tmp->n1); :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(a = (ty *)malloc(sizeof(ty)); -> <list of may-alias>
+ 
+After statement a = (ty *)malloc(sizeof(ty)); :
+ <list of may-alias>
 <end of list>
-)
-(idata = tmp->t2[*(tmp->n2)]; -> <list of may-alias>
+ 
+After statement idata = tmp->t2[*(tmp->n2)]; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(b = (ty *)malloc(sizeof(ty)); -> <list of may-alias>
+ 
+After statement b = (ty *)malloc(sizeof(ty)); :
+ <list of may-alias>
 <end of list>
-)
-(odata = tmp->t1[*(tmp->n1)]; -> <list of may-alias>
+ 
+After statement odata = tmp->t1[*(tmp->n1)]; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(i = 0; -> <list of may-alias>
+ 
+After statement i = 0; :
+ <list of may-alias>
 <end of list>
-)
-(idx = 0; -> <list of may-alias>
+ 
+After statement idx = 0; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(while (i < 2) {
-   a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));
-   a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));
-   i ++;
- } -> <list of may-alias>
-<end of list>
-)
-(while (idx < 10) {
-   {
-     double tmp_1;
-     tmp_1 = sin(*(idata + idx));
-     *(odata + idx) = 0.5 * tmp_1;
-   }
-   idx ++;
- } -> <list of may-alias>
+ 
+After statement while (i < 2) {
+                  a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));
+                  a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double));
+                  i ++;
+                } :
+ <list of may-alias>
+<end of list>
+ 
+After statement while (idx < 10) {
+                  {
+                    double tmp_1;
+                    tmp_1 = sin(*(idata + idx));
+                    *(odata + idx) = 0.5 * tmp_1;
+                  }
+                  idx ++;
+                } :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(return __retres; -> <list of may-alias>
+ 
+After statement return __retres; :
+ <list of may-alias>
 <end of list>
-)
-(if (! (i < 2)) break; -> <list of may-alias>
+ 
+After statement if (! (i < 2)) break; :
+ <list of may-alias>
 <end of list>
-)
-(if (! (idx < 10)) break; -> <list of may-alias>
+ 
+After statement if (! (idx < 10)) break; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(break; -> <list of may-alias>
+ 
+After statement break; :
+ <list of may-alias>
 <end of list>
-)
-(break; -> <list of may-alias>
+ 
+After statement break; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));
- a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); -> 
-<list of may-alias>
-<end of list>
-)
-({
-   double tmp_1;
-   tmp_1 = sin(*(idata + idx));
-   *(odata + idx) = 0.5 * tmp_1;
- } -> <list of may-alias>
+ 
+After statement a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double));
+                a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); :
+ <list of may-alias>
+<end of list>
+ 
+After statement {
+                  double tmp_1;
+                  tmp_1 = sin(*(idata + idx));
+                  *(odata + idx) = 0.5 * tmp_1;
+                } :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); -> 
-<list of may-alias>
+ 
+After statement a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); :
+ <list of may-alias>
 <end of list>
-)
-(tmp_1 = sin(*(idata + idx));
- *(odata + idx) = 0.5 * tmp_1; -> <list of may-alias>
+ 
+After statement tmp_1 = sin(*(idata + idx));
+                *(odata + idx) = 0.5 * tmp_1; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); -> 
-<list of may-alias>
+ 
+After statement a->t2[i] = (double *)malloc((unsigned long)10 * sizeof(double)); :
+ <list of may-alias>
 <end of list>
-)
-(tmp_1 = sin(*(idata + idx)); -> <list of may-alias>
+ 
+After statement tmp_1 = sin(*(idata + idx)); :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(i ++; -> <list of may-alias>
+ 
+After statement i ++; :
+ <list of may-alias>
 <end of list>
-)
-(*(odata + idx) = 0.5 * tmp_1; -> <list of may-alias>
+ 
+After statement *(odata + idx) = 0.5 * tmp_1; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(a->n1 = (int *)malloc(sizeof(int)); -> <list of may-alias>
+ 
+After statement a->n1 = (int *)malloc(sizeof(int)); :
+ <list of may-alias>
 <end of list>
-)
-(idx ++; -> <list of may-alias>
+ 
+After statement idx ++; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(a->n2 = (int *)malloc(sizeof(int)); -> <list of may-alias>
+ 
+After statement a->n2 = (int *)malloc(sizeof(int)); :
+ <list of may-alias>
 <end of list>
-)
-(swap(tmp->n1); -> <list of may-alias>
+ 
+After statement swap(tmp->n1); :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(*(a->n1) = 1; -> <list of may-alias>
+ 
+After statement *(a->n1) = 1; :
+ <list of may-alias>
 <end of list>
-)
-(*(a->n2) = 1; -> <list of may-alias>
+ 
+After statement *(a->n2) = 1; :
+ <list of may-alias>
 <end of list>
-)
-(i = 0; -> <list of may-alias>
+ 
+After statement i = 0; :
+ <list of may-alias>
 <end of list>
-)
-(ty *tmp = x; -> <list of may-alias>
+ 
+After statement ty *tmp = x; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(while (i < 2) {
-   b->t1[i] = a->t1[i];
-   b->t2[i] = a->t2[i];
-   i ++;
- } -> <list of may-alias>
-<end of list>
-)
-(idata = (double *)malloc((unsigned long)10 * sizeof(double)); -> <list of may-alias>
+ 
+After statement while (i < 2) {
+                  b->t1[i] = a->t1[i];
+                  b->t2[i] = a->t2[i];
+                  i ++;
+                } :
+ <list of may-alias>
+<end of list>
+ 
+After statement idata = (double *)malloc((unsigned long)10 * sizeof(double)); :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(while (1) {
-   idata = tmp->t1[*(tmp->n1)];
-   odata = tmp->t2[*(tmp->n2)];
-   idx = 0;
-   while (idx < 10) {
-     *(odata + idx) = (double)3 * *(idata + idx) + (double)1;
-     idx ++;
-   }
-   swap(tmp->n2);
- } -> <list of may-alias>
+ 
+After statement while (1) {
+                  idata = tmp->t1[*(tmp->n1)];
+                  odata = tmp->t2[*(tmp->n2)];
+                  idx = 0;
+                  while (idx < 10) {
+                    *(odata + idx) = (double)3 * *(idata + idx) + (double)1;
+                    idx ++;
+                  }
+                  swap(tmp->n2);
+                } :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(if (! (i < 2)) break; -> <list of may-alias>
-<end of list>
-)
-(idata = tmp->t1[*(tmp->n1)];
- odata = tmp->t2[*(tmp->n2)];
- idx = 0;
- while (idx < 10) {
-   *(odata + idx) = (double)3 * *(idata + idx) + (double)1;
-   idx ++;
- }
- swap(tmp->n2); -> <list of may-alias>
+ 
+After statement if (! (i < 2)) break; :
+ <list of may-alias>
+<end of list>
+ 
+After statement idata = tmp->t1[*(tmp->n1)];
+                odata = tmp->t2[*(tmp->n2)];
+                idx = 0;
+                while (idx < 10) {
+                  *(odata + idx) = (double)3 * *(idata + idx) + (double)1;
+                  idx ++;
+                }
+                swap(tmp->n2); :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(break; -> <list of may-alias>
+ 
+After statement break; :
+ <list of may-alias>
 <end of list>
-)
-(idata = tmp->t1[*(tmp->n1)]; -> <list of may-alias>
+ 
+After statement idata = tmp->t1[*(tmp->n1)]; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-(b->t1[i] = a->t1[i];
- b->t2[i] = a->t2[i]; -> <list of may-alias>
+ 
+After statement b->t1[i] = a->t1[i];
+                b->t2[i] = a->t2[i]; :
+ <list of may-alias>
 <end of list>
-)
-(odata = tmp->t2[*(tmp->n2)]; -> <list of may-alias>
+ 
+After statement odata = tmp->t2[*(tmp->n2)]; :
+ <list of may-alias>
 { x; tmp } are aliased
 <end of list>
-)
-]
+ 
+
 [alias] Analysis complete
-- 
GitLab