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

[e-acsl:archi] killing useless code

parent bf9c0a96
......@@ -318,7 +318,6 @@ let emitter =
~correctness:[ Options.Gmp_only.parameter ]
~tuning:[]
(* [TODO ARCHI] to be inlined? *)
let add_assert kf stmt annot = Annotations.add_assert emitter ~kf stmt annot
let add_stmt ?(post=false) ?before env kf stmt =
......@@ -432,13 +431,8 @@ let pop_and_get ?(split=false) env stmt ~global_clear where =
add the given [stmt] afterwards. This way, we have the guarantee that
the final block does not contain any local, so may be transient. *)
if split then
match stmt.skind with
(* [TODO ARCHI] would result in nicer generated pieces of code, but
* killing statements has huge consequences on Frama-C invariants... *)
(* | Instr (Skip _) -> b *)
| _ ->
let sblock = Cil.mkStmt ~valid_sid:true (Block b) in
Cil.transient_block (Cil.mkBlock [ sblock; stmt ])
let sblock = Cil.mkStmt ~valid_sid:true (Block b) in
Cil.transient_block (Cil.mkBlock [ sblock; stmt ])
else
b
in
......
......@@ -422,11 +422,6 @@ let rec inject_in_substmt env kf stmt = match stmt.skind with
| TryExcept(_blk1, (_instrs, _e), _blk2, _loc) ->
Error.not_yet "try ... except ..."
(* let env = inject_in_block env kf blk1 in
let e, env = replace_literal_string_in_exp false env kf e in
let env = inject_in_block env kf blk2 in
ignore (assert false) (* TODO ARCHI: instrs *);
TryExcept(blk1, (instrs, e), blk2, loc), env*)
(* nothing to do: *)
| Throw(None, _)
......@@ -765,7 +760,6 @@ let reset_all ast =
Typing.clear ();
Cfg.clearFileCFG ~clear_id:false ast;
Cfg.computeFileCFG ast;
Kernel_function.clear_sid_info (); (* [ARCHI] is it really useful? *)
Ast.mark_as_grown ()
let inject () =
......
......@@ -664,10 +664,7 @@ and at_to_exp_no_lscope env kf t_opt label e =
Cil.ChangeTo stmt
end
in
(* [TODO ARCHI] is it still useful? *)
ignore (Visitor.visitFramacStmt o stmt);
(*let _new_stmt = Visitor.visitFramacStmt o stmt in
Visitor_behavior.Set.stmt bhv stmt new_stmt;*)
res, !env_ref, C_number
and env_of_li li kf env loc =
......
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