Module Injector

module Injector: sig .. end
The E-ACSL main instrumentation step.

In the block outer_block in the function kf, this function finds the innermost last statement and insert the list of statements returned by last_stmts. The function last_stmts receives an optional argument ?return_stmt with the innermost return statement if it exists. In that case the function needs to return this statement as the last statement.


val inject : unit -> unit
Inject all the necessary pieces of code for monitoring the program annotations.