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