Frama-C API - Export
val export_value : loc:Frama_c_kernel.Cil_types.location -> ?name:string list -> Frama_c_kernel.Cil_types.lval -> Results.request -> Frama_c_kernel.Cil_types.predicateGenerates a predicate characterizing the domain of the l-value.
val export_stmt : ?callstack:Callstack.t -> ?name:string list -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.predicate listGenerates a collection of predicates for each l-value that is read by the instruction or the branching condition of the statement. Other kinds of statements, like loops, blocks and exceptions are not visited.
More precisely, for set and call instructions: the written l-values from left-hand-side are not visited, but their inner l-values are visited; any l-value from the right-hand-side of the instruction is also visited.
val emitter : Frama_c_kernel.Emitter.tEmitter used for generating domain assertions.
val generator : unit -> Frama_c_kernel.Visitor.frama_c_inplaceCreates a visitor that can be used to generate new annotations for all visited instructions. The generated assertions are associated with the local emitter. They are all assigned a valid status by Analysis.emitter.
val cleaner : unit -> Frama_c_kernel.Visitor.frama_c_inplaceCreates a visitor that can be used to remove all generated annotations from emitter. This will also remove their associated status.