From 130c2249ec95a2caee4c3f0fc1680d22b54e044d Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 16 Sep 2024 18:12:09 +0200
Subject: [PATCH] [Eva] add test for traces domain graph generation
---
src/plugins/eva/domains/traces_domain.ml | 9 +-
tests/value/traces/oracle/test1.dot | 105 +++++++++++++++++++++
tests/value/traces/oracle/test1.res.oracle | 1 +
tests/value/traces/test1.c | 3 +-
4 files changed, 113 insertions(+), 5 deletions(-)
create mode 100644 tests/value/traces/oracle/test1.dot
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index e3551aed9e2..4838ff3904a 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/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
diff --git a/tests/value/traces/oracle/test1.dot b/tests/value/traces/oracle/test1.dot
new file mode 100644
index 00000000000..e5e6cff56e6
--- /dev/null
+++ b/tests/value/traces/oracle/test1.dot
@@ -0,0 +1,105 @@
+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", ];
+
+ }
diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle
index 29eb5de43dc..42663736995 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 2eda2c29eb8..62cf888e562 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;
--
GitLab