class annot_visitor : Kernel_function.t ->
object
.. end
Inherits
val mutable skip_set : Cil_datatype.Exp.Set.t
val mutable index_behavior : int
val behavior_names : int Pervasives.ref KfPrecondBehaviors.Hashtbl.t
method private mark_to_skip : Cil_datatype.Exp.Set.elt -> unit
method private must_skip : Cil_datatype.Exp.Set.elt -> bool
method private do_mem_access : unit -> bool
method private do_called_precond : unit -> bool
method private do_div_mod : unit -> bool
method private do_shift : unit -> bool
method private do_signed_overflow : unit -> bool
method private do_unsigned_overflow : unit -> bool
method private do_downcast : unit -> bool
method private do_unsigned_downcast : unit -> bool
method private do_float_to_int : unit -> bool
method private queue_stmt_spec : (Cil_types.term, Cil_types.identified_predicate, Cil_types.identified_term)
Cil_types.spec -> unit
method private mk_new_behavior_name : Kernel_function.t -> Cil_types.funbehavior -> string
method private make_stmt_contract : Kernel_function.t ->
(Cil_types.varinfo * Cil_types.term) list ->
Cil_types.lval option ->
Cil_types.stmt ->
(Cil_types.term, Cil_types.identified_predicate, Cil_types.identified_term)
Cil_types.spec option
method private generate_assertion : 'a 'b. ('a, 'b) Rte.alarm_gen -> 'a -> 'b
method vstmt : Cil_types.stmt -> Cil_types.stmt Cil.visitAction
method vinst : Cil_types.instr -> Cil_types.instr list Cil.visitAction
method vexpr : Cil_datatype.Exp.Set.elt -> Cil_types.exp Cil.visitAction