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.Filled_string_set(sig
val option_name : string
val arg_name : string
val help : string
val default : Datatype.String.Set.t
end)
module DeadCode: Self.False(sig
val option_name : string
val help : string
end)
val pretty_stmt_kind : Stdlib.Format.formatter -> Cil_datatype.Stmt.t -> unit
val pp_numbered_stacks : Stdlib.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 : Ignore.elt -> bool
class stmt_collector : 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.Stmt.Hptset.elt, Value_types.Callstack.Hashtbl.key list)
Stdlib.Hashtbl.t -> Cil_datatype.Stmt.Hptset.t
val cmp_callstacks_aux : (Kernel_function.t * Cil_datatype.Kinstr.t) list ->
(Kernel_function.t * Cil_datatype.Kinstr.t) list -> int
val cmp_callstacks : (Kernel_function.t * Cil_datatype.Kinstr.t) list ->
(Kernel_function.t * Cil_datatype.Kinstr.t) list -> int
val run : unit -> unit
val main : unit -> unit