Commit 3defbd29 authored by Julien Signoles's avatar Julien Signoles
Browse files

[archi] visit block stmts in the correct order

parent 52d39bfe
......@@ -494,14 +494,14 @@ and inject_in_stmt env kf stmt =
and inject_in_block (env: Env.t) kf blk =
let stmts, env =
List.fold_right
(fun stmt (stmts, env) ->
List.fold_left
(fun (stmts, env) stmt ->
let stmt, env = inject_in_stmt env kf stmt in
stmt :: stmts, env)
blk.bstmts
([], env)
blk.bstmts
in
blk.bstmts <- stmts;
blk.bstmts <- List.rev stmts;
let free_stmts = At_with_lscope.Free.find_all kf in
match blk.blocals, free_stmts with
| [], [] ->
......
......@@ -980,12 +980,12 @@ let translate_preconditions kf env behaviors =
~loc
(assumes_pred,
Logic_const.unamed ~loc p.ip_content.pred_content)
in
translate_named_predicate kf env p
else
env
in
handle_error do_it env)
in
translate_named_predicate kf env p
else
env
in
handle_error do_it env)
env
b.b_requires
in
......
......@@ -150,3 +150,9 @@ let must_translate kf kind =
pretty_kind kind';
keep
with Not_found -> true
(*
Local Variables:
compile-command: "make -C ../.."
End:
*)
......@@ -44,7 +44,7 @@ val push: Kernel_function.t -> kind -> Property.t -> unit
(** store the given property of the given kind for the given function *)
val before_translation: unit -> unit
(** to be called just before the main translation *)
(** to be called just before injecting the code *)
val must_translate: Kernel_function.t -> kind -> bool
(** To be called just before transforming a property of the given kind for the
......@@ -52,3 +52,9 @@ val must_translate: Kernel_function.t -> kind -> bool
VERY IMPORTANT: the property of the n-th call to this function exactly
correspond to the n-th pushed property (see {!push}).
@return true if and only if the translation must occur. *)
(*
Local Variables:
compile-command: "make -C ../.."
End:
*)
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