module Visit: sig
.. end
Runtime Error annotation generation plugin
val precond_prefix : string
type
orig_lval =
val find_term_to_replace : Cil_types.varinfo -> (Cil_types.varinfo * 'a) list -> 'a option
exception AddrOfFormal
exception NoResult
val treat_tlval : (Cil_types.varinfo * Cil_types.term) list ->
Cil_types.term_lval option ->
orig_lval ->
Cil_types.term_lhost * Cil_types.term_offset ->
Cil_types.term_node Cil.visitAction
val replacement_visitor : Cil_types.logic_label ->
(Cil_types.varinfo * Cil_types.term) list ->
Cil_types.term_lval option -> Cil.genericCilVisitor
val treat_pred : Cil_types.logic_label ->
Cil_types.predicate ->
(Cil_types.varinfo * Cil_types.term) list ->
Cil_types.term_lval option -> Cil_types.predicate
val treat_term : Cil_types.logic_label ->
Cil_types.term ->
(Cil_types.varinfo * Cil_types.term) list ->
Cil_types.term_lval option -> Cil_types.term
exception Untreated_assign
module KfPrecondBehaviors: Datatype.Triple_with_collections
(
Kernel_function
)
(
Kernel_function
)
(
Datatype.String
)
(
sig
end
)
class annot_visitor : Kernel_function.t ->
object
.. end
val rte_annotations : Cil_types.stmt -> Cil_types.code_annotation list
val get_annotations : (Cil.cilVisitor -> 'a -> 'b) ->
Kernel_function.t -> Cil_types.stmt -> 'a -> Cil_types.code_annotation list
val do_stmt_annotations : Kernel_function.t -> Cil_types.stmt -> Cil_types.code_annotation list
val do_exp_annotations : Kernel_function.t ->
Cil_types.stmt -> Cil_types.exp -> Cil_types.code_annotation list
val check_compute : 'a ->
(unit -> bool) ->
('a -> bool) -> ('a -> bool -> 'b) -> (unit -> 'b) -> bool * (unit -> 'b)
val annotate_kf : Kernel_function.t -> unit
val do_precond : Kernel_function.t -> unit
val do_all_rte : Kernel_function.t -> unit
val do_rte : Kernel_function.t -> unit
val compute : unit -> unit