From 19b1be74d24496c07b1247b71282ac76f0a5a156 Mon Sep 17 00:00:00 2001
From: Tristan Le Gall <tristan.le-gall@cea.fr>
Date: Thu, 16 Feb 2023 17:11:23 +0100
Subject: [PATCH] [alias] fixed - print_dot function
---
src/plugins/alias/Alias.ml | 2 +-
src/plugins/alias/abstract_state.ml | 13 +++++++------
src/plugins/alias/analysis.ml | 2 +-
3 files changed, 9 insertions(+), 8 deletions(-)
diff --git a/src/plugins/alias/Alias.ml b/src/plugins/alias/Alias.ml
index b1143e01c4a..dbc33eef711 100644
--- a/src/plugins/alias/Alias.ml
+++ b/src/plugins/alias/Alias.ml
@@ -29,6 +29,6 @@ let main () =
Analysis.compute ();
Options.feedback "Analysis complete";
end
-
+
let () =
Db.Main.extend main
diff --git a/src/plugins/alias/abstract_state.ml b/src/plugins/alias/abstract_state.ml
index 4cd5c110cab..01b59fcfa59 100644
--- a/src/plugins/alias/abstract_state.ml
+++ b/src/plugins/alias/abstract_state.ml
@@ -297,11 +297,10 @@ let remove_lval (x:t) (lv:lval) :t =
let find_vertex_name_ref = Extlib.mk_fun "find_vertex_name"
-let lset_to_string s =
- let buffer = Buffer.create 16 in
- let fmt = Format.formatter_of_buffer buffer in
- Format.fprintf fmt "%a" LSet.pretty s ;
- Buffer.contents buffer
+let lset_to_string (s: LSet.t) : string =
+ let fmt = Format.str_formatter in
+ Format.fprintf fmt "\"%a\"" LSet.pretty s;
+ Format.flush_str_formatter ()
module Dot = Graphviz.Dot(struct
include G
@@ -311,7 +310,9 @@ module Dot = Graphviz.Dot(struct
let vertex_attributes _ = [`Shape `Box]
let vertex_name (v:V.t) =
let lset = !find_vertex_name_ref v in
- lset_to_string lset
+ let v_name = lset_to_string lset in
+ Format.printf "Vertex %d set %s@." v v_name;
+ v_name
let default_vertex_attributes _ = []
let graph_attributes _ = []
end)
diff --git a/src/plugins/alias/analysis.ml b/src/plugins/alias/analysis.ml
index bbadf5c6d4a..5b4e214c27b 100644
--- a/src/plugins/alias/analysis.ml
+++ b/src/plugins/alias/analysis.ml
@@ -103,7 +103,7 @@ let do_assignment (a:Abstract_state.t option) (lv:lval) (exp:exp) : Abstract_sta
begin
match e1.enode with
Lval lv1 -> Some (Abstract_state.assignment_ptr_x_y a lv1 lv2)
- | _ -> (Options.feedback "Skipping assignment @[%a@] = @[%a@] (BUG do_assignment 2)" Lval.pretty lv Exp.pretty exp; Some a)
+ | _ -> (Options.feedback "Skipping assignment @[%a@] = @[%a@] (BUG do_assignment 2)" Lval.pretty lv Exp.pretty exp; Some a)
end
(* cases *x = cst *)
| (Some a, (Mem e1, NoOffset), BNone) ->
--
GitLab