sig
  val annotate_kf : Cil_types.kernel_function -> unit
  val compute : unit -> unit
  val do_precond : Cil_types.kernel_function -> unit
  val do_all_rte : Cil_types.kernel_function -> unit
  val do_rte : Cil_types.kernel_function -> unit
  val rte_annotations : Cil_types.stmt -> Cil_types.code_annotation list
  val do_stmt_annotations :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Cil_types.code_annotation list
  val do_exp_annotations :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Cil_types.exp -> Cil_types.code_annotation list
end