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 : 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 : 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)
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