From e76a0b77394440fd55f3ad7b0c559286b06860e2 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 3 Dec 2019 09:52:27 +0100
Subject: [PATCH] [e-acsl:archi] fix bug with constinit
---
src/plugins/e-acsl/src/code_generator/injector.ml | 10 ++++------
.../e-acsl/src/project_initializer/dup_functions.ml | 2 +-
2 files changed, 5 insertions(+), 7 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index a6b0a343fbd..b5d6f518de3 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -59,8 +59,6 @@ let rec inject_in_init env kf_opt vi off = function
if vi.vglob then Global_observer.add_initializer vi off init;
let e, env = replace_literal_string_in_exp env kf_opt e in
SingleInit e, env
- | CompoundInit(_, []) as init ->
- init, env
| CompoundInit(typ, l) ->
let l, env =
List.fold_left
@@ -115,12 +113,12 @@ let inject_in_local_init loc env kf vi = function
| ConsInit(vi, l, ck) ->
let l, env =
- List.fold_left
- (fun (l, env) e ->
+ List.fold_right
+ (fun e (l, env) ->
let e, env = replace_literal_string_in_exp env (Some kf) e in
e :: l, env)
- ([], env)
l
+ ([], env)
in
ConsInit(vi, l, ck), env
@@ -768,7 +766,7 @@ let reset_all ast =
Typing.clear ();
Cfg.clearFileCFG ~clear_id:false ast;
Cfg.computeFileCFG ast;
- Kernel_function.clear_sid_info ();
+ Kernel_function.clear_sid_info (); (* [ARCHI] is it really useful? *)
Ast.mark_as_grown ()
let inject () =
diff --git a/src/plugins/e-acsl/src/project_initializer/dup_functions.ml b/src/plugins/e-acsl/src/project_initializer/dup_functions.ml
index aa56af94e4c..a0e7efedc5e 100644
--- a/src/plugins/e-acsl/src/project_initializer/dup_functions.ml
+++ b/src/plugins/e-acsl/src/project_initializer/dup_functions.ml
@@ -415,7 +415,7 @@ let dup () =
Options.feedback ~level:2 "duplicating annotated functions";
let prj =
File.create_project_from_visitor
- "e_acsl_dup_functions"
+ "e_acsl_dup_functions"
(new dup_functions_visitor)
in
Queue.iter (fun f -> f ()) actions;
--
GitLab