From 59c600bec85d38ebaebdd0a30493de6d8dfaefdf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 18 Apr 2019 14:08:42 +0200
Subject: [PATCH] [Eva] Trace_partitioning.fill joins states instead of keeping
only the new ones.
---
src/plugins/value/engine/trace_partitioning.ml | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/engine/trace_partitioning.ml
index 063afad6c95..336e75f30ac 100644
--- a/src/plugins/value/engine/trace_partitioning.ml
+++ b/src/plugins/value/engine/trace_partitioning.ml
@@ -203,13 +203,13 @@ struct
flow
let fill ~(into : tank) (flow : flow) : unit =
- let erase _key dest src =
- if Extlib.has_some src
- then src
- else dest
- in
let new_states = Flow.to_partition flow in
- into.tank_states <- Partition.merge erase into.tank_states new_states
+ let join _key dest src = match dest, src with
+ | Some dest, Some src -> Some (Domain.join dest src)
+ | Some v, None | None, Some v -> Some v
+ | None, None -> None
+ in
+ into.tank_states <- Partition.merge join into.tank_states new_states
let transfer = Flow.transfer_states
--
GitLab