Module Cil

module Cil: sig .. end

CIL main API.

CIL original API documentation is available as an html version at http://manju.cs.berkeley.edu/cil.


Builtins management

module Frama_c_builtins: State_builder.Hashtbl  with type key = string and type data = Cil_types.varinfo

This module associates the name of a built-in function that might be used during elaboration with the corresponding varinfo.

val is_builtin : Cil_types.varinfo -> bool
val is_unused_builtin : Cil_types.varinfo -> bool
val is_special_builtin : string -> bool
val add_special_builtin : string -> unit

register a new special built-in function

val add_special_builtin_family : (string -> bool) -> unit

register a new family of special built-in functions.

val init_builtins : unit -> unit

initialize the C built-ins. Should be called once per project, after the machine has been set.

val initCIL : initLogicBuiltins:(unit -> unit) -> Cil_types.mach -> unit

Call this function to perform some initialization, and only after you have set Cil.msvcMode. initLogicBuiltins is the function to call to init logic builtins. The Machdeps argument is a description of the hardware platform and of the compiler used.

Customization

type theMachine = private {
   mutable useLogicalOperators : bool; (*

Whether to use the logical operands LAnd and LOr. By default, do not use them because they are unlike other expressions and do not evaluate both of their operands

*)
   mutable theMachine : Cil_types.mach;
   mutable lowerConstants : bool; (*

Do lower constants (default true)

*)
   mutable insertImplicitCasts : bool; (*

Do insert implicit casts (default true)

*)
   mutable underscore_name : bool; (*

Whether the compiler generates assembly labels by prepending "_" to the identifier. That is, will function foo() have the label "foo", or "_foo"?

*)
   mutable stringLiteralType : Cil_types.typ;
   mutable upointKind : Cil_types.ikind; (*

An unsigned integer type that fits pointers.

*)
   mutable upointType : Cil_types.typ;
   mutable wcharKind : Cil_types.ikind; (*

An integer type that fits wchar_t.

*)
   mutable wcharType : Cil_types.typ;
   mutable ptrdiffKind : Cil_types.ikind; (*

An integer type that fits ptrdiff_t.

*)
   mutable ptrdiffType : Cil_types.typ;
   mutable typeOfSizeOf : Cil_types.typ; (*

An integer type that is the type of sizeof.

*)
   mutable kindOfSizeOf : Cil_types.ikind; (*

The integer kind of Cil.typeOfSizeOf.

*)
}
val theMachine : theMachine

Current machine description

val selfMachine : State.t
val selfMachine_is_computed : ?project:Project.project -> unit -> bool

whether current project has set its machine description.

val msvcMode : unit -> bool
val gccMode : unit -> bool

Values for manipulating globals

val emptyFunctionFromVI : Cil_types.varinfo -> Cil_types.fundec

Make an empty function from an existing global varinfo.

val emptyFunction : string -> Cil_types.fundec

Make an empty function

val setFormals : Cil_types.fundec -> Cil_types.varinfo list -> unit

Update the formals of a fundec and make sure that the function type has the same information. Will copy the name as well into the type.

val getReturnType : Cil_types.typ -> Cil_types.typ

Takes as input a function type (or a typename on it) and return its return type.

val setReturnTypeVI : Cil_types.varinfo -> Cil_types.typ -> unit

Change the return type of the function passed as 1st argument to be the type passed as 2nd argument.

val setReturnType : Cil_types.fundec -> Cil_types.typ -> unit
val setFunctionType : Cil_types.fundec -> Cil_types.typ -> unit

Set the types of arguments and results as given by the function type passed as the second argument. Will not copy the names from the function type to the formals

val setFunctionTypeMakeFormals : Cil_types.fundec -> Cil_types.typ -> unit

Set the type of the function and make formal arguments for them

val setMaxId : Cil_types.fundec -> unit

Update the smaxid after you have populated with locals and formals (unless you constructed those using Cil.makeLocalVar or Cil.makeTempVar.

val selfFormalsDecl : State.t

state of the table associating formals to each prototype.

val makeFormalsVarDecl : ?ghost:bool ->
string * Cil_types.typ * Cil_types.attributes -> Cil_types.varinfo

creates a new varinfo for the parameter of a prototype. By default, this formal variable is not ghost.

val setFormalsDecl : Cil_types.varinfo -> Cil_types.typ -> unit

Update the formals of a function declaration from its identifier and its type. For a function definition, use Cil.setFormals. Do nothing if the type is not a function type or if the list of argument is empty.

val removeFormalsDecl : Cil_types.varinfo -> unit

remove a binding from the table.

val unsafeSetFormalsDecl : Cil_types.varinfo -> Cil_types.varinfo list -> unit

replace formals of a function declaration with the given list of varinfo.

val iterFormalsDecl : (Cil_types.varinfo -> Cil_types.varinfo list -> unit) -> unit

iterate the given function on declared prototypes.

val getFormalsDecl : Cil_types.varinfo -> Cil_types.varinfo list

Get the formals of a function declaration registered with Cil.setFormalsDecl.

val dummyFile : Cil_types.file

A dummy file

val iterGlobals : Cil_types.file -> (Cil_types.global -> unit) -> unit

Iterate over all globals, including the global initializer

val foldGlobals : Cil_types.file -> ('a -> Cil_types.global -> 'a) -> 'a -> 'a

Fold over all globals, including the global initializer

val mapGlobals : Cil_types.file -> (Cil_types.global -> Cil_types.global) -> unit

Map over all globals, including the global initializer and change things in place

val findOrCreateFunc : Cil_types.file -> string -> Cil_types.typ -> Cil_types.varinfo

Find a function or function prototype with the given name in the file. If it does not exist, create a prototype with the given type, and return the new varinfo. This is useful when you need to call a libc function whose prototype may or may not already exist in the file.

Because the new prototype is added to the start of the file, you shouldn't refer to any struct or union types in the function type.

val new_exp : loc:Cil_types.location -> Cil_types.exp_node -> Cil_types.exp

creates an expression with a fresh id

val copy_exp : Cil_types.exp -> Cil_types.exp

performs a deep copy of an expression (especially, avoid eid sharing).

val dummy_exp : Cil_types.exp_node -> Cil_types.exp

creates an expression with a dummy id. Use with caution, i.e. not on expressions that may be put in the AST.

val is_case_label : Cil_types.label -> bool

Return true on case and default labels, false otherwise.

val pushGlobal : Cil_types.global ->
types:Cil_types.global list Stdlib.ref ->
variables:Cil_types.global list Stdlib.ref -> unit

CIL keeps the types at the beginning of the file and the variables at the end of the file. This function will take a global and add it to the corresponding stack. Its operation is actually more complicated because if the global declares a type that contains references to variables (e.g. in sizeof in an array length) then it will also add declarations for the variables to the types stack

val invalidStmt : Cil_types.stmt

An empty statement. Used in pretty printing

module Builtin_functions: State_builder.Hashtbl  with type key = string
                         and type data = typ * typ list * bool

A list of the built-in functions for the current compiler (GCC or MSVC, depending on !msvcMode).

val builtinLoc : Cil_types.location

This is used as the location of the prototypes of builtin functions.

val range_loc : Cil_types.location -> Cil_types.location -> Cil_types.location

Returns a location that ranges over the two locations in arguments.

Values for manipulating initializers

val makeZeroInit : loc:Cil_types.location -> Cil_types.typ -> Cil_types.init

Make a initializer for zero-ing a data type

val foldLeftCompound : implicit:bool ->
doinit:(Cil_types.offset -> Cil_types.init -> Cil_types.typ -> 'a -> 'a) ->
ct:Cil_types.typ ->
initl:(Cil_types.offset * Cil_types.init) list -> acc:'a -> 'a

Fold over the list of initializers in a Compound (not also the nested ones). doinit is called on every present initializer, even if it is of compound type. The parameters of doinit are: the offset in the compound (this is Field(f,NoOffset) or Index(i,NoOffset)), the initializer value, expected type of the initializer value, accumulator. In the case of arrays there might be missing zero-initializers at the end of the list. These are scanned only if implicit is true. This is much like List.fold_left except we also pass the type of the initializer.

This is a good way to use it to scan even nested initializers :

  let rec myInit (lv: lval) (i: init) (acc: 'a) : 'a =
    match i with
      | SingleInit e -> (* ... do something with [lv] and [e] and [acc] ... *)
      | CompoundInit (ct, initl) ->
         foldLeftCompound ~implicit:false
           ~doinit:(fun off' i' _typ acc' ->
                      myInit (addOffsetLval off' lv) i' acc')
           ~ct
           ~initl
           ~acc

Values for manipulating types

val voidType : Cil_types.typ

void

val isVoidType : Cil_types.typ -> bool

is the given type "void"?

val isVoidPtrType : Cil_types.typ -> bool

is the given type "void *"?

val intType : Cil_types.typ

int

val uintType : Cil_types.typ

unsigned int

val longType : Cil_types.typ

long

val longLongType : Cil_types.typ

long long

val ulongType : Cil_types.typ

unsigned long

val ulongLongType : Cil_types.typ

unsigned long long

val uint16_t : unit -> Cil_types.typ

Any unsigned integer type of size 16 bits. It is equivalent to the ISO C uint16_t type but without using the corresponding header. Shall not be called if not such type exists in the current architecture.

val uint32_t : unit -> Cil_types.typ

Any unsigned integer type of size 32 bits. It is equivalent to the ISO C uint32_t type but without using the corresponding header. Shall not be called if not such type exists in the current architecture.

val uint64_t : unit -> Cil_types.typ

Any unsigned integer type of size 64 bits. It is equivalent to the ISO C uint64_t type but without using the corresponding header. Shall not be called if no such type exists in the current architecture.

val charType : Cil_types.typ

char

val scharType : Cil_types.typ
val ucharType : Cil_types.typ
val charPtrType : Cil_types.typ

char *

val scharPtrType : Cil_types.typ
val ucharPtrType : Cil_types.typ
val charConstPtrType : Cil_types.typ

char const *

val voidPtrType : Cil_types.typ

void *

val voidConstPtrType : Cil_types.typ

void const *

val intPtrType : Cil_types.typ

int *

val uintPtrType : Cil_types.typ

unsigned int *

val floatType : Cil_types.typ

float

val doubleType : Cil_types.typ

double

val longDoubleType : Cil_types.typ

long double

val isSignedInteger : Cil_types.typ -> bool
val isUnsignedInteger : Cil_types.typ -> bool
val missingFieldName : string

This is a constant used as the name of an unnamed bitfield. These fields do not participate in initialization and their name is not printed.

val compFullName : Cil_types.compinfo -> string

Get the full name of a comp, including the 'struct' or 'union' prefix

val isCompleteType : ?allowZeroSizeArrays:bool -> Cil_types.typ -> bool

Returns true if this is a complete type. This means that sizeof(t) makes sense. Incomplete types are not yet defined structures and empty arrays.

allowZeroSizeArrays : indicates whether arrays of size 0 (a gcc extension) are considered as complete. Default value depends on the current machdep.
val has_flexible_array_member : Cil_types.typ -> bool

true iff the given type is a struct whose last field is a flexible array member. When in gcc mode, a zero-sized array is identified with a FAM for this purpose.

val unrollType : Cil_types.typ -> Cil_types.typ

Unroll a type until it exposes a non TNamed. Will collect all attributes appearing in TNamed!!!

val unrollTypeDeep : Cil_types.typ -> Cil_types.typ

Unroll all the TNamed in a type (even under type constructors such as TPtr, TFun or TArray. Does not unroll the types of fields in TComp types. Will collect all attributes

val separateStorageModifiers : Cil_types.attribute list ->
Cil_types.attribute list * Cil_types.attribute list

Separate out the storage-modifier name attributes

val arithmeticConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ

returns the type of the result of an arithmetic operator applied to values of the corresponding input types.

val integralPromotion : Cil_types.typ -> Cil_types.typ

performs the usual integral promotions mentioned in C reference manual.

val isAnyCharType : Cil_types.typ -> bool

True if the argument is a character type (i.e. plain, signed or unsigned)

val isCharType : Cil_types.typ -> bool

True if the argument is a plain character type (but neither signed char nor unsigned char).

val isShortType : Cil_types.typ -> bool

True if the argument is a short type (i.e. signed or unsigned)

val isAnyCharPtrType : Cil_types.typ -> bool

True if the argument is a pointer to a character type (i.e. plain, signed or unsigned).

val isCharPtrType : Cil_types.typ -> bool

True if the argument is a pointer to a plain character type (but neither signed char nor unsigned char).

val isCharConstPtrType : Cil_types.typ -> bool

True if the argument is a pointer to a constant character type, e.g. a string literal.

val isAnyCharArrayType : Cil_types.typ -> bool

True if the argument is an array of a character type (i.e. plain, signed or unsigned)

val isCharArrayType : Cil_types.typ -> bool

True if the argument is an array of a character type (i.e. plain, signed or unsigned)

val isIntegralType : Cil_types.typ -> bool

True if the argument is an integral type (i.e. integer or enum)

val isBoolType : Cil_types.typ -> bool

True if the argument is _Bool

val isLogicPureBooleanType : Cil_types.logic_type -> bool

True if the argument is _Bool or boolean.

val isIntegralOrPointerType : Cil_types.typ -> bool

True if the argument is an integral or pointer type.

val isLogicIntegralType : Cil_types.logic_type -> bool

True if the argument is an integral type (i.e. integer or enum), either C or mathematical one.

val isLogicBooleanType : Cil_types.logic_type -> bool

True if the argument is a boolean type, either integral C type or mathematical boolean one.

val isFloatingType : Cil_types.typ -> bool

True if the argument is a floating point type.

val isLogicFloatType : Cil_types.logic_type -> bool

True if the argument is a floating point type.

val isLogicRealOrFloatType : Cil_types.logic_type -> bool

True if the argument is a C floating point type or logic 'real' type.

val isLogicRealType : Cil_types.logic_type -> bool

True if the argument is the logic 'real' type.

val isArithmeticType : Cil_types.typ -> bool

True if the argument is an arithmetic type (i.e. integer, enum or floating point

val isScalarType : Cil_types.typ -> bool

True if the argument is a scalar type (i.e. integral, enum, floating point or pointer

val isArithmeticOrPointerType : Cil_types.typ -> bool
Deprecated.22.0-Titanium use isScalarType instead

alias of isScalarType.

val isLogicArithmeticType : Cil_types.logic_type -> bool

True if the argument is a logic arithmetic type (i.e. integer, enum or floating point, either C or mathematical one.

val isFunctionType : Cil_types.typ -> bool

True if the argument is a function type

val isLogicFunctionType : Cil_types.logic_type -> bool

True if the argument is the logic function type. Expands the logic type definition if necessary.

val isPointerType : Cil_types.typ -> bool

True if the argument is a pointer type.

val isFunPtrType : Cil_types.typ -> bool

True if the argument is a function pointer type.

val isLogicFunPtrType : Cil_types.logic_type -> bool

True if the argument is the logic function pointer type. Expands the logic type definition if necessary.

val isTypeTagType : Cil_types.logic_type -> bool

True if the argument is the type for reified C types.

val isVariadicListType : Cil_types.typ -> bool

True if the argument denotes the type of ... in a variadic function.

val argsToList : (string * Cil_types.typ * Cil_types.attributes) list option ->
(string * Cil_types.typ * Cil_types.attributes) list

Obtain the argument list ([] if None).

val argsToPairOfLists : (string * Cil_types.typ * Cil_types.attributes) list option ->
(string * Cil_types.typ * Cil_types.attributes) list *
(string * Cil_types.typ * Cil_types.attributes) list
val isArrayType : Cil_types.typ -> bool

True if the argument is an array type

val isStructOrUnionType : Cil_types.typ -> bool

True if the argument is a struct of union type

exception LenOfArray

Raised when Cil.lenOfArray fails either because the length is None or because it is a non-constant expression

val lenOfArray : Cil_types.exp option -> int

Call to compute the array length as present in the array type, to an integer. Raises Cil.LenOfArray if not able to compute the length, such as when there is no length or the length is not a constant.

val lenOfArray64 : Cil_types.exp option -> Integer.t
val getCompField : Cil_types.compinfo -> string -> Cil_types.fieldinfo

Return a named fieldinfo in compinfo, or raise Not_found

type existsAction = 
| ExistsTrue (*

We have found it

*)
| ExistsFalse (*

Stop processing this branch

*)
| ExistsMaybe (*

This node is not what we are looking for but maybe its successors are

*)

A datatype to be used in conjunction with existsType

val existsType : (Cil_types.typ -> existsAction) -> Cil_types.typ -> bool

Scans a type by applying the function on all elements. When the function returns ExistsTrue, the scan stops with true. When the function returns ExistsFalse then the current branch is not scanned anymore. Care is taken to apply the function only once on each composite type, thus avoiding circularity. When the function returns ExistsMaybe then the types that construct the current type are scanned (e.g. the base type for TPtr and TArray, the type of fields for a TComp, etc).

val splitFunctionType : Cil_types.typ ->
Cil_types.typ * (string * Cil_types.typ * Cil_types.attributes) list option *
bool * Cil_types.attributes

Given a function type split it into return type, arguments, is_vararg and attributes. An error is raised if the type is not a function type

Same as Cil.splitFunctionType but takes a varinfo. Prints a nicer error message if the varinfo is not for a function

val splitFunctionTypeVI : Cil_types.varinfo ->
Cil_types.typ * (string * Cil_types.typ * Cil_types.attributes) list option *
bool * Cil_types.attributes

LVALUES

val makeVarinfo : ?source:bool ->
?temp:bool ->
?referenced:bool ->
?ghost:bool ->
?loc:Cil_datatype.Location.t ->
bool -> bool -> string -> Cil_types.typ -> Cil_types.varinfo

Make a varinfo. Use this (rarely) to make a raw varinfo. Use other functions to make locals (Cil.makeLocalVar or Cil.makeFormalVar or Cil.makeTempVar) and globals (Cil.makeGlobalVar). Note that this function will assign a new identifier. The temp argument defaults to false, and corresponds to the vtemp field in type Cil_types.varinfo. The source argument defaults to true, and corresponds to the field vsource . The referenced argument defaults to false, and corresponds to the field vreferenced . The ghost argument defaults to false, and corresponds to the field vghost . The loc argument defaults to Location.unknown, and corresponds to the field vdecl . The first unnamed argument specifies whether the varinfo is for a global and the second is for formals.

val makeFormalVar : Cil_types.fundec ->
?ghost:bool ->
?where:string ->
?loc:Cil_datatype.Location.t -> string -> Cil_types.typ -> Cil_types.varinfo

Make a formal variable for a function declaration. Insert it in both the sformals and the type of the function. You can optionally specify where to insert this one. If where = "^" then it is inserted first. If where = "$" then it is inserted last. Otherwise where must be the name of a formal after which to insert this. By default it is inserted at the end.

The ghost parameter indicates if the variable should be inserted in the list of formals or ghost formals. By default, it takes the ghost status of the function where the formal is inserted. Note that:

val makeLocalVar : Cil_types.fundec ->
?scope:Cil_types.block ->
?temp:bool ->
?referenced:bool ->
?insert:bool ->
?ghost:bool ->
?loc:Cil_datatype.Location.t -> string -> Cil_types.typ -> Cil_types.varinfo

Make a local variable and add it to a function's slocals and to the given block (only if insert = true, which is the default). Make sure you know what you are doing if you set insert=false. temp is passed to Cil.makeVarinfo. The variable is attached to the toplevel block if scope is not specified. If the name passed as argument already exists within the function, a fresh name will be generated for the varinfo.

val refresh_local_name : Cil_types.fundec -> Cil_types.varinfo -> unit

if needed, rename the given varinfo so that its vname does not clash with the one of a local or formal variable of the given function.

val makeTempVar : Cil_types.fundec ->
?insert:bool ->
?ghost:bool ->
?name:string ->
?descr:string ->
?descrpure:bool ->
?loc:Cil_datatype.Location.t -> Cil_types.typ -> Cil_types.varinfo

Make a temporary variable and add it to a function's slocals. The name of the temporary variable will be generated based on the given name hint so that to avoid conflicts with other locals. Optionally, you can give the variable a description of its contents and its location. Temporary variables are always considered as generated variables. If insert is true (the default), the variable will be inserted among other locals of the function. The value for insert should only be changed if you are completely sure this is not useful.

val makeGlobalVar : ?source:bool ->
?temp:bool ->
?referenced:bool ->
?ghost:bool ->
?loc:Cil_datatype.Location.t -> string -> Cil_types.typ -> Cil_types.varinfo

Make a global variable. Your responsibility to make sure that the name is unique. source defaults to true. temp defaults to false.

val copyVarinfo : Cil_types.varinfo -> string -> Cil_types.varinfo

Make a shallow copy of a varinfo and assign a new identifier. If the original varinfo has an associated logic var, it is copied too and associated to the copied varinfo

val update_var_type : Cil_types.varinfo -> Cil_types.typ -> unit

Changes the type of a varinfo and of its associated logic var if any.

val isBitfield : Cil_types.lval -> bool

Is an lvalue a bitfield?

val lastOffset : Cil_types.offset -> Cil_types.offset

Returns the last offset in the chain.

val addOffsetLval : Cil_types.offset -> Cil_types.lval -> Cil_types.lval

Add an offset at the end of an lvalue. Make sure the type of the lvalue and the offset are compatible.

val addOffset : Cil_types.offset -> Cil_types.offset -> Cil_types.offset

addOffset o1 o2 adds o1 to the end of o2.

val removeOffsetLval : Cil_types.lval -> Cil_types.lval * Cil_types.offset

Remove ONE offset from the end of an lvalue. Returns the lvalue with the trimmed offset and the final offset. If the final offset is NoOffset then the original lval did not have an offset.

val removeOffset : Cil_types.offset -> Cil_types.offset * Cil_types.offset

Remove ONE offset from the end of an offset sequence. Returns the trimmed offset and the final offset. If the final offset is NoOffset then the original lval did not have an offset.

val typeOfLval : Cil_types.lval -> Cil_types.typ

Compute the type of an lvalue

val typeOfLhost : Cil_types.lhost -> Cil_types.typ

Compute the type of an lhost (with no offset)

val typeOfTermLval : Cil_types.term_lval -> Cil_types.logic_type

Equivalent to typeOfLval for terms.

val typeOffset : Cil_types.typ -> Cil_types.offset -> Cil_types.typ

Compute the type of an offset from a base type

val typeTermOffset : Cil_types.logic_type -> Cil_types.term_offset -> Cil_types.logic_type

Equivalent to typeOffset for terms.

val typeOfInit : Cil_types.init -> Cil_types.typ

Compute the type of an initializer

val is_modifiable_lval : Cil_types.lval -> bool

indicates whether the given lval is a modifiable lvalue in the sense of the C standard 6.3.2.1§1.

Values for manipulating expressions

val zero : loc:Cil_datatype.Location.t -> Cil_types.exp

0

val one : loc:Cil_datatype.Location.t -> Cil_types.exp

1

val mone : loc:Cil_datatype.Location.t -> Cil_types.exp

-1

val kinteger64 : loc:Cil_types.location ->
?repr:string -> ?kind:Cil_types.ikind -> Integer.t -> Cil_types.exp

Construct an integer of a given kind without literal representation. Truncate the integer if kind is given, and the integer does not fit inside the type. The integer can have an optional literal representation repr.

val kinteger : loc:Cil_types.location -> Cil_types.ikind -> int -> Cil_types.exp

Construct an integer of a given kind. Converts the integer to int64 and then uses kinteger64. This might truncate the value if you use a kind that cannot represent the given integer. This can only happen for one of the Char or Short kinds

val integer : loc:Cil_types.location -> int -> Cil_types.exp

Construct an integer of kind IInt. You can use this always since the OCaml integers are 31 bits and are guaranteed to fit in an IInt

val kfloat : loc:Cil_types.location -> Cil_types.fkind -> float -> Cil_types.exp

Constructs a floating point constant.

val isInteger : Cil_types.exp -> Integer.t option

True if the given expression is a (possibly cast'ed) character or an integer constant

val isConstant : Cil_types.exp -> bool

True if the expression is a compile-time constant

val isIntegerConstant : Cil_types.exp -> bool

True if the expression is a compile-time integer constant

val isConstantOffset : Cil_types.offset -> bool

True if the given offset contains only field names or constant indices.

val isZero : Cil_types.exp -> bool

True if the given expression is a (possibly cast'ed) integer or character constant with value zero

val isLogicZero : Cil_types.term -> bool

True if the term is the constant 0

val isLogicNull : Cil_types.term -> bool

True if the given term is \null or a constant null pointer

val no_op_coerce : Cil_types.logic_type -> Cil_types.term -> bool

no_op_coerce typ term is true iff converting term to typ does not modify its value.

val reduce_multichar : Cil_types.typ -> int64 list -> int64

gives the value of a wide char literal.

val interpret_character_constant : int64 list -> Cil_types.constant * Cil_types.typ

gives the value of a char literal.

val charConstToInt : char -> Integer.t

Given the character c in a (CChr c), sign-extend it to 32 bits. (This is the official way of interpreting character constants, according to ISO C 6.4.4.4.10, which says that character constants are chars cast to ints) Returns CInt64(sign-extended c, IInt, None)

val charConstToIntConstant : char -> Cil_types.constant
val constFold : bool -> Cil_types.exp -> Cil_types.exp

Do constant folding on an expression. If the first argument is true then will also compute compiler-dependent expressions such as sizeof. See also Cil.constFoldVisitor, which will run constFold on all expressions in a given AST node.

val constFoldToInt : ?machdep:bool -> Cil_types.exp -> Integer.t option

Do constant folding on the given expression, just as constFold would. The resulting integer value, if the const-folding was complete, is returned. The machdep optional parameter, which is set to true by default, forces the simplification of architecture-dependent expressions.

val constFoldTermNodeAtTop : Cil_types.term_node -> Cil_types.term_node

Do constant folding on an term at toplevel only. This uses compiler-dependent informations and will remove all sizeof and alignof.

val constFoldTerm : bool -> Cil_types.term -> Cil_types.term

Do constant folding on an term. If the first argument is true then will also compute compiler-dependent expressions such as sizeof and alignof.

val constFoldOffset : bool -> Cil_types.offset -> Cil_types.offset

Do constant folding on a Cil_types.offset. If the second argument is true then will also compute compiler-dependent expressions such as sizeof.

val constFoldBinOp : loc:Cil_types.location ->
bool ->
Cil_types.binop ->
Cil_types.exp -> Cil_types.exp -> Cil_types.typ -> Cil_types.exp

Do constant folding on a binary operation. The bulk of the work done by constFold is done here. If the second argument is true then will also compute compiler-dependent expressions such as sizeof.

val compareConstant : Cil_types.constant -> Cil_types.constant -> bool

true if the two constant are equal.

val increm : Cil_types.exp -> int -> Cil_types.exp

Increment an expression. Can be arithmetic or pointer type

val increm64 : Cil_types.exp -> Integer.t -> Cil_types.exp

Increment an expression. Can be arithmetic or pointer type

val var : Cil_types.varinfo -> Cil_types.lval

Makes an lvalue out of a given variable

val evar : ?loc:Cil_types.location -> Cil_types.varinfo -> Cil_types.exp

Creates an expr representing the variable.

val mkAddrOf : loc:Cil_types.location -> Cil_types.lval -> Cil_types.exp

Make an AddrOf. Given an lvalue of type T will give back an expression of type ptr(T). It optimizes somewhat expressions like "& v" and "& v0"

val mkAddrOfVi : Cil_types.varinfo -> Cil_types.exp

Creates an expression corresponding to "&v".

val mkAddrOrStartOf : loc:Cil_types.location -> Cil_types.lval -> Cil_types.exp

Like mkAddrOf except if the type of lval is an array then it uses StartOf. This is the right operation for getting a pointer to the start of the storage denoted by lval.

val mkMem : addr:Cil_types.exp -> off:Cil_types.offset -> Cil_types.lval

Make a Mem, while optimizing AddrOf. The type of the addr must be TPtr(t) and the type of the resulting lval is t. Note that in CIL the implicit conversion between an array and the pointer to the first element does not apply. You must do the conversion yourself using StartOf

val mkBinOp : loc:Cil_types.location ->
Cil_types.binop -> Cil_types.exp -> Cil_types.exp -> Cil_types.exp

makes a binary operation and performs const folding. Inserts casts between arithmetic types as needed, or between pointer types, but do not attempt to cast pointer to int or vice-versa. Use appropriate binop (PlusPI & friends) for that.

val mkBinOp_safe_ptr_cmp : loc:Cil_types.location ->
Cil_types.binop -> Cil_types.exp -> Cil_types.exp -> Cil_types.exp

same as Cil.mkBinOp, but performs a systematic cast (unless one of the arguments is 0) of pointers into uintptr_t during comparisons, making such operation defined even if the pointers do not share the same base. This was the behavior of Cil.mkBinOp prior to the introduction of this function.

val mkTermMem : addr:Cil_types.term -> off:Cil_types.term_offset -> Cil_types.term_lval

Equivalent to mkMem for terms.

val mkString : loc:Cil_types.location -> string -> Cil_types.exp

Make an expression that is a string constant (of pointer type)

val need_cast : ?force:bool -> Cil_types.typ -> Cil_types.typ -> bool

true if both types are not equivalent. if force is true, returns true whenever both types are not equal (modulo typedefs). If force is false (the default), other equivalences are considered, in particular between an enum and its representative integer type.

val mkCastT : ?force:bool ->
e:Cil_types.exp -> oldt:Cil_types.typ -> newt:Cil_types.typ -> Cil_types.exp

Construct a cast when having the old type of the expression. If the new type is the same as the old type, then no cast is added, unless force is true (default is false)

val mkCast : ?force:bool -> e:Cil_types.exp -> newt:Cil_types.typ -> Cil_types.exp

Like Cil.mkCastT but uses typeOf to get oldt

val stripTermCasts : Cil_types.term -> Cil_types.term

Equivalent to stripCasts for terms.

val stripCasts : Cil_types.exp -> Cil_types.exp

Removes casts from this expression, but ignores casts within other expression constructs. So we delete the (A) and (B) casts from "(A)(B)(x + (C)y)", but leave the (C) cast.

val stripInfo : Cil_types.exp -> Cil_types.exp

Removes info wrappers and return underlying expression

val stripCastsAndInfo : Cil_types.exp -> Cil_types.exp

Removes casts and info wrappers and return underlying expression

val stripCastsButLastInfo : Cil_types.exp -> Cil_types.exp

Removes casts and info wrappers,except last info wrapper, and return underlying expression

val exp_info_of_term : Cil_types.term -> Cil_types.exp_info

Extracts term information in an expression information

val term_of_exp_info : Cil_types.location ->
Cil_types.term_node -> Cil_types.exp_info -> Cil_types.term

Constructs a term from a term node and an expression information

val map_under_info : (Cil_types.exp -> Cil_types.exp) -> Cil_types.exp -> Cil_types.exp

Map some function on underlying expression if Info or else on expression

val app_under_info : (Cil_types.exp -> unit) -> Cil_types.exp -> unit

Apply some function on underlying expression if Info or else on expression

val typeOf : Cil_types.exp -> Cil_types.typ

Compute the type of an expression.

val typeOf_pointed : Cil_types.typ -> Cil_types.typ

Returns the type pointed by the given type. Asserts it is a pointer type.

val typeOf_array_elem : Cil_types.typ -> Cil_types.typ

Returns the type of the array elements of the given type. Asserts it is an array type.

val is_fully_arithmetic : Cil_types.typ -> bool

Returns true whenever the type contains only arithmetic types

val parseInt : string -> Integer.t

Convert a string representing a C integer literal to an expression. Handles the prefixes 0x and 0 and the suffixes L, U, UL, LL, ULL.

val parseIntExp : loc:Cil_types.location -> string -> Cil_types.exp
val parseIntLogic : loc:Cil_types.location -> string -> Cil_types.term

Convert a string representing a C integer literal to an expression. Handles the prefixes 0x and 0 and the suffixes L, U, UL, LL, ULL

val appears_in_expr : Cil_types.varinfo -> Cil_types.exp -> bool

Values for manipulating statements

val mkStmt : ?ghost:bool ->
?valid_sid:bool ->
?sattr:Cil_types.attributes -> Cil_types.stmtkind -> Cil_types.stmt

Construct a statement, given its kind. Initialize the sid field to -1 if valid_sid is false (the default), or to a valid sid if valid_sid is true, and labels, succs and preds to the empty list

val mkStmtCfg : before:bool ->
new_stmtkind:Cil_types.stmtkind -> ref_stmt:Cil_types.stmt -> Cil_types.stmt
val mkBlock : Cil_types.stmt list -> Cil_types.block

Construct a block with no attributes, given a list of statements

val mkBlockNonScoping : Cil_types.stmt list -> Cil_types.block

Construct a non-scoping block, i.e. a block that is not used to determine the end of scope of local variables. Hence, the blocals of such a block must always be empty.

val mkStmtCfgBlock : Cil_types.stmt list -> Cil_types.stmt

Construct a block with no attributes, given a list of statements and wrap it into the Cfg.

val mkStmtOneInstr : ?ghost:bool ->
?valid_sid:bool ->
?sattr:Cil_types.attributes -> Cil_types.instr -> Cil_types.stmt

Construct a statement consisting of just one instruction See Cil.mkStmt for the signification of the optional args.

Try to compress statements so as to get maximal basic blocks. use this instead of List.@ because you get fewer basic blocks

val mkEmptyStmt : ?ghost:bool ->
?valid_sid:bool ->
?sattr:Cil_types.attributes ->
?loc:Cil_types.location -> unit -> Cil_types.stmt

Returns an empty statement (of kind Instr). See mkStmt for ghost and valid_sid arguments.

val dummyInstr : Cil_types.instr

A instr to serve as a placeholder

val dummyStmt : Cil_types.stmt

A statement consisting of just dummyInstr.

val mkPureExprInstr : fundec:Cil_types.fundec ->
scope:Cil_types.block ->
?loc:Cil_types.location -> Cil_types.exp -> Cil_types.instr

Create an instruction equivalent to a pure expression. The new instruction corresponds to the initialization of a new fresh variable, i.e. int tmp = exp. The scope of this fresh variable is determined by the block given in argument, that is the instruction must be placed directly (modulo non-scoping blocks) inside this block.

val mkPureExpr : ?ghost:bool ->
?valid_sid:bool ->
fundec:Cil_types.fundec ->
?loc:Cil_types.location -> Cil_types.exp -> Cil_types.stmt

Create an instruction as above, enclosed in a block of a single (Instr) statement, which will be the scope of the fresh variable holding the value of the expression.

See Cil.mkStmt for information about ghost and valid_sid, and Cil.mkPureExprInstr for information about loc.

val mkLoop : ?sattr:Cil_types.attributes ->
guard:Cil_types.exp -> body:Cil_types.stmt list -> Cil_types.stmt list

Make a loop. Can contain Break or Continue. The kind of loop (While, For, DoWhile) is given by sattr; it is a While loop if unspecified.

val mkForIncr : iter:Cil_types.varinfo ->
first:Cil_types.exp ->
stopat:Cil_types.exp ->
incr:Cil_types.exp -> body:Cil_types.stmt list -> Cil_types.stmt list

Make a for loop for(i=start; i<past; i += incr) { ... }. The body can contain Break but not Continue. Can be used with i a pointer or an integer. Start and done must have the same type but incr must be an integer

val mkFor : start:Cil_types.stmt list ->
guard:Cil_types.exp ->
next:Cil_types.stmt list -> body:Cil_types.stmt list -> Cil_types.stmt list

Make a for loop for(start; guard; next) { ... }. The body can contain Break but not Continue !!!

val block_from_unspecified_sequence : (Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
Cil_types.lval list * Cil_types.stmt Stdlib.ref list)
list -> Cil_types.block

creates a block with empty attributes from an unspecified sequence.

val treat_constructor_as_func : (Cil_types.lval option ->
Cil_types.exp -> Cil_types.exp list -> Cil_types.location -> 'a) ->
Cil_types.varinfo ->
Cil_types.varinfo ->
Cil_types.exp list -> Cil_types.constructor_kind -> Cil_types.location -> 'a

treat_constructor_as_func action v f args kind loc calls action with the parameters corresponding to the call to f, of kind kind, initializing v with arguments args.

val find_def_stmt : Cil_types.block -> Cil_types.varinfo -> Cil_types.stmt

find_def_stmt b v returns the Local_init instruction within b that initializes v. v must have its vdefined field set to true, and be among b.blocals.

val has_extern_local_init : Cil_types.block -> bool

returns true iff the given non-scoping block contains local init statements (thus of locals belonging to an outer block), either directly or within a non-scoping block or undefined sequence.labels

val is_ghost_else : Cil_types.block -> bool

returns true iff the given block is a ghost else block.

Values for manipulating attributes

type attributeClass = 
| AttrName of bool (*

Attribute of a name. If argument is true and we are on MSVC then the attribute is printed using __declspec as part of the storage specifier

*)
| AttrFunType of bool (*

Attribute of a function type. If argument is true and we are on MSVC then the attribute is printed just before the function name

*)
| AttrType (*

Attribute of a type

*)

Various classes of attributes

val registerAttribute : string -> attributeClass -> unit

Add a new attribute with a specified class

val removeAttribute : string -> unit

Remove an attribute previously registered.

val attributeClass : string -> attributeClass

Return the class of an attributes.

val partitionAttributes : default:attributeClass ->
Cil_types.attributes ->
Cil_types.attribute list * Cil_types.attribute list *
Cil_types.attribute list

Partition the attributes into classes:name attributes, function type, and type attributes

val addAttribute : Cil_types.attribute -> Cil_types.attributes -> Cil_types.attributes

Add an attribute. Maintains the attributes in sorted order of the second argument

val addAttributes : Cil_types.attribute list -> Cil_types.attributes -> Cil_types.attributes

Add a list of attributes. Maintains the attributes in sorted order. The second argument must be sorted, but not necessarily the first

val dropAttribute : string -> Cil_types.attributes -> Cil_types.attributes

Remove all attributes with the given name. Maintains the attributes in sorted order.

val dropAttributes : string list -> Cil_types.attributes -> Cil_types.attributes

Remove all attributes with names appearing in the string list. Maintains the attributes in sorted order

val frama_c_ghost_else : string

A block marked with this attribute is known to be a ghost else.

val frama_c_ghost_formal : string

A varinfo marked with this attribute is known to be a ghost formal.

val frama_c_init_obj : string

a formal marked with this attribute is known to be a pointer to an object being initialized by the current function, which can thus assign any sub-object regardless of const status.

val frama_c_mutable : string

a field struct marked with this attribute is known to be mutable, i.e. it can be modified even on a const object.

val frama_c_inlined : string

A block marked with this attribute is known to be inlined, i.e. it replaces a call to an inline function.

val is_mutable_or_initialized : Cil_types.lval -> bool

true if the given lval is allowed to be assigned to thanks to a frama_c_init_obj or a frama_c_mutable attribute.

val isGhostFormalVarinfo : Cil_types.varinfo -> bool

true if the given varinfo is a ghost formal variable.

val isGhostFormalVarDecl : string * Cil_types.typ * Cil_types.attributes -> bool

true if the given formal declaration corresponds to a ghost formal variable.

val typeDeepDropAttributes : string list -> Cil_types.typ -> Cil_types.typ
Deprecated.Chlorine-20180501 use Cil.typeRemoveAttributesDeep instead, which does not traverse pointers and function types, or Cil.typeDeepDropAllAttributes, which will give a pristine version of the type, without any attributes.

Remove attributes whose name appears in the first argument that are present anywhere in the fully expanded version of the type.

val typeDeepDropAllAttributes : Cil_types.typ -> Cil_types.typ

Remove any attribute appearing somewhere in the fully expanded version of the type.

val filterAttributes : string -> Cil_types.attributes -> Cil_types.attributes

Retains attributes with the given name

val hasAttribute : string -> Cil_types.attributes -> bool

True if the named attribute appears in the attribute list. The list of attributes must be sorted.

val mkAttrAnnot : string -> string

returns the complete name for an attribute annotation.

val attributeName : Cil_types.attribute -> string

Returns the name of an attribute.

val findAttribute : string -> Cil_types.attribute list -> Cil_types.attrparam list

Returns the list of parameters associated to an attribute. The list is empty if there is no such attribute or it has no parameters at all.

val typeAttrs : Cil_types.typ -> Cil_types.attribute list

Returns all the attributes contained in a type. This requires a traversal of the type structure, in case of composite, enumeration and named types

val typeAttr : Cil_types.typ -> Cil_types.attribute list

Returns the attributes of a type.

val setTypeAttrs : Cil_types.typ -> Cil_types.attributes -> Cil_types.typ

Sets the attributes of the type to the given list. Previous attributes are discarded.

val typeAddAttributes : Cil_types.attribute list -> Cil_types.typ -> Cil_types.typ

Add some attributes to a type

val typeRemoveAttributes : string list -> Cil_types.typ -> Cil_types.typ

Remove all attributes with the given names from a type. Note that this does not remove attributes from typedef and tag definitions, just from their uses (unfolding the type definition when needed). It only removes attributes of topmost type, i.e. does not recurse under pointers, arrays, ...

val typeRemoveAllAttributes : Cil_types.typ -> Cil_types.typ

same as above, but remove any existing attribute from the type.

val typeRemoveAttributesDeep : string list -> Cil_types.typ -> Cil_types.typ

Same as typeRemoveAttributes, but recursively removes the given attributes from inner types as well. Mainly useful to check whether two types are equal modulo some attributes. See also typeDeepDropAllAttributes, which will strip every single attribute from a type.

val typeHasAttribute : string -> Cil_types.typ -> bool

Does the type have the given attribute. Does not recurse through pointer types, nor inside function prototypes.

val typeHasQualifier : string -> Cil_types.typ -> bool

Does the type have the given qualifier. Handles the case of arrays, for which the qualifiers are actually carried by the type of the elements. It is always correct to call this function instead of Cil.typeHasAttribute. For l-values, both functions return the same results, as l-values cannot have array type.

val typeHasAttributeDeep : string -> Cil_types.typ -> bool
val typeHasAttributeMemoryBlock : string -> Cil_types.typ -> bool

typeHasAttributeMemoryBlock attr t is true iff at least one component of an object of type t has attribute attr. In other words, it searches for attr under aggregates, but not under pointers.

val type_remove_qualifier_attributes : Cil_types.typ -> Cil_types.typ

Remove all attributes relative to const, volatile and restrict attributes

val type_remove_qualifier_attributes_deep : Cil_types.typ -> Cil_types.typ

remove also qualifiers under Ptr and Arrays

val type_remove_attributes_for_c_cast : Cil_types.typ -> Cil_types.typ

Remove all attributes relative to const, volatile and restrict attributes when building a C cast

val type_remove_attributes_for_logic_type : Cil_types.typ -> Cil_types.typ

Remove all attributes relative to const, volatile and restrict attributes when building a logic cast

val filter_qualifier_attributes : Cil_types.attributes -> Cil_types.attributes

retains attributes corresponding to type qualifiers (6.7.3)

val splitArrayAttributes : Cil_types.attributes -> Cil_types.attributes * Cil_types.attributes

given some attributes on an array type, split them into those that belong to the type of the elements of the array (currently, qualifiers such as const and volatile), and those that must remain on the array, in that order

val bitfield_attribute_name : string

Name of the attribute that is automatically inserted (with an AINT size argument when querying the type of a field that is a bitfield

val expToAttrParam : Cil_types.exp -> Cil_types.attrparam

Convert an expression into an attrparam, if possible. Otherwise raise NotAnAttrParam with the offending subexpression

val global_annotation_attributes : Cil_types.global_annotation -> Cil_types.attributes

Return the attributes of the global annotation, if any.

val global_attributes : Cil_types.global -> Cil_types.attributes

Return the attributes of the global, if any.

exception NotAnAttrParam of Cil_types.exp

Const Attribute

val isConstType : Cil_types.typ -> bool

Check for "const" qualifier from the type of an l-value (do not follow pointer)

Volatile Attribute

val isVolatileType : Cil_types.typ -> bool

Check for "volatile" qualifier from the type of an l-value (do not follow pointer)

val isVolatileLogicType : Cil_types.logic_type -> bool

Check for "volatile" qualifier from a logic type

val isVolatileLval : Cil_types.lval -> bool

Check if the l-value has a volatile part

val isVolatileTermLval : Cil_types.term_lval -> bool

Check if the l-value has a volatile part

Ghost Attribute

val isGhostType : Cil_types.typ -> bool

Check for "ghost" qualifier from the type of an l-value (do not follow pointer)

val isWFGhostType : Cil_types.typ -> bool

Check if the received type is well-formed according to \ghost semantics, that is once the type is not ghost anymore, \ghost cannot appear again.

The visitor

type 'a visitAction = 
| SkipChildren (*

Do not visit the children. Return the node as it is.

*)
| DoChildren (*

Continue with the children of this node. Rebuild the node on return if any of the children changes (use == test).

*)
| DoChildrenPost of ('a -> 'a) (*

visit the children, and apply the given function to the result.

*)
| JustCopy (*

visit the children, but only to make the necessary copies (only useful for copy visitor).

*)
| JustCopyPost of ('a -> 'a) (*

same as JustCopy + applies the given function to the result.

*)
| ChangeTo of 'a (*

Replace the expression with the given one.

*)
| ChangeToPost of 'a * ('a -> 'a) (*

applies the expression to the function and gives back the result. Useful to insert some actions in an inheritance chain.

*)
| ChangeDoChildrenPost of 'a * ('a -> 'a) (*

First consider that the entire exp is replaced by the first parameter. Then continue with the children. On return rebuild the node if any of the children has changed and then apply the function on the node.

*)

Different visiting actions. 'a will be instantiated with exp, instr, etc.

val mk_behavior : ?name:string ->
?assumes:Cil_types.identified_predicate list ->
?requires:Cil_types.identified_predicate list ->
?post_cond:(Cil_types.termination_kind * Cil_types.identified_predicate) list ->
?assigns:Cil_types.assigns ->
?allocation:Cil_types.allocation ->
?extended:Cil_types.acsl_extension list -> unit -> Cil_types.behavior
val default_behavior_name : string
val is_default_behavior : Cil_types.behavior -> bool
val find_default_behavior : Cil_types.funspec -> Cil_types.funbehavior option
val find_default_requires : Cil_types.behavior list -> Cil_types.identified_predicate list

Visitor mechanism

Visitor class

class type cilVisitor = object .. end

A visitor interface for traversing CIL trees.

val register_behavior_extension : string ->
(cilVisitor ->
Cil_types.acsl_extension_kind ->
Cil_types.acsl_extension_kind visitAction) ->
unit
Deprecated.21.0-Scandium

Indicates how an extended behavior clause is supposed to be visited. The default behavior is DoChildren, which ends up visiting each identified predicate in the list and leave the id as is.

class genericCilVisitor : Visitor_behavior.t -> cilVisitor

generic visitor, parameterized by its copying behavior.

class nopCilVisitor : cilVisitor

Default in place visitor doing nothing and operating on current project.

Generic visit functions

val doVisit : 'visitor ->
'visitor ->
('a -> 'a) ->
('a -> 'a visitAction) -> ('visitor -> 'a -> 'a) -> 'a -> 'a

doVisit vis deepCopyVisitor copy action children node visits a node (or its copy according to the result of copy) and if needed its children. Do not use it if you don't understand Cil visitor mechanism

val doVisitList : 'visitor ->
'visitor ->
('a -> 'a) ->
('a -> 'a list visitAction) -> ('visitor -> 'a -> 'a) -> 'a -> 'a list

same as above, but can return a list of nodes

Visitor's entry points

val visitCilFileCopy : cilVisitor -> Cil_types.file -> Cil_types.file

Visit a file. This will re-cons all globals TWICE (so that it is tail-recursive). Use Cil.visitCilFileSameGlobals if your visitor will not change the list of globals.

val visitCilFile : cilVisitor -> Cil_types.file -> unit

Same thing, but the result is ignored. The given visitor must thus be an inplace visitor. Nothing is done if the visitor is a copy visitor.

val visitCilFileSameGlobals : cilVisitor -> Cil_types.file -> unit

A visitor for the whole file that does not *physically* change the globals (but maybe changes things inside the globals through side-effects). Use this function instead of Cil.visitCilFile whenever appropriate because it is more efficient for long files.

val visitCilGlobal : cilVisitor -> Cil_types.global -> Cil_types.global list

Visit a global

val visitCilFunction : cilVisitor -> Cil_types.fundec -> Cil_types.fundec

Visit a function definition

val visitCilExpr : cilVisitor -> Cil_types.exp -> Cil_types.exp
val visitCilEnumInfo : cilVisitor -> Cil_types.enuminfo -> Cil_types.enuminfo
val visitCilLval : cilVisitor -> Cil_types.lval -> Cil_types.lval

Visit an lvalue

val visitCilOffset : cilVisitor -> Cil_types.offset -> Cil_types.offset

Visit an lvalue or recursive offset

val visitCilInitOffset : cilVisitor -> Cil_types.offset -> Cil_types.offset

Visit an initializer offset

val visitCilLocal_init : cilVisitor ->
Cil_types.varinfo -> Cil_types.local_init -> Cil_types.local_init

Visit a local initializer (with the local being initialized).

val visitCilInstr : cilVisitor -> Cil_types.instr -> Cil_types.instr list

Visit an instruction

val visitCilStmt : cilVisitor -> Cil_types.stmt -> Cil_types.stmt

Visit a statement

val visitCilBlock : cilVisitor -> Cil_types.block -> Cil_types.block

Visit a block

val transient_block : Cil_types.block -> Cil_types.block

Mark the given block as candidate to be flattened into its parent block, after returning from its visit. This is not systematic, as the environment might prevent it (e.g. if the preceding statement is a statement contract or a slicing/pragma annotation, or if there are labels involved). Use that whenever you're creating a block in order to hold multiple statements as a result of visiting a single statement. If the block contains local variables, it will not be marked as transient, since removing it will change the scope of those variables.

val is_transient_block : Cil_types.block -> bool

tells whether the block has been marked as transient

val flatten_transient_sub_blocks : Cil_types.block -> Cil_types.block

flatten_transient_sub_blocks b flattens all direct sub-blocks of b that have been marked as cleanable, whenever possible

val visitCilType : cilVisitor -> Cil_types.typ -> Cil_types.typ

Visit a type

val visitCilVarDecl : cilVisitor -> Cil_types.varinfo -> Cil_types.varinfo

Visit a variable declaration

val visitCilInit : cilVisitor ->
Cil_types.varinfo -> Cil_types.offset -> Cil_types.init -> Cil_types.init

Visit an initializer, pass also the global to which this belongs and the offset.

val visitCilAttributes : cilVisitor -> Cil_types.attribute list -> Cil_types.attribute list

Visit a list of attributes

val visitCilAnnotation : cilVisitor -> Cil_types.global_annotation -> Cil_types.global_annotation
val visitCilCodeAnnotation : cilVisitor -> Cil_types.code_annotation -> Cil_types.code_annotation
val visitCilDeps : cilVisitor -> Cil_types.deps -> Cil_types.deps
val visitCilFrom : cilVisitor -> Cil_types.from -> Cil_types.from
val visitCilAssigns : cilVisitor -> Cil_types.assigns -> Cil_types.assigns
val visitCilFrees : cilVisitor ->
Cil_types.identified_term list -> Cil_types.identified_term list
val visitCilAllocates : cilVisitor ->
Cil_types.identified_term list -> Cil_types.identified_term list
val visitCilAllocation : cilVisitor -> Cil_types.allocation -> Cil_types.allocation
val visitCilFunspec : cilVisitor -> Cil_types.funspec -> Cil_types.funspec
val visitCilBehavior : cilVisitor -> Cil_types.funbehavior -> Cil_types.funbehavior
val visitCilBehaviors : cilVisitor -> Cil_types.funbehavior list -> Cil_types.funbehavior list
val visitCilExtended : cilVisitor -> Cil_types.acsl_extension -> Cil_types.acsl_extension

visit an extended clause of a behavior.

val visitCilModelInfo : cilVisitor -> Cil_types.model_info -> Cil_types.model_info
val visitCilLogicType : cilVisitor -> Cil_types.logic_type -> Cil_types.logic_type
val visitCilIdPredicate : cilVisitor ->
Cil_types.identified_predicate -> Cil_types.identified_predicate
val visitCilPredicateNode : cilVisitor -> Cil_types.predicate_node -> Cil_types.predicate_node
val visitCilPredicate : cilVisitor -> Cil_types.predicate -> Cil_types.predicate
val visitCilPredicates : cilVisitor ->
Cil_types.identified_predicate list -> Cil_types.identified_predicate list
val visitCilTerm : cilVisitor -> Cil_types.term -> Cil_types.term
val visitCilIdTerm : cilVisitor -> Cil_types.identified_term -> Cil_types.identified_term

visit identified_term.

val visitCilTermLval : cilVisitor -> Cil_types.term_lval -> Cil_types.term_lval

visit term_lval.

val visitCilTermLhost : cilVisitor -> Cil_types.term_lhost -> Cil_types.term_lhost
val visitCilTermOffset : cilVisitor -> Cil_types.term_offset -> Cil_types.term_offset
val visitCilLogicInfo : cilVisitor -> Cil_types.logic_info -> Cil_types.logic_info
val visitCilLogicVarUse : cilVisitor -> Cil_types.logic_var -> Cil_types.logic_var
val visitCilLogicVarDecl : cilVisitor -> Cil_types.logic_var -> Cil_types.logic_var

Visiting children of a node

val childrenBehavior : cilVisitor -> Cil_types.funbehavior -> Cil_types.funbehavior

Utility functions

val is_skip : Cil_types.stmtkind -> bool
val constFoldVisitor : bool -> cilVisitor

A visitor that does constant folding. Pass as argument whether you want machine specific simplifications to be done, or not.

Debugging support

module CurrentLoc: State_builder.Ref  with type data = location

A reference to the current location.

val pp_thisloc : Stdlib.Format.formatter -> unit

Pretty-print (Cil.CurrentLoc.get ())

val empty_funspec : unit -> Cil_types.funspec
val is_empty_funspec : Cil_types.funspec -> bool
val is_empty_behavior : Cil_types.funbehavior -> bool

ALPHA conversion

has been moved to the Alpha module.

val uniqueVarNames : Cil_types.file -> unit

Assign unique names to local variables. This might be necessary after you transformed the code and added or renamed some new variables. Names are not used by CIL internally, but once you print the file out the compiler downstream might be confused. You might have added a new global that happens to have the same name as a local in some function. Rename the local to ensure that there would never be confusion. Or, viceversa, you might have added a local with a name that conflicts with a global

Optimization Passes

val peepHole2 : aggressive:bool ->
(Cil_types.stmt * Cil_types.stmt -> Cil_types.stmt list option) ->
Cil_types.stmt list -> Cil_types.stmt list

A peephole optimizer that processes two adjacent statements and possibly replaces them both. If some replacement happens and aggressive is true, then the new statements are themselves subject to optimization. Each statement in the list is optimized independently.

val peepHole1 : (Cil_types.instr -> Cil_types.instr list option) ->
Cil_types.stmt list -> unit

Similar to peepHole2 except that the optimization window consists of one statement, not two

Machine dependency

exception SizeOfError of string * Cil_types.typ

Raised when one of the SizeOf/AlignOf functions cannot compute the size of a type. This can happen because the type contains array-length expressions that we don't know how to compute or because it is a type whose size is not defined (e.g. TFun or an undefined compinfo). The string is an explanation of the error

val empty_size_cache : unit -> Cil_types.bitsSizeofTypCache

Create a fresh size cache with Not_Computed

val unsignedVersionOf : Cil_types.ikind -> Cil_types.ikind

Give the unsigned kind corresponding to any integer kind

val intKindForSize : int -> bool -> Cil_types.ikind

The signed integer kind for a given size (unsigned if second argument is true). Raises Not_found if no such kind exists

val floatKindForSize : int -> Cil_types.fkind

The float kind for a given size. Raises Not_found if no such kind exists

val bitsSizeOf : Cil_types.typ -> int

The size of a type, in bits. Trailing padding is added for structs and arrays. Raises Cil.SizeOfError when it cannot compute the size. This function is architecture dependent, so you should only call this after you call Cil.initCIL. Remember that on GCC sizeof(void) is 1!

val bytesSizeOf : Cil_types.typ -> int

The size of a type, in bytes. Raises Cil.SizeOfError when it cannot compute the size.

val bytesSizeOfInt : Cil_types.ikind -> int

Returns the number of bytes (resp. bits) to represent the given integer kind depending on the current machdep.

val bitsSizeOfInt : Cil_types.ikind -> int
val isSigned : Cil_types.ikind -> bool

Returns the signedness of the given integer kind depending on the current machdep.

val bitsSizeOfBitfield : Cil_types.typ -> int

Returns the size of the given type, in bits. If this is the type of an lvalue which is a bitfield, the size of the bitfield is returned.

val rank : Cil_types.ikind -> int

Returns a unique number representing the integer conversion rank.

val intTypeIncluded : Cil_types.ikind -> Cil_types.ikind -> bool

intTypeIncluded i1 i2 returns true iff the range of values representable in i1 is included in the one of i2

val frank : Cil_types.fkind -> int

Returns a unique number representing the floating-point conversion rank.

val truncateInteger64 : Cil_types.ikind -> Integer.t -> Integer.t * bool

Represents an integer as for a given kind. Returns a flag saying whether the value was changed during truncation (because it was too large to fit in k).

val max_signed_number : int -> Integer.t

Returns the maximal value representable in a signed integer type of the given size (in bits)

val min_signed_number : int -> Integer.t

Returns the smallest value representable in a signed integer type of the given size (in bits)

val max_unsigned_number : int -> Integer.t

Returns the maximal value representable in a unsigned integer type of the given size (in bits)

val fitsInInt : Cil_types.ikind -> Integer.t -> bool

True if the integer fits within the kind's range

val isFiniteFloat : Cil_types.fkind -> float -> bool

True if the float is finite for the kind's range

val isExactFloat : Cil_types.fkind -> Cil_types.logic_real -> bool

True if the real constant is an exact float for the given type

exception Not_representable

raised by Cil.intKindForValue.

val intKindForValue : Integer.t -> bool -> Cil_types.ikind
val sizeOf : loc:Cil_types.location -> Cil_types.typ -> Cil_types.exp

The size of a type, in bytes. Returns a constant expression or a "sizeof" expression if it cannot compute the size. This function is architecture dependent, so you should only call this after you call Cil.initCIL.

val bytesAlignOf : Cil_types.typ -> int

The minimum alignment (in bytes) for a type. This function is architecture dependent, so you should only call this after you call Cil.initCIL.

val intOfAttrparam : Cil_types.attrparam -> int option

intOfAttrparam a tries to const-fold a into a numeric value. Returns Some n if it succeeds, None otherwise.

val bitsOffset : Cil_types.typ -> Cil_types.offset -> int * int

Give a type of a base and an offset, returns the number of bits from the base address and the width (also expressed in bits) for the subobject denoted by the offset. Raises Cil.SizeOfError when it cannot compute the size. This function is architecture dependent, so you should only call this after you call Cil.initCIL.

val mapNoCopy : ('a -> 'a) -> 'a list -> 'a list

Like map but try not to make a copy of the list

val optMapNoCopy : ('a -> 'a) -> 'a option -> 'a option

same as mapNoCopy for options

val mapNoCopyList : ('a -> 'a list) -> 'a list -> 'a list

Like map but each call can return a list. Try not to make a copy of the list

val startsWith : string -> string -> bool

sm: return true if the first is a prefix of the second string

An Interpreter for constructing CIL constructs

type formatArg = 
| Fe of Cil_types.exp
| Feo of Cil_types.exp option (*

For array lengths

*)
| Fu of Cil_types.unop
| Fb of Cil_types.binop
| Fk of Cil_types.ikind
| FE of Cil_types.exp list (*

For arguments in a function call

*)
| Ff of (string * Cil_types.typ * Cil_types.attributes) (*

For a formal argument

*)
| FF of (string * Cil_types.typ * Cil_types.attributes) list (*

For formal argument lists

*)
| Fva of bool (*

For the ellipsis in a function type

*)
| Fv of Cil_types.varinfo
| Fl of Cil_types.lval
| Flo of Cil_types.lval option
| Fo of Cil_types.offset
| Fc of Cil_types.compinfo
| Fi of Cil_types.instr
| FI of Cil_types.instr list
| Ft of Cil_types.typ
| Fd of int
| Fg of string
| Fs of Cil_types.stmt
| FS of Cil_types.stmt list
| FA of Cil_types.attributes
| Fp of Cil_types.attrparam
| FP of Cil_types.attrparam list
| FX of string

The type of argument for the interpreter

val d_formatarg : Stdlib.Format.formatter -> formatArg -> unit

Misc

val stmt_of_instr_list : ?loc:Cil_types.location -> Cil_types.instr list -> Cil_types.stmtkind

if the list has 2 elements or more, it will return a block with bscoping=false

val cvar_to_lvar : Cil_types.varinfo -> Cil_types.logic_var

Convert a C variable into the corresponding logic variable. The returned logic variable is unique for a given C variable.

val make_temp_logic_var : Cil_types.logic_type -> Cil_types.logic_var

Make a temporary variable to use in annotations

val lzero : ?loc:Cil_types.location -> unit -> Cil_types.term

The constant logic term zero.

val lone : ?loc:Cil_types.location -> unit -> Cil_types.term

The constant logic term 1.

val lmone : ?loc:Cil_types.location -> unit -> Cil_types.term

The constant logic term -1.

val lconstant : ?loc:Cil_types.location -> Integer.t -> Cil_types.term

The given constant logic term

val close_predicate : Cil_types.predicate -> Cil_types.predicate

Bind all free variables with an universal quantifier

val extract_varinfos_from_exp : Cil_types.exp -> Cil_datatype.Varinfo.Set.t

extract varinfo elements from an exp

val extract_varinfos_from_lval : Cil_types.lval -> Cil_datatype.Varinfo.Set.t

extract varinfo elements from an lval

val extract_free_logicvars_from_term : Cil_types.term -> Cil_datatype.Logic_var.Set.t

extract logic_var elements from a term

val extract_free_logicvars_from_predicate : Cil_types.predicate -> Cil_datatype.Logic_var.Set.t

extract logic_var elements from a predicate

val extract_labels_from_annot : Cil_types.code_annotation -> Cil_datatype.Logic_label.Set.t

extract logic_label elements from a code_annotation

val extract_labels_from_term : Cil_types.term -> Cil_datatype.Logic_label.Set.t

extract logic_label elements from a term

val extract_labels_from_pred : Cil_types.predicate -> Cil_datatype.Logic_label.Set.t

extract logic_label elements from a pred

val extract_stmts_from_labels : Cil_datatype.Logic_label.Set.t -> Cil_datatype.Stmt.Set.t

extract stmt elements from logic_label elements

val create_alpha_renaming : Cil_types.varinfo list -> Cil_types.varinfo list -> cilVisitor

creates a visitor that will replace in place uses of var in the first list by their counterpart in the second list.

val separate_switch_succs : Cil_types.stmt -> Cil_types.stmt list * Cil_types.stmt

Provided s is a switch, separate_switch_succs s returns the subset of s.succs that correspond to the Case labels of s, and a "default statement" that either corresponds to the Default label, or to the syntactic successor of s if there is no default label. Note that this "default statement" can thus appear in the returned list.

val separate_if_succs : Cil_types.stmt -> Cil_types.stmt * Cil_types.stmt

Provided s is a if, separate_if_succs s splits the successors of s according to the truth value of the condition. The first element of the pair is the successor statement if the condition is true, and the second if the condition is false.