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
end