Frama-C API - Cil_const
Smart constructors for some CIL data types
val voidType : Cil_types.typvoid
val boolType : Cil_types.typbool
val intType : Cil_types.typint
val uintType : Cil_types.typunsigned
val shortType : Cil_types.typshort
val ushortType : Cil_types.typunsigned short
val longType : Cil_types.typlong
val longLongType : Cil_types.typlong long
val ulongType : Cil_types.typunsigned long
val ulongLongType : Cil_types.typunsigned long long
val charType : Cil_types.typchar
val scharType : Cil_types.typsigned char
val ucharType : Cil_types.typunsigned char
val charPtrType : Cil_types.typchar *
val scharPtrType : Cil_types.typsigned char *
val ucharPtrType : Cil_types.typunisgned char *
val charConstPtrType : Cil_types.typchar const *
val voidPtrType : Cil_types.typvoid *
val voidConstPtrType : Cil_types.typvoid const *
val intPtrType : Cil_types.typint *
val uintPtrType : Cil_types.typunsigned int *
val floatType : Cil_types.typfloat
val doubleType : Cil_types.typdouble
val longDoubleType : Cil_types.typlong double
module Vid : sig ... endmodule Sid : sig ... endmodule Eid : sig ... endval set_vid : Cil_types.varinfo -> unitset the vid to a fresh number.
val copy_with_new_vid : Cil_types.varinfo -> Cil_types.varinforeturns a copy of the varinfo with a fresh vid. If the varinfo has an associated logic var, a copy of the logic var is made as well.
val change_varinfo_name : Cil_types.varinfo -> string -> unitchange_varinfo_name vi name changes the name of vi to name. Takes care of renaming the associated logic_var if any.
Generate a new ID. This will be different than any variable ID that is generated by Cil.makeLocalVar and friends. Must not be used for setting vid: use set_vid instead.
val mkCompInfo : bool -> string -> ?norig:string -> (Cil_types.compinfo -> (string * Cil_types.typ * int option * Cil_types.attributes * Cil_types.location) list option) -> Cil_types.attributes -> Cil_types.compinfoCreates a (potentially recursive) composite type. The arguments are: (1) a boolean indicating whether it is a struct or a union, (2) the name (always non-empty), (3) a function that when given a representation of the structure type constructs the type of the fields recursive type (the first argument is only useful when some fields need to refer to the type of the structure itself), and (4) an optional list of attributes to be associated with the composite type, "None" means that the struct is incomplete.
val copyCompInfo : ?fresh:bool -> Cil_types.compinfo -> string -> Cil_types.compinfoMakes a shallow copy of a Cil_types.compinfo changing the name. It also copies the fields, and makes sure that the copied field points back to the copied compinfo. If fresh is true (the default), it will also give a fresh id to the copy.
val make_logic_var_kind : string -> Cil_types.logic_var_kind -> Cil_types.logic_type -> Cil_types.logic_varCreate a fresh logical variable giving its name, type and origin.
val make_logic_var_global : string -> Cil_types.logic_type -> Cil_types.logic_varCreate a new global logic variable
val make_logic_var_formal : string -> Cil_types.logic_type -> Cil_types.logic_varCreate a new formal logic variable
val make_logic_var_quant : string -> Cil_types.logic_type -> Cil_types.logic_varCreate a new quantified logic variable
val make_logic_var_local : string -> Cil_types.logic_type -> Cil_types.logic_varCreate a new local logic variable
val make_logic_info : string -> Cil_types.logic_infoCreate a fresh logical (global) variable giving its name and type.
val make_logic_info_local : string -> Cil_types.logic_infoCreate a new local logic variable given its name.
val make_logic_type : string -> Cil_types.logic_type_infoCreate a logic type info given its name.