From 3b427eb01c56292fdc8218800750b8d8b409014e Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime2.jacquemin@gmail.com>
Date: Mon, 12 Sep 2022 13:58:15 +0200
Subject: [PATCH] [Eva] Bug fix in the "smashed" function of
traece_partitionning.ml
The function relied on "List.map" which is not tail-rec. With enough
plevel, it provoked a stack overflow. I've simply fixed it by performing
the mapped computation inside the fold directly.
---
src/plugins/eva/partitioning/trace_partitioning.ml | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/plugins/eva/partitioning/trace_partitioning.ml b/src/plugins/eva/partitioning/trace_partitioning.ml
index 14df1779833..1b6826e7e7b 100644
--- a/src/plugins/eva/partitioning/trace_partitioning.ml
+++ b/src/plugins/eva/partitioning/trace_partitioning.ml
@@ -117,7 +117,9 @@ struct
let smashed (s : store) : state Lattice_bounds.or_bottom =
match expanded s with
| [] -> `Bottom
- | (_k, v1) :: l -> `Value (List.fold_left Domain.join v1 (List.map snd l))
+ | (_k, v1) :: l ->
+ let f acc (_k, v) = Domain.join acc v in
+ `Value (List.fold_left f v1 l)
let contents (flow : flow) : state list =
Flow.to_list flow
--
GitLab