Frama-C:
Plug-ins:
Libraries:

Frama-C API - Build

val zero : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val one : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val int : ikind:Frama_c_kernel.Cil_types.ikind -> int -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val float : fkind:Frama_c_kernel.Cil_types.fkind -> float -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val integer : ikind:Frama_c_kernel.Cil_types.ikind -> Frama_c_kernel.Z.t -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val bool : bool -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val cast : Frama_c_kernel.Cil_types.typ -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val add : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val div : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val eq : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val ne : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val index : (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag
val field : (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> Frama_c_kernel.Cil_types.fieldinfo -> (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag
val mem : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag
val var : Frama_c_kernel.Cil_types.varinfo -> (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag
val var_exp : Frama_c_kernel.Cil_types.varinfo -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val var_addr : Frama_c_kernel.Cil_types.varinfo -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val lval : (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag