diff --git a/src/plugins/alias/abstract_state.ml b/src/plugins/alias/abstract_state.ml index 9af3dced6b0a54a8e0e16085da453522d8e46193..411a14dc38f0c42cb06a0ee4d71c2aa980c5b3b2 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 2ad7d6c10f4e71d23139156e44c0971828253203..06744a481025467ba031977a9a30bf8d69f1433f 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 0000000000000000000000000000000000000000..41d177f99d68ef6fc6e6fa725c9506021a573c0a --- /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 0000000000000000000000000000000000000000..dd313a5e7633c500498e0ad9cf55db895178a2c8 --- /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 0000000000000000000000000000000000000000..f38e06e7fb0d47978a4ed71b797ddc693d262ac3 --- /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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391