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).