sig
module Print_api : sig val run : string -> unit end
module Aorai : sig val run : unit -> unit end
module RteGen :
sig
val do_all_rte : Cil_datatype.Kf.t -> unit
val stmt_annotations :
Cil_datatype.Kf.t ->
Cil_datatype.Stmt.t -> Cil_datatype.Code_annotation.t list
val do_precond : Cil_datatype.Kf.t -> unit
val exp_annotations :
Cil_datatype.Kf.t ->
Cil_datatype.Stmt.t ->
Cil_datatype.Exp.t -> Cil_datatype.Code_annotation.t list
val emitter : Emitter.t
val get_rte_annotations :
Cil_datatype.Stmt.t -> Cil_datatype.Code_annotation.t list
end
module Security_slicing :
sig
val get_forward_component :
Cil_datatype.Stmt.t -> Cil_datatype.Stmt.t list
val impact_analysis :
Cil_datatype.Kf.t -> Cil_datatype.Stmt.t -> Cil_datatype.Stmt.t list
val get_direct_component :
Cil_datatype.Stmt.t -> Cil_datatype.Stmt.t list
val get_indirect_backward_component :
Cil_datatype.Stmt.t -> Cil_datatype.Stmt.t list
end
module Wp :
sig
module Wpo :
sig
type prover
type result
type po
val file_for_log_proof :
Dynamic_plugins.Wp.Wpo.po ->
Dynamic_plugins.Wp.Wpo.prover -> string * string
val prover_of_name : string -> Dynamic_plugins.Wp.Wpo.prover option
val iter_on_goals : (Dynamic_plugins.Wp.Wpo.po -> unit) -> unit
val is_valid : Dynamic_plugins.Wp.Wpo.result -> bool
val goals_of_property :
Property.t -> Dynamic_plugins.Wp.Wpo.po list
val get_result :
Dynamic_plugins.Wp.Wpo.po ->
Dynamic_plugins.Wp.Wpo.prover -> Dynamic_plugins.Wp.Wpo.result
val get_gid : Dynamic_plugins.Wp.Wpo.po -> string
val get_property : Dynamic_plugins.Wp.Wpo.po -> Property.t
end
val wp_compute_kf :
Cil_datatype.Kf.t option -> string list -> string list -> unit
val wp_clear_session : unit -> unit
val wp_iter_session : (Dynamic_plugins.Wp.Wpo.po -> unit) -> unit
val wp_compute :
Cil_datatype.Kf.t option -> string list -> Property.t option -> unit
val wp_end_session : unit -> unit
val wp_compute_call : Cil_datatype.Stmt.t -> unit
val run : unit -> unit
val wp_clear : unit -> unit
val wp_begin_session : unit -> unit
val wp_compute_ip : Property.t -> unit
end
module Report : sig val print : unit -> unit end
module Obfuscator : sig val force_run : unit -> unit end
module Semantic_callgraph :
sig
val iter_on_callers :
(Cil_datatype.Kf.t -> unit) -> Cil_datatype.Kf.t -> unit
end
end