From 0f39af6e9eb4b47dfc46d64f16b10679e7758b00 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 21 Jun 2021 11:13:47 +0200
Subject: [PATCH] [eacsl] Recompute CFG before launching the dataflow analysis
---
src/plugins/e-acsl/src/analyses/memory_tracking.ml | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index cfb1f9aae8c..109f3d3beb5 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -639,6 +639,15 @@ end = struct
if not is_init then Env.add kf tbl;
(try
let fundec = Kernel_function.get_definition kf in
+ (* FIXME: Since the memory tracking analysis is launched during the
+ translation, we need to recompute the CFG of the function before the
+ dataflow analysis.
+ This fix is just temporary and should be removed once the correct fix
+ is applied: identifying in an early pre-analysis if some memory
+ annotations are used, and in that case launch the memory tracking in a
+ pre-analysis. *)
+ Cfg.clearCFGinfo ~clear_id:false fundec;
+ Cfg.cfgFun fundec;
let stmts, returns = Dataflow.find_stmts fundec in
if is_init then
Option.iter
--
GitLab