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.
Consult the Plugin Development Guide for additional details.
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
Since Fluorine-20130401
Returns true if the given variable refers to a Frama-C builtin.
val is_unused_builtin : Cil_types.varinfo -> bool
Returns true if the given variable refers to a Frama-C builtin that
is not used in the current program. Plugins may (and in fact should)
hide this builtin from their outputs
val is_special_builtin : string -> bool
Since Boron-20100401-dev
Returns true
if the given name refers to a special built-in function.
A special built-in function can have any number of arguments. It is up to
the plug-ins to know what to do with it.
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.
Since Carbon-20101201
val init_builtins : unit -> unit
initialize the C built-ins. Should be called once per project, after the
machine has been set.
module type Machdeps = sig
.. end
Description of the machine as seen in GCC and MSVC modes.
val initCIL : initLogicBuiltins:(unit -> unit) -> (module Cil.Machdeps) -> 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 {
}
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 set_msvcMode : bool -> unit
type
lineDirectiveStyle =
| |
|
| |
|
| |
LinePreprocessorInput |
| |
LinePreprocessorOutput |
Styles of printing line directives
type
miscState = {
|
mutable lineDirectiveStyle : lineDirectiveStyle option ; |
|
mutable print_CIL_Input : bool ; |
|
mutable printCilAsIs : bool ; |
|
mutable lineLength : int ; |
|
mutable warnTruncate : bool ; |
}
val miscState : miscState
type
featureDescr = {
|
fd_enabled : bool Pervasives.ref ; |
|
fd_name : string ; |
|
fd_description : string ; |
|
: (string * Arg.spec * string) list ; |
|
fd_doit : Cil_types.file -> unit ; |
|
fd_post_check : bool ; |
}
To be able to add/remove features easily, each feature should be package
as an interface with the following interface.
val emptyFunctionFromVI : Cil_types.varinfo -> Cil_types.fundec
Make an empty function from an existing global varinfo.
Since Nitrogen-20111001
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
val stripConstLocalType : Cil_types.typ -> Cil_types.typ
Strip const attribute from the type. This is useful for
any type used as the type of a local variable which may be assigned.
Note that the type attributes are mutated in place.
Since Nitrogen-20111001
val selfFormalsDecl : State.t
state of the table associating formals to each prototype.
val makeFormalsVarDecl : string * Cil_types.typ * Cil_types.attributes -> Cil_types.varinfo
creates a new varinfo for the parameter of a prototype.
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.
Since Oxygen-20120901
val unsafeSetFormalsDecl : Cil_types.varinfo -> Cil_types.varinfo list -> unit
replace to formals of a function declaration with the given
list of varinfo.
val iterFormalsDecl : (Cil_types.varinfo -> Cil_types.varinfo list -> unit) -> unit
iters the given function on declared prototypes.
Since Oxygen-20120901
val getFormalsDecl : Cil_types.varinfo -> Cil_types.varinfo list
Get the formals of a function declaration registered with
Cil.setFormalsDecl
.
Raises Not_found
if the function is not registered (this is in particular
the case for prototypes with an empty list of arguments.
See
Cil.setFormalsDecl
)
val dummyFile : Cil_types.file
A dummy file
val getGlobInit : ?main_name:string -> Cil_types.file -> Cil_types.fundec
Deprecated.using this function is incorrect since it modifies the
current AST (see Plug-in Development Guide, Section "Using Projects").
Get the global initializer and create one if it does not already exist.
When it creates a global initializer it attempts to place a call to it in
the main function named by the optional argument (default "main").
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.
module Sid: sig
.. end
module Eid: sig
.. end
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).
Since Nitrogen-20111001
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 Pervasives.ref ->
variables:Cil_types.global list Pervasives.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.
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' t' acc ->
myInit (addOffsetLval lv off') i' acc)
~ct:ct
~initl:initl
~acc:acc
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.
Since Nitrogen-20111001
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.
Since Nitrogen-20111001
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.
Since Nitrogen-20111001
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
Returns true if and only if the given type is a signed integer type.
val isUnsignedInteger : Cil_types.typ -> bool
Since Oxygen-20120901
Returns true if and only if the given type is an unsigned integer type.
val mkCompInfo : bool ->
string ->
?norig:string ->
(Cil_types.compinfo ->
(string * Cil_types.typ * int option * Cil_types.attributes *
Cil_types.location)
list) ->
Cil_types.attributes -> Cil_types.compinfo
Creates a a (potentially recursive) composite type. The arguments are:
(1) a boolean indicating whether it is a struct or a union, (2) the name
(always non-empty), (3) a function that when given a representation of the
structure type constructs the type of the fields recursive type (the first
argument is only useful when some fields need to refer to the type of the
structure itself), and (4) a list of attributes to be associated with the
composite type. The resulting compinfo has the field "cdefined" only if
the list of fields is non-empty.
val copyCompInfo : Cil_types.compinfo -> string -> Cil_types.compinfo
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
val isCompleteType : 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 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.
Since Nitrogen-20111001 (moved from Cabs2cil)
val integralPromotion : Cil_types.typ -> Cil_types.typ
performs the usual integral promotions mentioned in C reference manual.
Since Nitrogen-20111001 (moved from Cabs2cil)
val isCharType : Cil_types.typ -> bool
True if the argument is a character type (i.e. plain, signed or unsigned)
val isShortType : Cil_types.typ -> bool
True if the argument is a short type (i.e. signed or unsigned)
val isCharPtrType : Cil_types.typ -> bool
True if the argument is a pointer to 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 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 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 isArithmeticOrPointerType : Cil_types.typ -> bool
True if the argument is an arithmetic or pointer type (i.e. integer, 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 isPointerType : Cil_types.typ -> bool
True if the argument is a pointer type
val isTypeTagType : Cil_types.logic_type -> bool
True if the argument is the type for reified C types
val isFunctionType : Cil_types.typ -> bool
True if the argument is a function type.
val isVariadicListType : Cil_types.typ -> bool
True if the argument denotes the type of ... in a variadic function.
Since Nitrogen-20111001 moved from cabs2cil
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 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 |
| |
ExistsFalse |
| |
ExistsMaybe |
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 : ?logic:bool ->
?generated:bool ->
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
logic
argument defaults to
false
and should be used to create a varinfo such that
varinfo.vlogic=true
.
The
generated
argument defaults to
true
(in fact, only front-ends have
the need to set it to false), and tells whether the variable is generated
or comes directly from user input (the
vgenerated
flag).
The first unnmamed argument specifies whether the varinfo is for a global and
the second is for formals.
val makeFormalVar : Cil_types.fundec ->
?where:string -> 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.
A formal var is never generated.
val makeLocalVar : Cil_types.fundec ->
?scope:Cil_types.block ->
?generated:bool ->
?insert:bool -> 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.
generated
is passed to
Cil.makeVarinfo
.
The variable is attached to the toplevel block if
scope
is not specified.
Since Nitrogen-20111001 This function will strip const attributes
of its type in place in order for local variable to be assignable at
least once.
val makePseudoVar : Cil_types.typ -> Cil_types.varinfo
Make a pseudo-variable to use as placeholder in term to expression
conversions. Its logic field is set. They are always generated.
val makeTempVar : Cil_types.fundec ->
?insert:bool ->
?name:string ->
?descr:string -> ?descrpure:bool -> 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.
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 : ?logic:bool ->
?generated:bool -> string -> Cil_types.typ -> Cil_types.varinfo
Make a global variable. Your responsibility to make sure that the name
is unique. logic
defaults to false
. generated
defaults to true
.
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.
Since Neon-20130301
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 lastTermOffset : Cil_types.term_offset -> Cil_types.term_offset
Deprecated.Oxygen-20120901 use Logic_const.addTermOffsetLval
Equivalent to lastOffset
for terms.
val addTermOffsetLval : Cil_types.term_offset -> Cil_types.term_lval -> Cil_types.term_lval
Deprecated.Oxygen-20120901 use Logic_const.addTermOffsetLval
Equivalent to addOffsetLval
for terms.
val addTermOffset : Cil_types.term_offset -> Cil_types.term_offset -> Cil_types.term_offset
Deprecated.Oxygen-20120901 use Logic_const.
Equivalent to addOffset
for terms.
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 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_repr : loc:Cil_types.location ->
Cil_types.ikind -> Integer.t -> string option -> Cil_types.exp
Construct an integer of a given kind, using OCaml's int64 type. If needed
it will truncate the integer to be within the representable range for the
given kind. The integer can have an optional literal representation.
val kinteger64 : loc:Cil_types.location -> Cil_types.ikind -> Integer.t -> Cil_types.exp
Construct an integer of a given kind without literal representation.
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.
Since Oxygen-20120901
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 nanmes 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 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 -> Cil_types.constant
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-extened c, IInt, None)
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 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 at toplevel only.
If the first argument is true then
will also compute compiler-dependent expressions such as sizeof
and alignof
.
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.
Since Nitrogen-20111001
val compareExp : Cil_types.exp -> Cil_types.exp -> bool
Deprecated.Oxygen-20120901 use Cil_datatype.ExpStructEq.compare
true
if the two expressions are syntactically the same.
val compareLval : Cil_types.lval -> Cil_types.lval -> bool
Deprecated.Oxygen-20120901 use Cil_datatype.LvalStructEq.compare
true
if the two lval are syntactically the same.
val compareOffset : Cil_types.offset -> Cil_types.offset -> bool
Deprecated.Oxygen-20120901 use Cil_datatype.OffsetStructEq.compare
true
if the two offsets are syntactically the same.
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.
Since Nitrogen-20111001
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".
Since Oxygen-20120901
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 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.
Change in Fluorine-20130401: added force
argument
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
)
Change in Fluorine-20130401: add force
argument
val mkCast : ?force:bool -> e:Cil_types.exp -> newt:Cil_types.typ -> Cil_types.exp
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
Returns true if the given variable appears in the expression.
val mkStmt : ?ghost:bool -> ?valid_sid:bool -> 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 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 -> 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 -> ?loc:Cil_types.location -> unit -> Cil_types.stmt
Returns an empty statement (of kind Instr
). See mkStmt
for ghost
and
valid_sid
arguments.
Change in Neon-20130301: adds the valid_sid
optional argument.
val dummyInstr : Cil_types.instr
A instr to serve as a placeholder
val dummyStmt : Cil_types.stmt
val mkWhile : guard:Cil_types.exp -> body:Cil_types.stmt list -> Cil_types.stmt list
Make a while loop. Can contain Break or Continue
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 Pervasives.ref list)
list -> Cil_types.block
creates a block with empty attributes from an unspecified sequence.
type
attributeClass =
| |
AttrName of bool |
| |
AttrFunType of bool |
| |
AttrType |
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 typeDeepDropAttributes : string list -> Cil_types.typ -> Cil_types.typ
Remove attributes whose name appears in the first argument that are
present anywhere in the fully expanded version of the type.
Since Oxygen-20120901
val typeDeepDropAllAttributes : Cil_types.typ -> Cil_types.typ
Remove any attribute appearing somewhere in the fully expanded
version of the type.
Since Oxygen-20120901
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
val typeHasAttributeDeep : string -> Cil_types.typ -> bool
Does the type or one of its subtypes have the given attribute. Does
not recurse through pointer types, nor inside function prototypes.
Since Oxygen-20120901
val type_remove_qualifier_attributes : Cil_types.typ -> Cil_types.typ
Remove all attributes relative to const, volatile and restrict attributes
Since Nitrogen-20111001
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
Since Oxygen-20120901
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
Since Oxygen-20120901
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
Since Oxygen-20120901
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
exception NotAnAttrParam of Cil_types.exp
The visitor
type 'a
visitAction =
| |
SkipChildren |
| |
DoChildren |
| |
DoChildrenPost of ('a -> 'a) |
| |
JustCopy |
| |
JustCopyPost of ('a -> 'a) |
| |
ChangeTo of 'a |
| |
ChangeToPost of 'a * ('a -> 'a) |
| |
ChangeDoChildrenPost of 'a * ('a -> 'a) |
Different visiting actions. 'a will be instantiated with
exp
,
instr
,
etc.
Consult the Plugin Development Guide for additional details.
val mk_behavior : ?name:string ->
?assumes:'a list ->
?requires:'a list ->
?post_cond:(Cil_types.termination_kind * 'a) list ->
?assigns:'b Cil_types.assigns ->
?allocation:'b Cil_types.allocation option ->
?extended:(string * int * 'a list) list ->
unit -> ('a, 'b) Cil_types.behavior
Since Carbon-20101201
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 default_behavior_name : string
Since Carbon-20101201
val is_default_behavior : ('a, 'b) Cil_types.behavior -> bool
val find_default_behavior : Cil_types.funspec -> Cil_types.funbehavior option
Since Carbon-20101201
val find_default_requires : ('a, 'b) Cil_types.behavior list -> 'a list
Since Carbon-20101201
Visitor mechanism
type
visitor_behavior
Visitor behavior
How the visitor should behave in front of mutable fields: in
place modification or copy of the structure. This type is abstract.
Use one of the two values below in your classes.
Consult the Plugin Development Guide for additional details.
val inplace_visit : unit -> visitor_behavior
In-place modification. Behavior of the original cil visitor.
Consult the Plugin Development Guide for additional details.
val copy_visit : Project.t -> visitor_behavior
Makes fresh copies of the mutable structures.
- preserves sharing for varinfo.
- makes fresh copy of varinfo only for declarations. Variables that are
only used in the visited AST are thus still shared with the original
AST. This allows for instance to copy a function with its
formals and local variables, and to keep the references to other
globals in the function's body.
Consult the Plugin Development Guide for additional details.
val is_copy_behavior : visitor_behavior -> bool
true iff the behavior is a copy behavior.
val reset_behavior_varinfo : visitor_behavior -> unit
resets the internal tables used by the given visitor_behavior. If you use
fresh instances of visitor for each round of transformation, this should
not be needed. In place modifications do not need that at all.
val reset_behavior_compinfo : visitor_behavior -> unit
val reset_behavior_enuminfo : visitor_behavior -> unit
val reset_behavior_enumitem : visitor_behavior -> unit
val reset_behavior_typeinfo : visitor_behavior -> unit
val reset_behavior_stmt : visitor_behavior -> unit
val reset_behavior_logic_info : visitor_behavior -> unit
val reset_behavior_logic_type_info : visitor_behavior -> unit
val reset_behavior_fieldinfo : visitor_behavior -> unit
val reset_behavior_model_info : visitor_behavior -> unit
val reset_logic_var : visitor_behavior -> unit
val reset_behavior_kernel_function : visitor_behavior -> unit
val reset_behavior_fundec : visitor_behavior -> unit
val get_varinfo : visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo
retrieve the representative of a given varinfo in the current
state of the visitor
val get_compinfo : visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo
val get_enuminfo : visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo
val get_enumitem : visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem
val get_typeinfo : visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo
val get_stmt : visitor_behavior -> Cil_types.stmt -> Cil_types.stmt
val get_logic_info : visitor_behavior -> Cil_types.logic_info -> Cil_types.logic_info
val get_logic_type_info : visitor_behavior ->
Cil_types.logic_type_info -> Cil_types.logic_type_info
val get_fieldinfo : visitor_behavior -> Cil_types.fieldinfo -> Cil_types.fieldinfo
val get_model_info : visitor_behavior -> Cil_types.model_info -> Cil_types.model_info
val get_logic_var : visitor_behavior -> Cil_types.logic_var -> Cil_types.logic_var
val get_kernel_function : visitor_behavior ->
Cil_types.kernel_function -> Cil_types.kernel_function
val get_fundec : visitor_behavior -> Cil_types.fundec -> Cil_types.fundec
val get_original_varinfo : visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo
retrieve the original representative of a given copy of a varinfo
in the current state of the visitor.
val get_original_compinfo : visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo
val get_original_enuminfo : visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo
val get_original_enumitem : visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem
val get_original_typeinfo : visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo
val get_original_stmt : visitor_behavior -> Cil_types.stmt -> Cil_types.stmt
val get_original_logic_info : visitor_behavior -> Cil_types.logic_info -> Cil_types.logic_info
val get_original_logic_type_info : visitor_behavior ->
Cil_types.logic_type_info -> Cil_types.logic_type_info
val get_original_fieldinfo : visitor_behavior -> Cil_types.fieldinfo -> Cil_types.fieldinfo
val get_original_model_info : visitor_behavior -> Cil_types.model_info -> Cil_types.model_info
val get_original_logic_var : visitor_behavior -> Cil_types.logic_var -> Cil_types.logic_var
val get_original_kernel_function : visitor_behavior ->
Cil_types.kernel_function -> Cil_types.kernel_function
val get_original_fundec : visitor_behavior -> Cil_types.fundec -> Cil_types.fundec
val set_varinfo : visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo -> unit
change the representative of a given varinfo in the current
state of the visitor. Use with care (i.e. makes sure that the old one
is not referenced anywhere in the AST, or sharing will be lost.
val set_compinfo : visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo -> unit
val set_enuminfo : visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo -> unit
val set_enumitem : visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem -> unit
val set_typeinfo : visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo -> unit
val set_stmt : visitor_behavior -> Cil_types.stmt -> Cil_types.stmt -> unit
val set_logic_info : visitor_behavior -> Cil_types.logic_info -> Cil_types.logic_info -> unit
val set_logic_type_info : visitor_behavior ->
Cil_types.logic_type_info -> Cil_types.logic_type_info -> unit
val set_fieldinfo : visitor_behavior -> Cil_types.fieldinfo -> Cil_types.fieldinfo -> unit
val set_model_info : visitor_behavior -> Cil_types.model_info -> Cil_types.model_info -> unit
val set_logic_var : visitor_behavior -> Cil_types.logic_var -> Cil_types.logic_var -> unit
val set_kernel_function : visitor_behavior ->
Cil_types.kernel_function -> Cil_types.kernel_function -> unit
val set_fundec : visitor_behavior -> Cil_types.fundec -> Cil_types.fundec -> unit
val set_orig_varinfo : visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo -> unit
change the reference of a given new varinfo in the current
state of the visitor. Use with care
val set_orig_compinfo : visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo -> unit
val set_orig_enuminfo : visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo -> unit
val set_orig_enumitem : visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem -> unit
val set_orig_typeinfo : visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo -> unit
val set_orig_stmt : visitor_behavior -> Cil_types.stmt -> Cil_types.stmt -> unit
val set_orig_logic_info : visitor_behavior -> Cil_types.logic_info -> Cil_types.logic_info -> unit
val set_orig_logic_type_info : visitor_behavior ->
Cil_types.logic_type_info -> Cil_types.logic_type_info -> unit
val set_orig_fieldinfo : visitor_behavior -> Cil_types.fieldinfo -> Cil_types.fieldinfo -> unit
val set_orig_model_info : visitor_behavior -> Cil_types.model_info -> Cil_types.model_info -> unit
val set_orig_logic_var : visitor_behavior -> Cil_types.logic_var -> Cil_types.logic_var -> unit
val set_orig_kernel_function : visitor_behavior ->
Cil_types.kernel_function -> Cil_types.kernel_function -> unit
val set_orig_fundec : visitor_behavior -> Cil_types.fundec -> Cil_types.fundec -> unit
val memo_varinfo : visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo
finds a binding in new project for the given varinfo, creating one
if it does not already exists.
val memo_compinfo : visitor_behavior -> Cil_types.compinfo -> Cil_types.compinfo
val memo_enuminfo : visitor_behavior -> Cil_types.enuminfo -> Cil_types.enuminfo
val memo_enumitem : visitor_behavior -> Cil_types.enumitem -> Cil_types.enumitem
val memo_typeinfo : visitor_behavior -> Cil_types.typeinfo -> Cil_types.typeinfo
val memo_stmt : visitor_behavior -> Cil_types.stmt -> Cil_types.stmt
val memo_logic_info : visitor_behavior -> Cil_types.logic_info -> Cil_types.logic_info
val memo_logic_type_info : visitor_behavior ->
Cil_types.logic_type_info -> Cil_types.logic_type_info
val memo_fieldinfo : visitor_behavior -> Cil_types.fieldinfo -> Cil_types.fieldinfo
val memo_model_info : visitor_behavior -> Cil_types.model_info -> Cil_types.model_info
val memo_logic_var : visitor_behavior -> Cil_types.logic_var -> Cil_types.logic_var
val memo_kernel_function : visitor_behavior ->
Cil_types.kernel_function -> Cil_types.kernel_function
val memo_fundec : visitor_behavior -> Cil_types.fundec -> Cil_types.fundec
val iter_visitor_varinfo : visitor_behavior ->
(Cil_types.varinfo -> Cil_types.varinfo -> unit) -> unit
iter_visitor_varinfo vis f
iterates f
over each pair of
varinfo registered in vis
. Varinfo for the old AST is presented
to f
first.
Since Oxygen-20120901
val iter_visitor_compinfo : visitor_behavior ->
(Cil_types.compinfo -> Cil_types.compinfo -> unit) -> unit
val iter_visitor_enuminfo : visitor_behavior ->
(Cil_types.enuminfo -> Cil_types.enuminfo -> unit) -> unit
val iter_visitor_enumitem : visitor_behavior ->
(Cil_types.enumitem -> Cil_types.enumitem -> unit) -> unit
val iter_visitor_typeinfo : visitor_behavior ->
(Cil_types.typeinfo -> Cil_types.typeinfo -> unit) -> unit
val iter_visitor_stmt : visitor_behavior -> (Cil_types.stmt -> Cil_types.stmt -> unit) -> unit
val iter_visitor_logic_info : visitor_behavior ->
(Cil_types.logic_info -> Cil_types.logic_info -> unit) -> unit
val iter_visitor_logic_type_info : visitor_behavior ->
(Cil_types.logic_type_info -> Cil_types.logic_type_info -> unit) -> unit
val iter_visitor_fieldinfo : visitor_behavior ->
(Cil_types.fieldinfo -> Cil_types.fieldinfo -> unit) -> unit
val iter_visitor_model_info : visitor_behavior ->
(Cil_types.model_info -> Cil_types.model_info -> unit) -> unit
val iter_visitor_logic_var : visitor_behavior ->
(Cil_types.logic_var -> Cil_types.logic_var -> unit) -> unit
val iter_visitor_kernel_function : visitor_behavior ->
(Cil_types.kernel_function -> Cil_types.kernel_function -> unit) -> unit
val iter_visitor_fundec : visitor_behavior ->
(Cil_types.fundec -> Cil_types.fundec -> unit) -> unit
val fold_visitor_varinfo : visitor_behavior ->
(Cil_types.varinfo -> Cil_types.varinfo -> 'a -> 'a) -> 'a -> 'a
fold_visitor_varinfo vis f
folds f
over each pair of varinfo registered
in vis
. Varinfo for the old AST is presented to f
first.
Since Oxygen-20120901
val fold_visitor_compinfo : visitor_behavior ->
(Cil_types.compinfo -> Cil_types.compinfo -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_enuminfo : visitor_behavior ->
(Cil_types.enuminfo -> Cil_types.enuminfo -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_enumitem : visitor_behavior ->
(Cil_types.enumitem -> Cil_types.enumitem -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_typeinfo : visitor_behavior ->
(Cil_types.typeinfo -> Cil_types.typeinfo -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_stmt : visitor_behavior ->
(Cil_types.stmt -> Cil_types.stmt -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_logic_info : visitor_behavior ->
(Cil_types.logic_info -> Cil_types.logic_info -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_logic_type_info : visitor_behavior ->
(Cil_types.logic_type_info -> Cil_types.logic_type_info -> 'a -> 'a) ->
'a -> 'a
val fold_visitor_fieldinfo : visitor_behavior ->
(Cil_types.fieldinfo -> Cil_types.fieldinfo -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_model_info : visitor_behavior ->
(Cil_types.model_info -> Cil_types.model_info -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_logic_var : visitor_behavior ->
(Cil_types.logic_var -> Cil_types.logic_var -> 'a -> 'a) -> 'a -> 'a
val fold_visitor_kernel_function : visitor_behavior ->
(Cil_types.kernel_function -> Cil_types.kernel_function -> 'a -> 'a) ->
'a -> 'a
val fold_visitor_fundec : visitor_behavior ->
(Cil_types.fundec -> Cil_types.fundec -> 'a -> 'a) -> 'a -> 'a
Visitor class
class type cilVisitor = object
.. end
A visitor interface for traversing CIL trees.
class genericCilVisitor : visitor_behavior ->
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
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.
Consult the Plugin Development Guide for additional details.
val visitCilFileSameGlobals : cilVisitor -> Cil_types.file -> unit
A visitor for the whole file that does not change the globals (but maybe
changes things inside the globals). Use this function instead of
Cil.visitCilFile
whenever appropriate because it is more efficient for
long files.
Consult the Plugin Development Guide for additional details.
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 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 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.identified_term Cil_types.deps ->
Cil_types.identified_term Cil_types.deps
val visitCilFrom : cilVisitor ->
Cil_types.identified_term Cil_types.from ->
Cil_types.identified_term Cil_types.from
val visitCilAssigns : cilVisitor ->
Cil_types.identified_term Cil_types.assigns ->
Cil_types.identified_term Cil_types.assigns
val visitCilFrees : cilVisitor ->
Cil_types.identified_term list -> Cil_types.identified_term list
Since Oxygen-20120901
val visitCilAllocates : cilVisitor ->
Cil_types.identified_term list -> Cil_types.identified_term list
Since Oxygen-20120901
val visitCilAllocation : cilVisitor ->
Cil_types.identified_term Cil_types.allocation ->
Cil_types.identified_term Cil_types.allocation
Since Oxygen-20120901
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 ->
string * int * Cil_types.identified_predicate list ->
string * int * Cil_types.identified_predicate list
visit an extended clause of a behavior.
Since Nitrogen-20111001
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 visitCilPredicate : cilVisitor -> Cil_types.predicate -> Cil_types.predicate
val visitCilPredicateNamed : cilVisitor ->
Cil_types.predicate Cil_types.named -> Cil_types.predicate Cil_types.named
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.
Since Oxygen-20120901
val visitCilTermLval : cilVisitor -> Cil_types.term_lval -> Cil_types.term_lval
visit term_lval.
Since Nitrogen-20111001
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.
val forgcc : string -> string
Return the string 's' if we're printing output for gcc, suppres
it if we're printing for CIL to parse back in. the purpose is to
hide things from gcc that it complains about, but still be able
to do lossless transformations when CIL is the consumer
Debugging support
module CurrentLoc: State_builder.Ref
with type data = location
A reference to the current location.
val pp_thisloc : Format.formatter -> unit
Pretty-print (Cil.CurrentLoc.get ())
val currentGlobal : Cil_types.global Pervasives.ref
A reference to the current global being visited
val empty_funspec : unit -> Cil_types.funspec
Returns a dummy specification
val is_empty_funspec : Cil_types.funspec -> bool
Returns true if the given spec is empty.
val is_empty_behavior : Cil_types.funbehavior -> bool
Returns true if the given behavior is empty.
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 confusioin. Or, viceversa, you might have
added a local with a name that conflicts with a global
Optimization Passes
val peepHole2 : agressive: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 agressive
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 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.
Since Oxygen-20120901
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
exception Not_representable
val intKindForValue : Integer.t -> bool -> Cil_types.ikind
Raises Not_representable
if the bigint is not representable.
Returns the smallest kind that will hold the integer's value.
The kind will be unsigned if the 2nd argument is true.
Change in Neon-20130301: may raise Not_representable.
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 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 dExp : string -> Cil_types.exp
val dInstr : string -> Cil_types.location -> Cil_types.instr
val dGlobal : string -> Cil_types.location -> Cil_types.global
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 =
The type of argument for the interpreter
val d_formatarg : Format.formatter -> formatArg -> unit
Misc
val stmt_of_instr_list : ?loc:Cil_types.location -> Cil_types.instr list -> Cil_types.stmtkind
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
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.named -> Cil_types.predicate Cil_types.named
Bind all free variables with an universal quantifier
: Cil_types.exp -> Cil_datatype.Varinfo.Set.t
extract varinfo
elements from an exp
: Cil_types.lval -> Cil_datatype.Varinfo.Set.t
extract varinfo
elements from an lval
: Cil_types.term -> Cil_datatype.Logic_var.Set.t
extract logic_var
elements from a term
: Cil_types.predicate Cil_types.named -> Cil_datatype.Logic_var.Set.t
extract logic_var
elements from a predicate
: Cil_types.code_annotation -> Cil_datatype.Logic_label.Set.t
extract logic_label
elements from a code_annotation
: Cil_types.term -> Cil_datatype.Logic_label.Set.t
extract logic_label
elements from a term
: Cil_types.predicate Cil_types.named -> Cil_datatype.Logic_label.Set.t
extract logic_label
elements from a pred
: 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.
Raises Invalid_argument
if the lists have different lengths.
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.