Frama-C:
Plug-ins:
Libraries:

Frama-C API - Cil_const

Smart constructors for some CIL data types

val mk_typ : ?push_qualifiers:bool -> ?tattr:Cil_types.attributes -> Cil_types.typ_node -> Cil_types.typ

Create a typ record, tattr defaults to empty list. push_qualifiers is passed to Ast_types.add_attributes and defaults to true.

  • since 31.0-Gallium
val mk_tvoid : ?tattr:Cil_types.attributes -> unit -> Cil_types.typ

Create a typ record TVoid, tattr defaults to empty list.

  • since 31.0-Gallium

Create a typ record TInt ik, tattr defaults to empty list.

  • since 31.0-Gallium

Create a typ record TFloat fk, tattr defaults to empty list.

  • since 31.0-Gallium

Create a typ record TPtr t, tattr defaults to empty list.

  • since 31.0-Gallium
val mk_tarray : ?push_qualifiers:bool -> ?tattr:Cil_types.attributes -> Cil_types.typ -> Cil_types.exp option -> Cil_types.typ

Create a typ record TArray (t, len), tattr defaults to empty list. push_qualifiers is passed to Ast_types.add_attributes and defaults to true, arrays are not supposed to be qualified.

  • since 31.0-Gallium
val mk_tfun : ?tattr:Cil_types.attributes -> Cil_types.typ -> (string * Cil_types.typ * Cil_types.attributes) list option -> bool -> Cil_types.typ

Create a typ record TFun (rt, args, is_va), tattr defaults to empty list.

  • since 31.0-Gallium

Create a typ record TNamed ti, tattr defaults to empty list.

  • since 31.0-Gallium

Create a typ record TComp ci, tattr defaults to empty list.

  • since 31.0-Gallium

Create a typ record TEnum ei, tattr defaults to empty list.

  • since 31.0-Gallium
val mk_tbuiltin : ?tattr:Cil_types.attributes -> unit -> Cil_types.typ

Create a typ record TBuiltin_va_list, tattr defaults to empty list.

  • since 31.0-Gallium
val voidType : Cil_types.typ

void

val boolType : Cil_types.typ

bool

  • since 30.0-Zinc
val intType : Cil_types.typ

int

  • since 30.0-Zinc
val uintType : Cil_types.typ

unsigned

  • since 30.0-Zinc
val shortType : Cil_types.typ

short

  • since 30.0-Zinc
val ushortType : Cil_types.typ

unsigned short

  • since 30.0-Zinc
val longType : Cil_types.typ

long

  • since 30.0-Zinc
val longLongType : Cil_types.typ

long long

  • since 30.0-Zinc
val ulongType : Cil_types.typ

unsigned long

  • since 30.0-Zinc
val ulongLongType : Cil_types.typ

unsigned long long

  • since 30.0-Zinc
val charType : Cil_types.typ

char

  • since 30.0-Zinc
val scharType : Cil_types.typ

signed char

  • since 30.0-Zinc
val ucharType : Cil_types.typ

unsigned char

  • since 30.0-Zinc
val charPtrType : Cil_types.typ

char *

  • since 30.0-Zinc
val scharPtrType : Cil_types.typ

signed char *

  • since 30.0-Zinc
val ucharPtrType : Cil_types.typ

unsigned char *

  • since 30.0-Zinc
val charConstPtrType : Cil_types.typ

char const *

  • since 30.0-Zinc
val voidPtrType : Cil_types.typ

void *

  • since 30.0-Zinc
val voidConstPtrType : Cil_types.typ

void const *

  • since 30.0-Zinc
val intPtrType : Cil_types.typ

int *

  • since 30.0-Zinc
val uintPtrType : Cil_types.typ

unsigned int *

  • since 30.0-Zinc
val floatType : Cil_types.typ

float

  • since 30.0-Zinc
val doubleType : Cil_types.typ

double

  • since 30.0-Zinc
val longDoubleType : Cil_types.typ

long double

  • since 30.0-Zinc
module Vid : sig ... end
module Sid : sig ... end
module Eid : sig ... end
val set_vid : Cil_types.varinfo -> unit

set the vid to a fresh number.

val copy_with_new_vid : Cil_types.varinfo -> Cil_types.varinfo

returns 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 -> unit

change_varinfo_name vi name changes the name of vi to name. Takes care of renaming the associated logic_var if any.

  • since Oxygen-20120901
val new_raw_id : unit -> int

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.exp option * Cil_types.attributes * Cil_types.location) list option) -> Cil_types.attributes -> Cil_types.compinfo

Creates 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.

  • since 23.0-Vanadium the 4th parameter is a function that returns an option.
val copyCompInfo : ?fresh:bool -> Cil_types.compinfo -> string -> Cil_types.compinfo

Makes 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_var

Create a fresh logical variable giving its name, type and origin.

  • since Fluorine-20130401
val make_logic_var_global : string -> Cil_types.logic_type -> Cil_types.logic_var

Create a new global logic variable

  • since Fluorine-20130401
val make_logic_var_formal : string -> Cil_types.logic_type -> Cil_types.logic_var

Create a new formal logic variable

  • since Fluorine-20130401
val make_logic_var_quant : string -> Cil_types.logic_type -> Cil_types.logic_var

Create a new quantified logic variable

  • since Fluorine-20130401
val make_logic_var_local : string -> Cil_types.logic_type -> Cil_types.logic_var

Create a new local logic variable

  • since Fluorine-20130401
val make_logic_info : string -> Cil_types.logic_info

Create a fresh logical (global) variable giving its name and type.

val make_logic_info_local : string -> Cil_types.logic_info

Create a new local logic variable given its name.

  • since Fluorine-20130401
val make_logic_type : string -> Cil_types.logic_type_info

Create a logic type info given its name.

  • since 30.0-Zinc