From 43bd8326c72bd63b2874a450afabf53bd26f22e8 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 17 Feb 2017 15:52:28 +0100
Subject: [PATCH] apply Project.on more carefully
---
src/plugins/e-acsl/visit.ml | 21 ++++++++++-----------
1 file changed, 10 insertions(+), 11 deletions(-)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 202130353ca..dc9997ed37d 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -635,17 +635,16 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
if not (may_safely_ignore assigned_lv) &&
Mmodel_analysis.must_model_lval ~kf ~stmt checked_lv
then
- (* must be in the new project to build a new stmt *)
- Project.on
- prj
- (fun () ->
- let new_stmt =
- Misc.mk_debug_mmodel_stmt (Misc.mk_initialize loc assigned_lv)
- in
- let before = Cil.memo_stmt self#behavior stmt in
- let new_stmt = Cil.memo_stmt self#behavior new_stmt in
- function_env := Env.add_stmt ~before !function_env new_stmt)
- ()
+ let new_stmt =
+ (* must be in the new project to build a new stmt *)
+ Project.on
+ prj
+ Misc.mk_debug_mmodel_stmt
+ (Misc.mk_initialize loc assigned_lv)
+ in
+ let before = Cil.memo_stmt self#behavior stmt in
+ let new_stmt = Cil.memo_stmt self#behavior new_stmt in
+ function_env := Env.add_stmt ~before !function_env new_stmt
method !vinst = function
| Set(old_lv, _, _) ->
--
GitLab