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.
val has_call : bool Pervasives.ref 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