[alias] added tests

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 *)
 
 
 

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
 

src/plugins/alias/tests/basic/assignment1.c

+// single pointer assignment
+
+int main () {
+
+  int *a, *b, *c, *d, e;
+  a = b;
+  b = c;
+  *a = 4;
+  *c = e;
+  a = d ;
+  return 0;
+}

src/plugins/alias/tests/basic/assignment2.c

+// double pointer assignment
+
+int main () {
+
+  int **a, *b, **c, *d;
+  *a = b;
+  *c = d;
+  a = c;
+  return 0;
+}

src/plugins/alias/tests/basic/assignment3.c

+// address assignment
+
+int main () {
+
+  int *a, b, *c;
+  a = &b;
+  *c = b;
+  return 0;
+}