Module Keep_status

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.