Skip to content
Snippets Groups Projects
Commit 691d64ad authored by Thibaut Benjamin's avatar Thibaut Benjamin
Browse files

[e-acsl] correct a comment

parent 7e510b1e
No related branches found
No related tags found
No related merge requests found
......@@ -58,9 +58,8 @@ val clean: loc:location -> Env.t -> t -> Env.t
memory allocated in the C structure will not be freed. *)
val push_pending_register_data: unit -> unit
(** data registering must be delayed after RTE checks to avoid crashes.
[push_pending_register_data] adds a regisration in the pending ones that
will be generated after the RTE. *)
(** [push_pending_register_data] adds a data registration to a stack of pending
data registration to be generated later *)
val do_pending_register_data:
Env.t -> Env.t
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment