Skip to content
Snippets Groups Projects
Commit 618e9d8d authored by Andre Maroneze's avatar Andre Maroneze Committed by David Bühler
Browse files

[eva] fix pretty-printing of dot graph in traces domain

Without escaping strings such as variable names, the produced .dot file
might print '\result' as a variable name, which results in '\r' being
stripped. Dot will then show edges such as 'esult<main>'.
parent 0b6079aa
No related branches found
No related tags found
No related merge requests found
......@@ -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)
......
......@@ -51,55 +51,53 @@ digraph G {
n0S -> n1S [label="initialize variable: entropy_source", ];
n1S -> n2S [label="initialize global variable using type
entropy_source", ];
n1S -> n2S [label="initialize global variable using type\nentropy_source", ];
n2S -> n3S [label="initialize variable: g", ];
n3S -> n4S [label="Assign: g = 42", ];
n4S -> n5S [label="initialize formal variable using type
c", ];
n5S -> n6S [label="EnterScope: tmp", ];
n6S -> n7S [label="Assign: tmp = 0", ];
n7S -> n8S [label="Assume: c true", ];
n7S -> n10S [label="Assume: c false", ];
n8S -> n9S [label="Assign: tmp = g", ];
n9S -> n12S [label="EnterScope: i", ];
n10S -> n11S [label="Assign: tmp = 2", ];
n11S -> n13S [label="EnterScope: i", ];
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: i = 0", ];
n14S -> n15S [label="Assign:\ni = 0", ];
n15S -> n19S [label="enter_loop", ];
n16S -> n17S [label="Assign: i = 0", ];
n16S -> n17S [label="Assign:\ni = 0", ];
n17S -> n18S [label="enter_loop", ];
n18S -> n20S [label="Assume: i < 3 true", ];
n19S -> n21S [label="Assume: i < 3 true", ];
n20S -> n22S [label="Assign: tmp = tmp + 1", ];
n21S -> n23S [label="Assign: tmp = tmp + 1", ];
n22S -> n24S [label="Assign: i = i + 1", ];
n23S -> n25S [label="Assign: i = i + 1", ];
n24S -> n27S [label="Assume: i < 3 true", ];
n25S -> n26S [label="Assume: i < 3 true", ];
n26S -> n28S [label="Assign: tmp = tmp + 1", ];
n27S -> n29S [label="Assign: tmp = tmp + 1", ];
n28S -> n30S [label="Assign: i = i + 1", ];
n29S -> n31S [label="Assign: i = i + 1", ];
n30S -> n33S [label="Assume: i < 3 true", ];
n31S -> n32S [label="Assume: i < 3 true", ];
n32S -> n34S [label="Assign: tmp = tmp + 1", ];
n33S -> n35S [label="Assign: tmp = tmp + 1", ];
n34S -> n36S [label="Assign: i = i + 1", ];
n35S -> n37S [label="Assign: i = i + 1", ];
n36S -> n39S [label="Assume: i < 3 false", ];
n37S -> n38S [label="Assume: i < 3 false", ];
n38S -> n41S [label="LeaveScope: i", ];
n39S -> n40S [label="LeaveScope: i", ];
n40S -> n42S [label="Assign: g = tmp", ];
n41S -> n43S [label="Assign: g = tmp", ];
n42S -> n44S [label="EnterScope: \result<main>", ];
n43S -> n46S [label="EnterScope: \result<main>", ];
n44S -> n45S [label="Assign: \result<main> = tmp", ];
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: \result<main> = tmp", ];
n46S -> n47S [label="Assign:\n\\result<main> = tmp", ];
n47S -> n48S [label="join", ];
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment