[alias] dot output WIP

src/plugins/alias/Alias.ml

@@ -27,8 +27,8 @@ let main () =
   if Options.Enabled.get() then
     begin
       Analysis.compute ();
-      Options.feedback "Analysis complete"
+      Options.feedback "Analysis complete";
     end
-
+    
 let () =
   Db.Main.extend main

src/plugins/alias/analysis.ml

@@ -234,10 +234,10 @@ let doFunction (kf:kernel_function) =
   if Kernel_function.has_definition kf then
     begin
       (* let print_key = Stmt.pretty in *)
-      let print_value fmt v =
+      let print_value ?(debug=false) fmt v =
         match v with
         | None -> Format.fprintf fmt "<Bot>"
-        | Some a -> Abstract_state.pretty fmt a
+        | Some a -> Abstract_state.pretty ~debug fmt a
       in
       let first_stmts =
         try [Kernel_function.find_first_stmt kf]
@@ -270,7 +270,18 @@ let doFunction (kf:kernel_function) =
         Function_table.add kf (Some summary)
       else
         (* if main, print the last abstract state *)
-        Options.feedback "May-aliases at the end of function main:@.%a@." print_value final_state
+        let f_name = Options.Dot_output.get () in
+        if f_name = ""
+        then
+          Options.feedback "May-aliases at the end of function main:@.%a@." (print_value ~debug:false) final_state
+        else
+          match final_state with
+            None  ->  Options.feedback "Abstract_state at the end of function main: <Bot>@."
+          | Some final_state ->
+            begin
+              Abstract_state.print_dot f_name final_state;
+              Options.feedback "Abstract_state at the end of function main:@.%a@." (print_value ~debug:true) (Some final_state)
+            end
     end
   else
     begin

src/plugins/alias/options.ml

@@ -51,3 +51,12 @@ module ShowStmtTable = False
       let option_name = "-alias-show-stmt-table"
       let help = "Displays the table [stmt -> abstract state] at the end of the analysis"
     end)
+
+
+module Dot_output =
+  Empty_string
+    (struct
+      let option_name = "-alias-dot-output"
+      let arg_name = "f"
+      let help = "Displays the final abstract state in Dot File <f>"
+    end)

src/plugins/alias/options.mli

@@ -34,3 +34,6 @@ module ShowFunctionTable : Parameter_sig.Bool
 
 (** Displays the table [statement -> state] at the end of the analysis *)
 module ShowStmtTable : Parameter_sig.Bool
+
+(** Displays the final abstract state in Dot File <f> *)
+module Dot_output : Parameter_sig.String