diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml index 4838ff3904aca27ce450de38a65eeb8df19d843a..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) diff --git a/tests/value/traces/oracle/test1.dot b/tests/value/traces/oracle/test1.dot index e5e6cff56e668e1fe6d5884171f28fadfce2a23a..1a176f1317b456c77508a71d0346d0b5006f8cc7 100644 --- a/tests/value/traces/oracle/test1.dot +++ b/tests/value/traces/oracle/test1.dot @@ -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", ]; }