From 2d9728a5d01818b417397266cf9bb17f773bc223 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 26 May 2011 09:22:51 +0000
Subject: [PATCH] [e-acsl] convert annotations into C code in the right project
---
src/plugins/e-acsl/visit.ml | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 681eaf4d5d6..82302b4394a 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -407,7 +407,9 @@ class e_acsl_visitor prj generate = object (self)
(self :> Visitor.frama_c_visitor)
(Kernel_function.get_spec old_kf)
in
- let pre_b, post_b, env = convert_spec Env.empty spec in
+ let pre_b, post_b, env =
+ Project.on prj (convert_spec Env.empty) spec
+ in
pre_block <- pre_b;
post_block <- post_b;
gen_vars <- Env.generated_function_variables env;
@@ -437,7 +439,9 @@ class e_acsl_visitor prj generate = object (self)
(self :> Visitor.frama_c_visitor)
old_a
in
- let env, post_block = convert_code_annotation env a in
+ let env, post_block =
+ Project.on prj (convert_code_annotation env) a
+ in
let post_stmts = match post_block with
| None -> post_stmts
| Some b ->
--
GitLab