Commit 0bc945bf authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl:archi] remove TODOs

parent 2142b6f7
...@@ -172,9 +172,7 @@ let add_initializer loc ?vi lv ?(post=false) stmt env kf = ...@@ -172,9 +172,7 @@ let add_initializer loc ?vi lv ?(post=false) stmt env kf =
else else
env env
let inject_in_instr env kf stmt instr = let inject_in_instr env kf stmt = function
(* [TODO ARCHI] recursive calls at the right places *)
match instr with
| Set(lv, e, loc) -> | Set(lv, e, loc) ->
let e, env = replace_literal_string_in_exp env (Some kf) e in let e, env = replace_literal_string_in_exp env (Some kf) e in
let env = add_initializer loc lv stmt env kf in let env = add_initializer loc lv stmt env kf in
...@@ -209,14 +207,10 @@ let inject_in_instr env kf stmt instr = ...@@ -209,14 +207,10 @@ let inject_in_instr env kf stmt instr =
(* nothing to do: *) (* nothing to do: *)
| Asm _ | Asm _
| Skip _ | Skip _
| Code_annot _ -> | Code_annot _ as instr ->
instr, env instr, env
let add_new_block_in_stmt env kf stmt = let add_new_block_in_stmt env kf stmt =
(* be careful: since this function is called in a post action, [env] has been
modified from the time where pre actions have been executed. Use
[function_env] to get it back. *)
(* [TODO ARCHI] what about the above comment? *)
(* Add temporal analysis instrumentations *) (* Add temporal analysis instrumentations *)
let env = Temporal.handle_stmt stmt env kf in let env = Temporal.handle_stmt stmt env kf in
let new_stmt, env = let new_stmt, env =
...@@ -331,9 +325,6 @@ let add_new_block_in_stmt env kf stmt = ...@@ -331,9 +325,6 @@ let add_new_block_in_stmt env kf stmt =
"@[new stmt (from sid %d):@ %a@]" stmt.sid Printer.pp_stmt new_stmt; "@[new stmt (from sid %d):@ %a@]" stmt.sid Printer.pp_stmt new_stmt;
new_stmt, env new_stmt, env
(* [TODO ARCHI] not sure returning the stmt_kind is useful;
actually probably useful for printf-like functions.
TO BE TESTED LATER *)
(* visit the substmts and build the new skind *) (* visit the substmts and build the new skind *)
let rec inject_in_substmt env kf stmt = match stmt.skind with let rec inject_in_substmt env kf stmt = match stmt.skind with
| Instr instr -> | Instr instr ->
...@@ -624,10 +615,10 @@ let inject_in_global (env, main) = function ...@@ -624,10 +615,10 @@ let inject_in_global (env, main) = function
| GVar(vi, { init = Some init }, _) -> | GVar(vi, { init = Some init }, _) ->
Global_observer.add vi; Global_observer.add vi;
vi.vghost <- false; vi.vghost <- false;
(* [TODO ARCHI] check that keeping changes in initializers is useless since let _init, env = inject_in_init env None vi NoOffset init in
all is done in place --> document why returning an expression is useful: (* ignore the new initializer that handles literal strings since they are
what may change? *) not substituted in global initializers (see
let _, env = inject_in_init env None vi NoOffset init in [replace_literal_string_in_exp]) *)
env, main env, main
(* function definition *) (* function definition *)
......
Supports Markdown
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