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
)
val warn_unreachable_return : Kernel_function.t -> Cil_datatype.Stmt.t -> unit
val warn_nonterminating_instruction : Kernel_function.t -> Cil_datatype.Stmt.t -> unit
val check_unreachable_returns : Kernel_function.t -> unit
class instr_stmt_collector :
object
.. end
val check_nonterminating_instructions : Cil_types.fundec -> Kernel_function.t -> unit
val run : unit -> unit
val main : unit -> unit