Class Aorai_visitors.visit_adding_pre_post_from_buch

class visit_adding_pre_post_from_buch : bool -> object .. end

This visitor adds a specification to each function and to each loop, according to specifications stored into Data_for_aorai.

Inherits
val has_call : bool Stdlib.ref Stdlib.Stack.t
method private enter_block : unit -> unit
method private call : unit -> unit
method private leave_block : unit -> bool
method vfunc : Cil_types.fundec -> Cil_types.fundec Cil.visitAction
method vglob_aux : Cil_types.global -> Cil_types.global list Cil.visitAction
method vstmt_aux : Cil_datatype.Stmt.t -> Cil_datatype.Stmt.t Cil.visitAction
method vinst : Cil_types.instr -> Cil_types.instr list Cil.visitAction