From ad9c6eccf67748ae4e371de6310d94b059abaff9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 18 Apr 2023 13:23:04 +0200
Subject: [PATCH] [Eva] Fixes interpretation of successive split annotations.
A skip statement is created on each split annotation: do not ration
states on them to avoid meddling in successive split directives.
---
src/plugins/eva/engine/iterator.ml | 2 +-
src/plugins/eva/partitioning/trace_partitioning.ml | 6 +++++-
2 files changed, 6 insertions(+), 2 deletions(-)
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index 2ccf27969ed..2a0c7af021a 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -464,7 +464,7 @@ module Make_Dataflow
end;
(* Get vertex store *)
let store = get_vertex_store v in
- (* Join incoming s tates *)
+ (* Join incoming states *)
let flow = Partitioning.join sources store in
let flow =
match v.vertex_start_of with
diff --git a/src/plugins/eva/partitioning/trace_partitioning.ml b/src/plugins/eva/partitioning/trace_partitioning.ml
index 6e0868ccf24..31742605441 100644
--- a/src/plugins/eva/partitioning/trace_partitioning.ml
+++ b/src/plugins/eva/partitioning/trace_partitioning.ml
@@ -74,7 +74,11 @@ struct
let empty_store ~(stmt : stmt option) : store =
let limit, merge, flow_actions = match stmt with
| None -> max_int, false, []
- | Some stmt -> slevel stmt, merge stmt, flow_actions stmt
+ | Some stmt ->
+ let actions = flow_actions stmt in
+ if Cil.is_skip stmt.skind && actions <> []
+ then max_int, false, actions
+ else slevel stmt, merge stmt, actions
in
let rationing = Partition.new_rationing ~limit ~merge in
{
--
GitLab