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 integer : ?ikind:Frama_c_kernel.Cil_types.ikind -> Frama_c_kernel.Z.t -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag

Builds an integer constant. If ikind is provided, truncates the integer if it does not fit. If ikind is not provided, uses type int if possible, or the largest signed or unsigned integer type which can represent the integer.

  • raises Cil.Not_representable

    if no ikind is provided and the integer does not fit in any integer type.

val int : ?ikind:Frama_c_kernel.Cil_types.ikind -> int -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag

Same as integer above for an ocaml int.

val float : fkind:Frama_c_kernel.Cil_types.fkind -> float -> 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 sub : 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