diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml index a6b0a343fbd01018363407416c0be247ec8bf7da..b5d6f518de3f5e477e0de003b7a3897330b9cdad 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 aa56af94e4ccf447d6f89867685836fa7152faba..a0e7efedc5e1d53d63988a48f40afb3d559c3344 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;