module Keep_status: sig
.. end
Make the property statuses of the initial project accessible when
doing the main translation
type
kind =
| |
K_Assert |
| |
K_Invariant |
| |
K_Variant |
| |
K_StmtSpec |
| |
K_Allocation |
| |
K_Assigns |
| |
K_Decreases |
| |
K_Terminates |
| |
K_Complete |
| |
K_Disjoint |
| |
K_Requires |
| |
K_Ensures |
val clear : unit -> unit
to be called before any program transformation
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
val must_translate : Kernel_function.t -> kind -> bool
To be called just before transforming a property of the given kind for the
given function.
VERY IMPORTANT: the property of the n-th call to this function exactly
correspond to the n-th pushed property (see
Keep_status.push
).
Returns true if and only if the translation must occur.