[Eva] add test for traces domain graph generation

src/plugins/eva/domains/traces_domain.ml

@@ -1245,9 +1245,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 +1269,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

tests/value/traces/oracle/test1.dot

+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
+entropy_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", ];
+  n12S -> n14S [label="initialize variable: i", ];
+  n13S -> n16S [label="initialize variable: i", ];
+  n14S -> n15S [label="Assign: i = 0", ];
+  n15S -> n19S [label="enter_loop", ];
+  n16S -> n17S [label="Assign: i = 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", ];
+  n45S -> n48S [label="join", ];
+  n46S -> n47S [label="Assign: \result<main> = tmp", ];
+  n47S -> n48S [label="join", ];
+  
+  }

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 ======

tests/value/traces/test1.c

 /* 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;