Skip to content
Snippets Groups Projects
Commit 2d9728a5 authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl] convert annotations into C code in the right project

parent 0acd43ee
No related branches found
No related tags found
No related merge requests found
...@@ -407,7 +407,9 @@ class e_acsl_visitor prj generate = object (self) ...@@ -407,7 +407,9 @@ class e_acsl_visitor prj generate = object (self)
(self :> Visitor.frama_c_visitor) (self :> Visitor.frama_c_visitor)
(Kernel_function.get_spec old_kf) (Kernel_function.get_spec old_kf)
in 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; pre_block <- pre_b;
post_block <- post_b; post_block <- post_b;
gen_vars <- Env.generated_function_variables env; gen_vars <- Env.generated_function_variables env;
...@@ -437,7 +439,9 @@ class e_acsl_visitor prj generate = object (self) ...@@ -437,7 +439,9 @@ class e_acsl_visitor prj generate = object (self)
(self :> Visitor.frama_c_visitor) (self :> Visitor.frama_c_visitor)
old_a old_a
in 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 let post_stmts = match post_block with
| None -> post_stmts | None -> post_stmts
| Some b -> | Some b ->
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment