diff --git a/src/libraries/utils/pretty_utils.ml b/src/libraries/utils/pretty_utils.ml
index b45091105571b31ea853dfe1f5891833b170f64d..cf7bc17c9d7773d63734f5192b56d729732b44e7 100644
--- a/src/libraries/utils/pretty_utils.ml
+++ b/src/libraries/utils/pretty_utils.ml
@@ -132,6 +132,10 @@ let pp_pair
let escape_underscores = Str.global_replace (Str.regexp_string "_") "__"
+let pp_escaped pp fmt e =
+ let s = Format.asprintf "%a" pp e in
+ Format.fprintf fmt "%s" (String.escaped s)
+
let pp_flowlist ?(left=format_of_string "(") ?(sep=format_of_string ",") ?(right=format_of_string ")") f out =
function
| [] -> Format.fprintf out "%(%)%(%)" left right
diff --git a/src/libraries/utils/pretty_utils.mli b/src/libraries/utils/pretty_utils.mli
index 4e3622182141bd02cd96d4416fd0b9ac6ed27fcf..12c9d35b3ecbb3add9430a38500183076c27b0c4 100644
--- a/src/libraries/utils/pretty_utils.mli
+++ b/src/libraries/utils/pretty_utils.mli
@@ -143,6 +143,10 @@ val pp_trail : 'a formatter -> 'a formatter
(** pretty-prints its contents inside an '(** ... **)' horizontal block trailed
with '*' *)
+val pp_escaped: 'a formatter -> 'a formatter
+(** [pp_escaped pp e] pretty-prints [e] with [String.escaped].
+ @since Frama-C+dev *)
+
(* ********************************************************************** *)
(** {2 Description Lists (margins)} *)
(* ********************************************************************** *)
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index e3551aed9e2793642dce4294288f8e81c8710e15..b6de18a2a56ddcca55cac06b18bd43930d12a226 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -817,7 +817,9 @@ module GraphDot = OCamlGraph.Graphviz.Dot(struct
let edge_attributes : E.t -> OCamlGraph.Graphviz.DotAttributes.edge list =
function
| Usual(_,{edge_trans = Loop _},_) -> [`Label (Format.asprintf "leave_loop")]
- | Usual(_,e,_) -> [`Label (Format.asprintf "@[<h>%a@]" Transition.pretty e.edge_trans)]
+ | Usual(_,e,_) ->
+ [`Label (Format.asprintf "@[<h>%a@]"
+ (Pretty_utils.pp_escaped Transition.pretty) e.edge_trans)]
| Head _ -> []
| Back(_,_,_) -> [`Constraint false]
end)
@@ -1245,9 +1247,10 @@ module D = struct
let leave_scope kf vars state =
Traces.add_trans state (LeaveScope (kf, vars))
- let output_dot filename state =
- let out = open_out filename in
- Self.feedback ~dkey:log_category "@[Output dot produced to %s.@]" filename;
+ let output_dot (filename : Filepath.Normalized.t) state =
+ let out = open_out (filename :> string) in
+ Self.feedback ~dkey:log_category "@[Output dot produced to %a.@]"
+ Filepath.Normalized.pretty filename;
GraphDot.output_graph out (complete_graph (snd (Traces.get_current state)));
close_out out
@@ -1268,7 +1271,7 @@ module D = struct
Self.failure "The trace is TOP can't generate code"
| `Value state ->
if not (Parameters.TracesDot.is_default ())
- then output_dot (Parameters.TracesDot.get ():>string) state;
+ then output_dot (Parameters.TracesDot.get ()) state;
if Parameters.TracesProject.get ()
then project_of_cfg return_exp state
end
diff --git a/tests/value/traces/oracle/test1.dot b/tests/value/traces/oracle/test1.dot
new file mode 100644
index 0000000000000000000000000000000000000000..1a176f1317b456c77508a71d0346d0b5006f8cc7
--- /dev/null
+++ b/tests/value/traces/oracle/test1.dot
@@ -0,0 +1,103 @@
+digraph G {
+ n0S [label="0", ];
+ n1S [label="1", ];
+ n2S [label="2", ];
+ n3S [label="3", ];
+ n4S [label="4", ];
+ n5S [label="5", ];
+ n6S [label="6", ];
+ n7S [label="7", ];
+ n8S [label="8", ];
+ n9S [label="9", ];
+ n10S [label="10", ];
+ n11S [label="11", ];
+ n12S [label="12", ];
+ n13S [label="13", ];
+ n14S [label="14", ];
+ n15S [label="15", ];
+ n16S [label="16", ];
+ n17S [label="17", ];
+ n18S [label="18", ];
+ n19S [label="19", ];
+ n20S [label="20", ];
+ n21S [label="21", ];
+ n22S [label="22", ];
+ n23S [label="23", ];
+ n24S [label="24", ];
+ n25S [label="25", ];
+ n26S [label="26", ];
+ n27S [label="27", ];
+ n28S [label="28", ];
+ n29S [label="29", ];
+ n30S [label="30", ];
+ n31S [label="31", ];
+ n32S [label="32", ];
+ n33S [label="33", ];
+ n34S [label="34", ];
+ n35S [label="35", ];
+ n36S [label="36", ];
+ n37S [label="37", ];
+ n38S [label="38", ];
+ n39S [label="39", ];
+ n40S [label="40", ];
+ n41S [label="41", ];
+ n42S [label="42", ];
+ n43S [label="43", ];
+ n44S [label="44", ];
+ n45S [label="45", ];
+ n46S [label="46", ];
+ n47S [label="47", ];
+ n48S [label="48", ];
+
+
+ n0S -> n1S [label="initialize variable: entropy_source", ];
+ n1S -> n2S [label="initialize global variable using type\nentropy_source", ];
+ n2S -> n3S [label="initialize variable: g", ];
+ n3S -> n4S [label="Assign:\ng = 42", ];
+ n4S -> n5S [label="initialize formal variable using type\nc", ];
+ n5S -> n6S [label="EnterScope:\ntmp", ];
+ n6S -> n7S [label="Assign:\ntmp = 0", ];
+ n7S -> n8S [label="Assume:\nc true", ];
+ n7S -> n10S [label="Assume:\nc false", ];
+ n8S -> n9S [label="Assign:\ntmp = g", ];
+ n9S -> n12S [label="EnterScope:\ni", ];
+ n10S -> n11S [label="Assign:\ntmp = 2", ];
+ n11S -> n13S [label="EnterScope:\ni", ];
+ n12S -> n14S [label="initialize variable: i", ];
+ n13S -> n16S [label="initialize variable: i", ];
+ n14S -> n15S [label="Assign:\ni = 0", ];
+ n15S -> n19S [label="enter_loop", ];
+ n16S -> n17S [label="Assign:\ni = 0", ];
+ n17S -> n18S [label="enter_loop", ];
+ n18S -> n20S [label="Assume:\ni < 3 true", ];
+ n19S -> n21S [label="Assume:\ni < 3 true", ];
+ n20S -> n22S [label="Assign:\ntmp = tmp + 1", ];
+ n21S -> n23S [label="Assign:\ntmp = tmp + 1", ];
+ n22S -> n24S [label="Assign:\ni = i + 1", ];
+ n23S -> n25S [label="Assign:\ni = i + 1", ];
+ n24S -> n27S [label="Assume:\ni < 3 true", ];
+ n25S -> n26S [label="Assume:\ni < 3 true", ];
+ n26S -> n28S [label="Assign:\ntmp = tmp + 1", ];
+ n27S -> n29S [label="Assign:\ntmp = tmp + 1", ];
+ n28S -> n30S [label="Assign:\ni = i + 1", ];
+ n29S -> n31S [label="Assign:\ni = i + 1", ];
+ n30S -> n33S [label="Assume:\ni < 3 true", ];
+ n31S -> n32S [label="Assume:\ni < 3 true", ];
+ n32S -> n34S [label="Assign:\ntmp = tmp + 1", ];
+ n33S -> n35S [label="Assign:\ntmp = tmp + 1", ];
+ n34S -> n36S [label="Assign:\ni = i + 1", ];
+ n35S -> n37S [label="Assign:\ni = i + 1", ];
+ n36S -> n39S [label="Assume:\ni < 3 false", ];
+ n37S -> n38S [label="Assume:\ni < 3 false", ];
+ n38S -> n41S [label="LeaveScope:\ni", ];
+ n39S -> n40S [label="LeaveScope:\ni", ];
+ n40S -> n42S [label="Assign:\ng = tmp", ];
+ n41S -> n43S [label="Assign:\ng = tmp", ];
+ n42S -> n44S [label="EnterScope:\n\\result<main>", ];
+ n43S -> n46S [label="EnterScope:\n\\result<main>", ];
+ n44S -> n45S [label="Assign:\n\\result<main> = tmp", ];
+ n45S -> n48S [label="join", ];
+ n46S -> n47S [label="Assign:\n\\result<main> = tmp", ];
+ n47S -> n48S [label="join", ];
+
+ }
diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle
index 29eb5de43dc24f35cadc830bf6bb351be0d8ee82..42663736995dcc0831eee3c795711f47aeb4affd 100644
--- a/tests/value/traces/oracle/test1.res.oracle
+++ b/tests/value/traces/oracle/test1.res.oracle
@@ -64,6 +64,7 @@ c -> 5
45 -> join -> 48
46 -> Assign: \result<main> = tmp -> 47
47 -> join -> 48 ]} at 48
+[eva:d-traces] Output dot produced to test1.dot.
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/value/traces/test1.c b/tests/value/traces/test1.c
index 2eda2c29eb845ca3b7a6c489f0be9bbd3a1b7c14..62cf888e562e7192aadb535a7c40305f83479f77 100644
--- a/tests/value/traces/test1.c
+++ b/tests/value/traces/test1.c
@@ -1,5 +1,6 @@
/* run.config
- STDOPT: #"-eva-domains traces -eva-msg-key d-traces -eva-slevel 10 -eva-traces-project" +"-then-last -eva -print -eva-msg-key=-d-traces"
+ LOG: @PTEST_NAME@.dot
+ STDOPT: #"-eva-domains traces -eva-msg-key d-traces -eva-traces-dot @PTEST_NAME@.dot -eva-slevel 10 -eva-traces-project" +"-then-last -eva -print -eva-msg-key=-d-traces"
*/
extern volatile int entropy_source;