sig
type reachability
val is_predicate : bool -> Cil_types.predicate -> bool
val is_dead_annot : Cil_types.code_annotation -> bool
val is_dead_code : Cil_types.stmt -> bool
val reachability : Kernel_function.t -> WpReached.reachability
val smoking : WpReached.reachability -> Cil_types.stmt -> bool
val dump :
dir:Datatype.Filepath.t ->
Kernel_function.t -> WpReached.reachability -> unit
val set_doomed : Emitter.t -> WpPropId.prop_id -> unit
val unreachable_proved : int Stdlib.ref
val unreachable_failed : int Stdlib.ref
val set_unreachable : WpPropId.prop_id -> unit
end