diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml index 2ccf27969ed46fad6a08704b096a9ecf824fc026..2a0c7af021ac216b6eae8cea7f8315e3604f3ece 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 6e0868ccf242c011ba4763e2f0a5649a59eaae2f..31742605441ee475862e3b73262f956cea1c4433 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 {