Module Nonterm_run

module Nonterm_run: sig .. end

module Self: Plugin.Register(sig
val name : string
val shortname : string
val help : string
end)
module Enabled: Self.WithOutput(sig
val option_name : string
val help : string
val output_by_default : bool
end)
module Ignore: Self.Kernel_function_set(sig
val option_name : string
val arg_name : string
val help : string
end)
module DeadCode: Self.False(sig
val option_name : string
val help : string
end)
val pretty_stmt_kind : Format.formatter -> Cil_datatype.Stmt.t -> unit
val pp_numbered_stacks : Format.formatter -> Value_types.Callstack.t list -> unit
val warn_nonterminating_statement : Cil_datatype.Stmt.t -> Value_types.Callstack.t list -> unit
val warn_dead_code : Cil_datatype.Stmt.t -> unit
class dead_cc_collector : Kernel_function.t -> object .. end
val warn_unreachable_statement : Cil_datatype.Stmt.t -> unit
class unreachable_stmt_visitor : Kernel_function.t -> Cil_datatype.Stmt.Hptset.t -> object .. end
val check_unreachable_returns : Kernel_function.t -> unit
val check_unreachable_statements : Kernel_function.t ->
to_ignore:Cil_datatype.Stmt.Hptset.t ->
dead_code:bool -> warned_kfs:Kernel_function.Set.t -> unit
val ignore_kf : string -> Cil_datatype.Kf.Set.t -> bool
class stmt_collector : Cil_datatype.Kf.Set.t -> object .. end
val get_callstack_state : after:bool ->
Cil_types.stmt -> Value_types.Callstack.Hashtbl.key -> Db.Value.state option
val collect_nonterminating_statements : Cil_types.fundec ->
Cil_datatype.Kf.Set.t ->
(Cil_datatype.Stmt.Hptset.elt, Value_types.Callstack.Hashtbl.key list)
Hashtbl.t -> Cil_datatype.Stmt.Hptset.t
val run : unit -> unit
val main : unit -> unit