Frama-C API - Cil
CIL main API.
CIL original API documentation is available as an html version at http://manju.cs.berkeley.edu/cil.
Customization
type theMachine = Machine.machine
val theMachine : theMachine
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
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 isVoidType : Cil_types.typ -> bool
is the given type "void"?
val isVoidPtrType : Cil_types.typ -> bool
is the given type "void *"?
val int16_t : unit -> Cil_types.typ
Any signed integer type of size 16 bits. It is equivalent to the ISO C int16_t type but without using the corresponding header. Must only be called if such type exists in the current architecture.
val int32_t : unit -> Cil_types.typ
Any signed integer type of size 32 bits. It is equivalent to the ISO C int32_t type but without using the corresponding header. Must only be called if such type exists in the current architecture.
val int64_t : unit -> Cil_types.typ
Any signed integer type of size 64 bits. It is equivalent to the ISO C int64_t type but without using the corresponding header. Must only be called if such type exists in the current architecture.
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. Must only be called if 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. Must only be called if 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. Must only be called if such type exists in the current architecture.
val isSignedInteger : Cil_types.typ -> bool
val isUnsignedInteger : Cil_types.typ -> bool
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.
val lvalue_conversion : Cil_types.typ -> (Cil_types.typ, string) Stdlib.result
Performs lvalue-conversion on the type and returns the converted type, or Error if the type is incomplete and not an array type.
val is_variably_modified_type : Cil_types.typ -> bool
true
iff the given type is variably modified, i.e., an array with variable size (VLA), or a composite type containing such an array.
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.
true
iff the given type has flexible array member, in GCC/MSVC mode, this function mode recursively searches in the type of the last field.
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 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 isTransparentUnion : Cil_types.typ -> Cil_types.fieldinfo option
Check if a type is a transparent union, and return the first field
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
Obtain the argument lists (non-ghost, ghosts) (, if None)
val isArrayType : Cil_types.typ -> bool
True if the argument is an array type
val isUnsizedArrayType : Cil_types.typ -> bool
True if the argument is an array type without size
val isSizedArrayType : Cil_types.typ -> bool
True if the argument is a sized array type
val isStructType : Cil_types.typ -> bool
True if the argument is a struct
val isUnionType : Cil_types.typ -> bool
True if the argument is a union type
val isStructOrUnionType : Cil_types.typ -> bool
True if the argument is a struct or union type
possible causes for raising Cil.LenOfArray
val pp_incorrect_array_length : Stdlib.Format.formatter -> incorrect_array_length -> unit
exception LenOfArray of incorrect_array_length
Raised when Cil.lenOfArray
fails either because the length is None
, because it is a non-constant expression, or because it overflows an int.
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
val getCompType : Cil_types.typ -> Cil_types.compinfo
Return the compinfo of the typ, or raise Not_found
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
val splitFunctionTypeVI : Cil_types.varinfo -> Cil_types.typ * (string * Cil_types.typ * Cil_types.attributes) list option * bool * Cil_types.attributes
Same as Cil.splitFunctionType
but takes a varinfo. Prints a nicer error message if the varinfo is not for a function
type combineWhat =
| CombineFundef of bool
(*The new definition is for a function definition. The old is for a prototype. arg is
*)true
for an old-style declaration.| CombineFunarg of bool
(*Comparing a function argument type with an old prototype argument. arg is
*)true
for an old-style declaration, which triggers some ad hoc treatment in GCC mode.| CombineFunret
(*Comparing the return of a function with that from an old prototype
*)| CombineOther
Used in combineTypes
and combineTypesGen
to indicate what we want to combine.
val combineAttributes : combineWhat -> Cil_types.attribute list -> Cil_types.attributes -> Cil_types.attributes
combineAttributes what olda a
combines the attributes in olda
and a
according to what
:
- if
what == CombineFunarg
, then override old attributes; this is used to ensure that attributes from formal argument types in a function definition are not mixed with attributes from arguments in other (compatible, but with different qualifiers) declarations; - else, perform the union of old and new attributes.
type combineFunction = {
typ_combine : combineFunction -> strictInteger:bool -> strictReturnTypes:bool -> combineWhat -> Cil_types.typ -> Cil_types.typ -> Cil_types.typ;
enum_combine : combineFunction -> Cil_types.enuminfo -> Cil_types.enuminfo -> Cil_types.enuminfo;
comp_combine : combineFunction -> Cil_types.compinfo -> Cil_types.compinfo -> Cil_types.compinfo;
name_combine : combineFunction -> combineWhat -> Cil_types.typeinfo -> Cil_types.typeinfo -> Cil_types.typeinfo;
}
combineFunction
contains information on how enum, struct/union and typedef are to be handled when combining with combineTypes
and combineTypesGen
. In pratice, the first argument of each field is a recursive definition.
val combineTypesGen : ?emitwith:(Log.event -> unit) -> combineFunction -> strictInteger:bool -> strictReturnTypes:bool -> combineWhat -> Cil_types.typ -> Cil_types.typ -> Cil_types.typ
combineTypesGen ~strictInteger ~strictReturnTypes combF combW oldt newt
Combine oldt
and newt
accordingly to combF
, combW
indicates what we are combinining.
Warning : this is not commutative. Indeed, excluding enum, struct/union and typedef which depend on combF
, the resulting type is as close as possible to newt
.
If strictInteger
is true
, same size/sign integers with different types will not be combined. Emits a warning if it is false
and the compatibility is machine-dependent.
If strictReturnTypes
is false
, anything will be considered compatible with void if combW
is CombineFunret
(i.e. comparing function return types).
~emitwith
is used to emit warnings.
val combineTypes : ?strictInteger:bool -> ?strictReturnTypes:bool -> combineWhat -> Cil_types.typ -> Cil_types.typ -> Cil_types.typ
Specialized version of combineTypesGen], we suppose here that if two global symbols are equal, then they are the same object. @since 28.0-Nickel @before 29.0-Copper [strictInteger (true)] was not present and left with its default value in combineTypesGen.
type qualifier_check_context =
| Identical
(*Identical qualifiers.
*)| IdenticalToplevel
(*Ignore at toplevel, use Identical when going under a pointer.
*)| Covariant
(*First type can have const-qualifications the second doesn't have.
*)| CovariantToplevel
(*Accepts everything for current type, use Covariant when going under a pointer.
*)| Contravariant
(*Second type can have const-qualifications the first doesn't have.
*)| ContravariantToplevel
(*Accepts everything for current type, use Contravariant when going under a pointer.
*)
How type qualifiers must be checked when checking for types compatibility with areCompatibleTypes
and compatibleTypes
.
val areCompatibleTypes : ?strictReturnTypes:bool -> ?context:qualifier_check_context -> Cil_types.typ -> Cil_types.typ -> bool
areCompatibleTypes
returns true
if two types are compatible. context
indicates how check the compatibility of qualifiers. Other arguments are the same than combineTypes
.
val compatibleTypes : ?strictReturnTypes:bool -> ?context:qualifier_check_context -> Cil_types.typ -> Cil_types.typ -> Cil_types.typ
Same as areCompatibleTypes old newt
but combine oldt
and newt
. context
does not impact the qualifiers of the result.
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:
- specifying ghost to false if the function is ghost leads to an error
- when
where
is specified, its status must be the same as the formal to insert (else, it cannot be found in the list of ghost or non ghost formals)
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 : ?is_varinfo_cst:(Cil_types.varinfo -> bool) -> Cil_types.exp -> bool
True if the expression is a compile-time constant. is_varinfo_cst
indicates whether a variable should be considered as having a constant content. Defaults to false
.
val isIntegerConstant : ?is_varinfo_cst:(Cil_types.varinfo -> bool) -> Cil_types.exp -> bool
True if the expression is a compile-time integer constant
val isConstantOffset : ?is_varinfo_cst:(Cil_types.varinfo -> bool) -> 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 is_nullptr : Cil_types.exp -> bool
True if the given expression is a null pointer, i.e. 0
, (void * )0
, which are the two null pointer constants in the standard, or the cast of a null pointer (constant or not) into a pointer type.
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 : Cil_types.term -> Cil_types.term
Do constant folding on an term.
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 sameSizeInt : ?machdep:bool -> Cil_types.ikind -> Cil_types.ikind -> bool
true
if two kinds have the same size independently of the machine.
val same_int64 : ?machdep:bool -> Cil_types.exp -> Cil_types.exp -> bool
true
if the result of two expressions are two equal integers.
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
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 typeForInsertedCast : (Cil_types.exp -> Cil_types.typ -> Cil_types.typ -> Cil_types.typ) Stdlib.ref
typeForInsertedCast expr original_type destination_type
returns the type into which expr
, which has type original_type
and whose type must be converted into destination_type
, must be casted.
By default, returns destination_type
.
This applies only to implicit casts. Casts already present in the source code are exempt from this hook.
val checkCast : ?context:qualifier_check_context -> ?nullptr_cast:bool -> ?fromsource:bool -> Cil_types.typ -> Cil_types.typ -> unit
checkCast context fromsource nullptr_cast oldt newt
emits a warning or an error if the cast from oldt
to newt
is invalid (does nothing otherwise). nullptr_cast
is true
iff the expression being casted is a null pointer. Default is false. fromsource
is false
(default) if the cast is not present in the source code. Check areCompatibleTypes
documentation for context
.
Suspicious cases that only emit a warning:
- Implicit cast from a pointer to an integer.
- Cast from a pointer to a function type to another pointer to a function type when the function types are not compatible.
- Cast from an array to a pointer/array when types are not compatible.
- Cast, in both directions, between pointer to an object type and pointer to a function type.
val mkCastTGen : ?check:bool -> ?context:qualifier_check_context -> ?fromsource:bool -> ?force:bool -> oldt:Cil_types.typ -> newt:Cil_types.typ -> Cil_types.exp -> Cil_types.typ * Cil_types.exp
Generic version of Cil.mkCastT
. Construct a cast when having the old type of the expression. fromsource
is false
(default) if the cast is not present in the source code. If check
is true
(default), we check that the cast is valid, emitting an error or warning if the cast is invalid. If the new type is the same as the old type, then no cast is added, unless force
is true
(default is false
). Cast from oldt
to newt
, returning the new type and the new expression.
val mkCastT : ?check:bool -> ?force:bool -> oldt:Cil_types.typ -> newt:Cil_types.typ -> Cil_types.exp -> 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
). Emit an error or warning if check
is true and the cast is invalid.
val mkCast : ?check:bool -> ?force:bool -> newt:Cil_types.typ -> Cil_types.exp -> 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 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 typeOf_array_elem_size : Cil_types.typ -> Cil_types.typ * Z.t option
Returns the type of the array elements of the given type, and the size of the array, if any. 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 Integer. Handles the prefixes 0x and 0 and the suffixes L, U, UL, LL, ULL.
val parseIntRes : string -> (Integer.t, string) Stdlib.result
Like parseInt
, but returns Error message
in case of failure, instead of aborting Frama-C.
val parseIntExp : loc:Cil_types.location -> string -> Cil_types.exp
Like parseInt
, but converts to an expression.
val parseIntExpRes : loc:Cil_types.location -> string -> (Cil_types.exp, string) Stdlib.result
Like parseIntExp
, but returns Error message
in case of failure, instead of aborting Frama-C.
val parseIntLogic : loc:Cil_types.location -> string -> Cil_types.term
Like parseInt
, but converts to a logic term.
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.
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 -> unit -> Cil_types.stmt list
Make a loop. Can contain Break or Continue. The kind of loop (while, for, dowhile) is given by sattr
(none by default). Use Cil.mkWhile
for a While loop.
val mkForIncr : ?sattr:Cil_types.attributes -> iter:Cil_types.varinfo -> first:Cil_types.exp -> stopat:Cil_types.exp -> incr:Cil_types.exp -> body:Cil_types.stmt list -> unit -> 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 : ?sattr:Cil_types.attributes -> start:Cil_types.stmt list -> guard:Cil_types.exp -> next:Cil_types.stmt list -> body:Cil_types.stmt list -> unit -> Cil_types.stmt list
Make a for loop for(start; guard; next) { ... }. The body can contain Break but not Continue !!!
val mkWhile : ?sattr:Cil_types.attributes -> guard:Cil_types.exp -> body:Cil_types.stmt list -> unit -> Cil_types.stmt list
Make a while loop.
val mkDoWhile : ?sattr:Cil_types.attributes -> body:Cil_types.stmt list -> guard:Cil_types.exp -> unit -> Cil_types.stmt list
Make a do ... while loop.
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.
val instr_falls_through : Cil_types.instr -> bool
returns false
if the given instruction is a call to a function with a "noreturn"
attribute, and true
otherwise.
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 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. The attribute is not added if it is already there.
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
A varinfo marked with this attribute is known to be a ghost formal.
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.
a field struct marked with this attribute is known to be mutable, i.e. it can be modified even on a const object.
A block marked with this attribute is known to be inlined, i.e. it replaces a call to an inline function.
val is_initialized : Cil_types.exp -> bool
true
if the underlying left-value of the given expression is allowed to be assigned to thanks to a frama_c_init_obj
attribute.
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 isGlobalInitConst : Cil_types.varinfo -> bool
true
iff the given variable is a const global variable with non extern storage.
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 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 : ?combine: (Cil_types.attribute list -> Cil_types.attributes -> Cil_types.attributes) -> Cil_types.attribute list -> Cil_types.typ -> Cil_types.typ
Add some attributes to a type. combine
explains how to combine attributes. Default is addAttributes
.
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 typeHasAttribute
. For l-values, both functions return the same results, as l-values cannot have array type.
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
Name of the attribute that is automatically inserted (with an AINT size
argument when querying the type of a field that is a bitfield
Name of the attribute that is inserted when generating a name for a varinfo representing an anonymous function parameter.
val anonymous_attribute : Cil_types.attribute
attribute identifying anonymous function parameters
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.
val is_in_libc : Cil_types.attributes -> bool
Whether the given attributes contain libc indicators.
val global_is_in_libc : Cil_types.global -> bool
Whether the given global contains libc indicators.
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.
val typeAddGhost : Cil_types.typ -> Cil_types.typ
Add the ghost attribute to a type (does nothing if the type is alreay ghost)
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
returns a dummy behavior with the default name Cil.default_behavior_name
. invariant: b_assumes
must always be empty for behavior named Cil.default_behavior_name
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. Create instantiations of this type by specializing the class nopCilVisitor
. Each of the specialized visiting functions can also call the queueInstr
to specify that some instructions should be inserted before the current statement. Use syntax like self#queueInstr
to call a method associated with the current object.
class genericCilVisitor : Visitor_behavior.t -> cilVisitor
generic visitor, parameterized by its copying behavior. Traverses the CIL tree without modifying anything
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 visitCilFileFunctions : cilVisitor -> Cil_types.file -> unit
Same as Cil.visitCilFileSameGlobals
, but only visits function definitions (i.e. behaves as if all globals but GFun
return SkipChildren
).
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 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
val empty_funspec : unit -> Cil_types.funspec
val is_empty_funspec : Cil_types.funspec -> bool
val is_empty_behavior : Cil_types.funbehavior -> bool
Renaming
See also the Alpha
module for other renaming operations.
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 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 Machine.init
. 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 selfTypSize : State.t
Cache for sizeof
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
raised by 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 Machine.init
.
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 Machine.init
.
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 Machine.init
.
val fieldBitsOffset : Cil_types.fieldinfo -> int * int
Give a field, returns the number of bits from the structure or union containing the field and the width (also expressed in bits) for the subobject denoted by the field. Raises Cil.SizeOfError
when it cannot compute the size. This function is architecture dependent, so you should only call this after you call Machine.init
.
Like map but each call can return a list. Try not to make a copy of the list
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 cvar_to_term : loc:Cil_types.location -> Cil_types.varinfo -> Cil_types.term
Convert a C variable into a logic term.
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.