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

[archi] fix a few TODOs

parent c3e912e4
......@@ -203,8 +203,8 @@ let index_from_sizes_and_shifts ~loc sizes_and_shifts =
in
sum
let put_block_at_label env block label =
let stmt = Label.get_stmt label in
let put_block_at_label env kf block label =
let stmt = Label.get_stmt kf label in
let env_ref = ref env in
let o = object
inherit Visitor.frama_c_inplace
......@@ -336,7 +336,7 @@ let to_exp ~loc kf env pot label =
Env.After
in
(* Put at label *)
let env = put_block_at_label env storing_loops_block label in
let env = put_block_at_label env kf storing_loops_block label in
(* Returning *)
let lval_at_index, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
let e = Cil.new_exp ~loc (Lval lval_at_index) in
......
......@@ -311,23 +311,15 @@ module Logic_scope = struct
else env
end
let _emitter = (* [TODO ARCHI] *)
let emitter =
Emitter.create
"E_ACSL"
[ Emitter.Code_annot ]
~correctness:[ Options.Gmp_only.parameter ]
~tuning:[]
(* [TODO ARCHI] to be reimplemented *)
let add_assert _env _stmt _annot = assert false
(*match current_kf env with
| None -> assert false
| Some _kf ->
(* Queue.add
(fun () -> Annotations.add_assert emitter ~kf stmt annot)
env.visitor#get_filling_actions
*)*)
(* [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 =
if not post then
......
......@@ -75,7 +75,7 @@ module Logic_binding: sig
end
val add_assert: t -> stmt -> predicate -> unit
val add_assert: kernel_function -> stmt -> predicate -> unit
(** [add_assert env s p] associates the assertion [p] to the statement [s] in
the environment [env]. *)
......
......@@ -426,12 +426,13 @@ let rec inject_in_substmt env kf stmt = match stmt.skind with
let env = inject_in_block env kf blk2 in
skind, env
| TryExcept(blk1, (instrs, e), blk2, loc) ->
let env = inject_in_block env kf blk1 in
| 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
TryExcept(blk1, (instrs, e), blk2, loc), env*)
(* nothing to do: *)
| Throw(None, _)
......
......@@ -69,19 +69,15 @@ let move kf ~old new_stmt =
in
List.iter mv_labels f.sallstmts
(* [TODO ARCHI] reimplement it *)
let get_stmt = function
let get_stmt kf = function
| StmtLabel { contents = stmt } -> stmt
| BuiltinLabel Here ->
(* (match vis#current_stmt with
| None -> Error.not_yet "label \"Here\" in function contract"
| Some s -> s)*) assert false
| BuiltinLabel Here -> Error.not_yet "Label 'Here'"
| BuiltinLabel(Old | Pre) ->
(* (try Kernel_function.find_first_stmt (Extlib.the vis#current_kf)
with Kernel_function.No_Statement -> assert false)*)assert false
(try Kernel_function.find_first_stmt kf
with Kernel_function.No_Statement -> assert false)
| BuiltinLabel(Post) ->
(* (try Kernel_function.find_return (Extlib.the vis#current_kf)
with Kernel_function.No_Statement -> assert false)*) assert false
(try Kernel_function.find_return kf
with Kernel_function.No_Statement -> assert false)
| BuiltinLabel _ | FormalLabel _ -> assert false
(*
......
......@@ -26,7 +26,7 @@ val move: kernel_function -> old:stmt -> stmt -> unit
(** Move all labels of the [old] stmt onto the new [stmt].
Both stmts must be in the new project. *)
val get_stmt: logic_label -> stmt
val get_stmt: kernel_function -> logic_label -> stmt
(** @return the statement where the logic label points to. *)
val new_labeled_stmt: stmt -> stmt
......
......@@ -177,10 +177,8 @@ let generate_kf ~loc fname env ret_ty params_ty li =
in
Cil.setMaxId fundec;
let spec = Cil.empty_funspec () in
(*[TODO ARCHI] reimplement *)
(* Queue.add
(fun () -> Globals.Functions.replace_by_definition spec fundec loc)
(Env.get_visitor env)#get_filling_actions;*)
(* register the definition *)
Globals.Functions.replace_by_definition spec fundec loc;
(* create the kernel function itself *)
let kf = { fundec = Definition(fundec, loc); spec } in
(* closure generating the function's body.
......
......@@ -369,7 +369,7 @@ and context_insensitive_term_to_exp kf env t =
guard
(Logic_const.prel ~loc (Req, t2, zero))
in
Env.add_assert env cond (Logic_const.prel (Rneq, t2, zero));
Env.add_assert kf cond (Logic_const.prel (Rneq, t2, zero));
let instr = Misc.mk_call ~loc name [ e; e1; e2 ] in
[ cond; instr ]
in
......@@ -619,7 +619,7 @@ and comparison_to_exp
Error.not_yet "comparison involving real numbers"
and at_to_exp_no_lscope env kf t_opt label e =
let stmt = E_acsl_label.get_stmt label in
let stmt = E_acsl_label.get_stmt kf label in
(* generate a new variable denoting [\at(t',label)].
That is this variable which is the resulting expression.
ACSL typing rule ensures that the type of this variable is the same as
......@@ -660,9 +660,10 @@ and at_to_exp_no_lscope env kf t_opt label e =
Cil.ChangeTo stmt
end
in
let _new_stmt = Visitor.visitFramacStmt o stmt in
(* [TODO ARCHI] reimplement *)
(*Visitor_behavior.Set.stmt bhv stmt new_stmt;*)
(* [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 =
......
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