Commit e76a0b77 authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl:archi] fix bug with constinit

parent d44a1535
......@@ -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 () =
......
......@@ -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;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment