module Cil:sig
..end
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.
module Frama_c_builtins:State_builder.Hashtbl
with type key = string and type data = Cil_types.varinfo
val is_builtin : Cil_types.varinfo -> bool
val is_unused_builtin : Cil_types.varinfo -> bool
val is_special_builtin : string -> bool
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
val add_special_builtin_family : (string -> bool) -> unit
val init_builtins : unit -> unit
val initCIL : initLogicBuiltins:(unit -> unit) -> Cil_types.mach -> unit
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.type
theMachine = private {
|
mutable useLogicalOperators : |
(* |
Whether to use the logical operands LAnd and LOr. By default, do not
use them because they are unlike other expressions and do not
evaluate both of their operands
| *) |
|
mutable theMachine : |
|||
|
mutable lowerConstants : |
(* |
Do lower constants (default true)
| *) |
|
mutable insertImplicitCasts : |
(* |
Do insert implicit casts (default true)
| *) |
|
mutable underscore_name : |
(* |
Whether the compiler generates assembly labels by prepending "_" to
the identifier. That is, will function foo() have the label "foo", or
"_foo"?
| *) |
|
mutable stringLiteralType : |
|||
|
mutable upointKind : |
(* |
An unsigned integer type that fits pointers.
| *) |
|
mutable upointType : |
|||
|
mutable wcharKind : |
(* |
An integer type that fits wchar_t.
| *) |
|
mutable wcharType : |
|||
|
mutable ptrdiffKind : |
(* |
An integer type that fits ptrdiff_t.
| *) |
|
mutable ptrdiffType : |
|||
|
mutable typeOfSizeOf : |
(* |
An integer type that is the type of sizeof.
| *) |
|
mutable kindOfSizeOf : |
(* |
The integer kind of
Cil.typeOfSizeOf . | *) |
val theMachine : theMachine
val selfMachine : State.t
val selfMachine_is_computed : ?project:Project.project -> unit -> bool
val msvcMode : unit -> bool
val gccMode : unit -> bool
val emptyFunctionFromVI : Cil_types.varinfo -> Cil_types.fundec
val emptyFunction : string -> Cil_types.fundec
val setFormals : Cil_types.fundec -> Cil_types.varinfo list -> unit
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
val setReturnTypeVI : Cil_types.varinfo -> Cil_types.typ -> unit
val setReturnType : Cil_types.fundec -> Cil_types.typ -> unit
val setFunctionType : Cil_types.fundec -> Cil_types.typ -> unit
val setFunctionTypeMakeFormals : Cil_types.fundec -> Cil_types.typ -> unit
val setMaxId : Cil_types.fundec -> unit
Cil.makeLocalVar
or
Cil.makeTempVar
.val selfFormalsDecl : State.t
val makeFormalsVarDecl : ?ghost:bool ->
string * Cil_types.typ * Cil_types.attributes -> Cil_types.varinfo
val setFormalsDecl : Cil_types.varinfo -> Cil_types.typ -> unit
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
val unsafeSetFormalsDecl : Cil_types.varinfo -> Cil_types.varinfo list -> unit
val iterFormalsDecl : (Cil_types.varinfo -> Cil_types.varinfo list -> unit) -> unit
val getFormalsDecl : Cil_types.varinfo -> Cil_types.varinfo list
Cil.setFormalsDecl
.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
val iterGlobals : Cil_types.file -> (Cil_types.global -> unit) -> unit
val foldGlobals : Cil_types.file -> ('a -> Cil_types.global -> 'a) -> 'a -> 'a
val mapGlobals : Cil_types.file -> (Cil_types.global -> Cil_types.global) -> unit
val findOrCreateFunc : Cil_types.file -> string -> Cil_types.typ -> Cil_types.varinfo
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
val copy_exp : Cil_types.exp -> Cil_types.exp
val dummy_exp : Cil_types.exp_node -> Cil_types.exp
val is_case_label : Cil_types.label -> bool
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
val invalidStmt : Cil_types.stmt
module Builtin_functions:State_builder.Hashtbl
with type key = string and type data = typ * typ list * bool
!msvcMode
).
val builtinLoc : Cil_types.location
val range_loc : Cil_types.location -> Cil_types.location -> Cil_types.location
val makeZeroInit : loc:Cil_types.location -> Cil_types.typ -> Cil_types.init
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
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
val voidType : Cil_types.typ
val isVoidType : Cil_types.typ -> bool
val isVoidPtrType : Cil_types.typ -> bool
val intType : Cil_types.typ
val uintType : Cil_types.typ
val longType : Cil_types.typ
val longLongType : Cil_types.typ
val ulongType : Cil_types.typ
val ulongLongType : Cil_types.typ
val uint16_t : unit -> Cil_types.typ
val uint32_t : unit -> Cil_types.typ
val uint64_t : unit -> Cil_types.typ
val charType : Cil_types.typ
val scharType : Cil_types.typ
val ucharType : Cil_types.typ
val charPtrType : Cil_types.typ
val scharPtrType : Cil_types.typ
val ucharPtrType : Cil_types.typ
val charConstPtrType : Cil_types.typ
val voidPtrType : Cil_types.typ
val voidConstPtrType : Cil_types.typ
val intPtrType : Cil_types.typ
val uintPtrType : Cil_types.typ
val floatType : Cil_types.typ
val doubleType : Cil_types.typ
val longDoubleType : Cil_types.typ
val isSignedInteger : Cil_types.typ -> bool
val isUnsignedInteger : Cil_types.typ -> bool
val missingFieldName : string
val compFullName : Cil_types.compinfo -> string
val isCompleteType : ?allowZeroSizeArrays:bool -> Cil_types.typ -> bool
allowZeroSizeArrays
: indicates whether arrays of
size 0 (a gcc extension) are considered as complete. Default value
depends on the current machdep.val has_flexible_array_member : Cil_types.typ -> bool
true
iff the given type is a struct
whose last field is a flexible
array member. When in gcc mode, a zero-sized array is identified with a
FAM for this purpose.val unrollType : Cil_types.typ -> Cil_types.typ
TNamed
. Will collect all attributes appearing in TNamed
!!!val unrollTypeDeep : Cil_types.typ -> Cil_types.typ
TPtr
, TFun
or TArray
. Does not unroll the types of fields in TComp
types. Will collect all attributesval separateStorageModifiers : Cil_types.attribute list ->
Cil_types.attribute list * Cil_types.attribute list
val arithmeticConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ
val integralPromotion : Cil_types.typ -> Cil_types.typ
val isAnyCharType : Cil_types.typ -> bool
val isCharType : Cil_types.typ -> bool
signed char
nor unsigned char
).isAnyCharType
val isShortType : Cil_types.typ -> bool
val isAnyCharPtrType : Cil_types.typ -> bool
val isCharPtrType : Cil_types.typ -> bool
signed char
nor unsigned char
).isAnyCharPtrType
val isCharConstPtrType : Cil_types.typ -> bool
val isAnyCharArrayType : Cil_types.typ -> bool
val isCharArrayType : Cil_types.typ -> bool
isAnyCharArrayType
val isIntegralType : Cil_types.typ -> bool
val isBoolType : Cil_types.typ -> bool
_Bool
val isLogicPureBooleanType : Cil_types.logic_type -> bool
_Bool
or boolean
.val isIntegralOrPointerType : Cil_types.typ -> bool
val isLogicIntegralType : Cil_types.logic_type -> bool
val isLogicBooleanType : Cil_types.logic_type -> bool
val isFloatingType : Cil_types.typ -> bool
val isLogicFloatType : Cil_types.logic_type -> bool
val isLogicRealOrFloatType : Cil_types.logic_type -> bool
val isLogicRealType : Cil_types.logic_type -> bool
val isArithmeticType : Cil_types.typ -> bool
val isArithmeticOrPointerType : Cil_types.typ -> bool
val isLogicArithmeticType : Cil_types.logic_type -> bool
val isFunctionType : Cil_types.typ -> bool
val isLogicFunctionType : Cil_types.logic_type -> bool
val isPointerType : Cil_types.typ -> bool
val isFunPtrType : Cil_types.typ -> bool
val isLogicFunPtrType : Cil_types.logic_type -> bool
val isTypeTagType : Cil_types.logic_type -> bool
val isVariadicListType : Cil_types.typ -> bool
val argsToList : (string * Cil_types.typ * Cil_types.attributes) list option ->
(string * Cil_types.typ * Cil_types.attributes) list
val argsToPairOfLists : (string * Cil_types.typ * Cil_types.attributes) list option ->
(string * Cil_types.typ * Cil_types.attributes) list *
(string * Cil_types.typ * Cil_types.attributes) list
val isArrayType : Cil_types.typ -> bool
val isStructOrUnionType : Cil_types.typ -> bool
exception LenOfArray
Cil.lenOfArray
fails either because the length is None
or because it is a non-constant expressionval lenOfArray : Cil_types.exp option -> int
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
type
existsAction =
| |
ExistsTrue |
(* |
We have found it
| *) |
| |
ExistsFalse |
(* |
Stop processing this branch
| *) |
| |
ExistsMaybe |
(* |
This node is not what we are
looking for but maybe its
successors are
| *) |
existsType
val existsType : (Cil_types.typ -> existsAction) -> Cil_types.typ -> bool
val splitFunctionType : Cil_types.typ ->
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
val splitFunctionTypeVI : Cil_types.varinfo ->
Cil_types.typ * (string * Cil_types.typ * Cil_types.attributes) list option *
bool * Cil_types.attributes
val makeVarinfo : ?source:bool ->
?temp:bool ->
?referenced:bool ->
?ghost:bool ->
?loc:Cil_datatype.Location.t ->
bool -> bool -> string -> Cil_types.typ -> Cil_types.varinfo
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
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:
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
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
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
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
source
defaults to true
. temp
defaults to false
.val copyVarinfo : Cil_types.varinfo -> string -> Cil_types.varinfo
varinfo
and assign a new identifier.
If the original varinfo has an associated logic var, it is copied too and
associated to the copied varinfoval update_var_type : Cil_types.varinfo -> Cil_types.typ -> unit
val isBitfield : Cil_types.lval -> bool
val lastOffset : Cil_types.offset -> Cil_types.offset
val addOffsetLval : Cil_types.offset -> Cil_types.lval -> Cil_types.lval
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
NoOffset
then the original lval
did not have an offset.val removeOffset : Cil_types.offset -> Cil_types.offset * Cil_types.offset
NoOffset
then the original lval
did not have an offset.val typeOfLval : Cil_types.lval -> Cil_types.typ
val typeOfLhost : Cil_types.lhost -> Cil_types.typ
val typeOfTermLval : Cil_types.term_lval -> Cil_types.logic_type
typeOfLval
for terms.val typeOffset : Cil_types.typ -> Cil_types.offset -> Cil_types.typ
val typeTermOffset : Cil_types.logic_type -> Cil_types.term_offset -> Cil_types.logic_type
typeOffset
for terms.val typeOfInit : Cil_types.init -> Cil_types.typ
val is_modifiable_lval : Cil_types.lval -> bool
val zero : loc:Cil_datatype.Location.t -> Cil_types.exp
val one : loc:Cil_datatype.Location.t -> Cil_types.exp
val mone : loc:Cil_datatype.Location.t -> Cil_types.exp
val kinteger64 : loc:Cil_types.location ->
?repr:string -> ?kind:Cil_types.ikind -> Integer.t -> Cil_types.exp
kind
is given, and the integer does not fit
inside the type. The integer can have an optional literal representation
repr
.Not_representable
if no ikind is provided and the integer is not
representable.val kinteger : loc:Cil_types.location -> Cil_types.ikind -> int -> Cil_types.exp
val integer : loc:Cil_types.location -> int -> Cil_types.exp
val kfloat : loc:Cil_types.location -> Cil_types.fkind -> float -> Cil_types.exp
val isInteger : Cil_types.exp -> Integer.t option
val isConstant : Cil_types.exp -> bool
val isIntegerConstant : Cil_types.exp -> bool
val isConstantOffset : Cil_types.offset -> bool
val isZero : Cil_types.exp -> bool
val isLogicZero : Cil_types.term -> bool
val isLogicNull : Cil_types.term -> bool
\null
or a constant null pointerval 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
val interpret_character_constant : int64 list -> Cil_types.constant * Cil_types.typ
val charConstToInt : char -> Integer.t
val charConstToIntConstant : char -> Cil_types.constant
val constFold : bool -> Cil_types.exp -> Cil_types.exp
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
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
val constFoldTerm : bool -> Cil_types.term -> Cil_types.term
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
constFold
is done here. If the second argument is true then
will also compute compiler-dependent expressions such as sizeof
.val compareConstant : Cil_types.constant -> Cil_types.constant -> bool
true
if the two constant are equal.val increm : Cil_types.exp -> int -> Cil_types.exp
val increm64 : Cil_types.exp -> Integer.t -> Cil_types.exp
val var : Cil_types.varinfo -> Cil_types.lval
val evar : ?loc:Cil_types.location -> Cil_types.varinfo -> Cil_types.exp
val mkAddrOf : loc:Cil_types.location -> Cil_types.lval -> Cil_types.exp
0
"val mkAddrOfVi : Cil_types.varinfo -> Cil_types.exp
val mkAddrOrStartOf : loc:Cil_types.location -> Cil_types.lval -> Cil_types.exp
val mkMem : addr:Cil_types.exp -> off:Cil_types.offset -> Cil_types.lval
val mkBinOp : loc:Cil_types.location ->
Cil_types.binop -> Cil_types.exp -> Cil_types.exp -> Cil_types.exp
val mkBinOp_safe_ptr_cmp : loc:Cil_types.location ->
Cil_types.binop -> Cil_types.exp -> Cil_types.exp -> Cil_types.exp
Cil.mkBinOp
, but performs a systematic cast (unless one of the
arguments is 0
) of pointers into uintptr_t
during comparisons,
making such operation defined even if the pointers do not share
the same base. This was the behavior of Cil.mkBinOp
prior to the
introduction of this function.val mkTermMem : addr:Cil_types.term -> off:Cil_types.term_offset -> Cil_types.term_lval
mkMem
for terms.val mkString : loc:Cil_types.location -> string -> Cil_types.exp
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.force
argumentval mkCastT : ?force:bool ->
e:Cil_types.exp -> oldt:Cil_types.typ -> newt:Cil_types.typ -> Cil_types.exp
force
is true
(default is false
)force
argumentval mkCast : ?force:bool -> e:Cil_types.exp -> newt:Cil_types.typ -> Cil_types.exp
val stripTermCasts : Cil_types.term -> Cil_types.term
stripCasts
for terms.val stripCasts : Cil_types.exp -> Cil_types.exp
val stripInfo : Cil_types.exp -> Cil_types.exp
val stripCastsAndInfo : Cil_types.exp -> Cil_types.exp
val stripCastsButLastInfo : Cil_types.exp -> Cil_types.exp
val exp_info_of_term : Cil_types.term -> Cil_types.exp_info
val term_of_exp_info : Cil_types.location ->
Cil_types.term_node -> Cil_types.exp_info -> Cil_types.term
val map_under_info : (Cil_types.exp -> Cil_types.exp) -> Cil_types.exp -> Cil_types.exp
val app_under_info : (Cil_types.exp -> unit) -> Cil_types.exp -> unit
val typeOf : Cil_types.exp -> Cil_types.typ
val typeOf_pointed : Cil_types.typ -> Cil_types.typ
val typeOf_array_elem : Cil_types.typ -> Cil_types.typ
val is_fully_arithmetic : Cil_types.typ -> bool
true
whenever the type contains only arithmetic typesval parseInt : string -> Integer.t
val parseIntExp : loc:Cil_types.location -> string -> Cil_types.exp
val parseIntLogic : loc:Cil_types.location -> string -> Cil_types.term
val appears_in_expr : Cil_types.varinfo -> Cil_types.exp -> bool
val mkStmt : ?ghost:bool ->
?valid_sid:bool ->
?sattr:Cil_types.attributes -> Cil_types.stmtkind -> Cil_types.stmt
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 listval 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
val mkBlockNonScoping : Cil_types.stmt list -> Cil_types.block
val mkStmtCfgBlock : Cil_types.stmt list -> Cil_types.stmt
val mkStmtOneInstr : ?ghost:bool ->
?valid_sid:bool ->
?sattr:Cil_types.attributes -> Cil_types.instr -> Cil_types.stmt
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
Instr
). See mkStmt
for ghost
and
valid_sid
arguments.valid_sid
optional argument.val dummyInstr : Cil_types.instr
val dummyStmt : Cil_types.stmt
dummyInstr
.val mkPureExprInstr : fundec:Cil_types.fundec ->
scope:Cil_types.block ->
?loc:Cil_types.location -> Cil_types.exp -> Cil_types.instr
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
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
.
Change in Chlorine-20180501: lift optional arg valid_sid from mkStmt
instead
of relying on ill-fated default.
val mkLoop : ?sattr:Cil_types.attributes ->
guard:Cil_types.exp -> body:Cil_types.stmt list -> Cil_types.stmt list
sattr
;
it is a While loop if unspecified.val mkForIncr : iter:Cil_types.varinfo ->
first:Cil_types.exp ->
stopat:Cil_types.exp ->
incr:Cil_types.exp -> body:Cil_types.stmt list -> Cil_types.stmt list
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
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
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
.Fatal
error if v
is not a local variable of b
with an
initializer.val has_extern_local_init : Cil_types.block -> bool
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.labelstype
attributeClass =
| |
AttrName of |
(* |
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 |
(* |
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
| *) |
val registerAttribute : string -> attributeClass -> unit
val removeAttribute : string -> unit
val attributeClass : string -> attributeClass
val partitionAttributes : default:attributeClass ->
Cil_types.attributes ->
Cil_types.attribute list * Cil_types.attribute list *
Cil_types.attribute list
val addAttribute : Cil_types.attribute -> Cil_types.attributes -> Cil_types.attributes
val addAttributes : Cil_types.attribute list -> Cil_types.attributes -> Cil_types.attributes
val dropAttribute : string -> Cil_types.attributes -> Cil_types.attributes
val dropAttributes : string list -> Cil_types.attributes -> Cil_types.attributes
val frama_c_ghost_formal : string
val frama_c_mutable : string
val frama_c_init_obj : string
val is_mutable_or_initialized : Cil_types.lval -> bool
true
if the given lval is allowed to be assigned to thanks to
a frama_c_init_obj
or a frama_c_mutable
attribute.val isGhostFormalVarinfo : Cil_types.varinfo -> bool
true
if the given varinfo is a ghost formal variable.val isGhostFormalVarDecl : string * Cil_types.typ * Cil_types.attributes -> bool
true
if the given formal declaration corresponds to a ghost formal variable.val typeDeepDropAttributes : string list -> Cil_types.typ -> Cil_types.typ
Cil.typeRemoveAttributesDeep
instead,
which does not traverse pointers and function types, or
Cil.typeDeepDropAllAttributes
, which will give a pristine version of the
type, without any attributes.val typeDeepDropAllAttributes : Cil_types.typ -> Cil_types.typ
val filterAttributes : string -> Cil_types.attributes -> Cil_types.attributes
val hasAttribute : string -> Cil_types.attributes -> bool
val mkAttrAnnot : string -> string
val attributeName : Cil_types.attribute -> string
val findAttribute : string -> Cil_types.attribute list -> Cil_types.attrparam list
val typeAttrs : Cil_types.typ -> Cil_types.attribute list
val typeAttr : Cil_types.typ -> Cil_types.attribute list
val setTypeAttrs : Cil_types.typ -> Cil_types.attributes -> Cil_types.typ
val typeAddAttributes : Cil_types.attribute list -> Cil_types.typ -> Cil_types.typ
val typeRemoveAttributes : string list -> Cil_types.typ -> Cil_types.typ
val typeRemoveAllAttributes : Cil_types.typ -> Cil_types.typ
val typeRemoveAttributesDeep : string list -> Cil_types.typ -> Cil_types.typ
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
val typeHasQualifier : string -> Cil_types.typ -> bool
Cil.typeHasAttribute
.
For l-values, both functions return the same results, as l-values cannot
have array type.val typeHasAttributeDeep : string -> Cil_types.typ -> bool
val typeHasAttributeMemoryBlock : string -> Cil_types.typ -> bool
typeHasAttributeMemoryBlock attr t
is
true
iff at least one component of an object of type t
has attribute
attr
. In other words, it searches for attr
under aggregates, but not
under pointers.val type_remove_qualifier_attributes : Cil_types.typ -> Cil_types.typ
val type_remove_qualifier_attributes_deep : Cil_types.typ -> Cil_types.typ
val type_remove_attributes_for_c_cast : Cil_types.typ -> Cil_types.typ
val type_remove_attributes_for_logic_type : Cil_types.typ -> Cil_types.typ
val filter_qualifier_attributes : Cil_types.attributes -> Cil_types.attributes
val splitArrayAttributes : Cil_types.attributes -> Cil_types.attributes * Cil_types.attributes
val bitfield_attribute_name : string
AINT size
argument when querying the type of a field that is a bitfieldval expToAttrParam : Cil_types.exp -> Cil_types.attrparam
val global_annotation_attributes : Cil_types.global_annotation -> Cil_types.attributes
val global_attributes : Cil_types.global -> Cil_types.attributes
exception NotAnAttrParam of Cil_types.exp
val isConstType : Cil_types.typ -> bool
"const"
qualifier from the type of an l-value (do not follow pointer)"const"
qualifierval isVolatileType : Cil_types.typ -> bool
"volatile"
qualifier from the type of an l-value (do not follow pointer)"volatile"
qualifierval isVolatileLogicType : Cil_types.logic_type -> bool
"volatile"
qualifier from a logic typeval isVolatileLval : Cil_types.lval -> bool
val isVolatileTermLval : Cil_types.term_lval -> bool
type 'a
visitAction =
| |
SkipChildren |
(* |
Do not visit the children. Return the node as it is.
Consult the Plugin Development Guide for additional details. | *) |
| |
DoChildren |
(* |
Continue with the children of this node. Rebuild the node on
return if any of the children changes (use == test).
Consult the Plugin Development Guide for additional details. | *) |
| |
DoChildrenPost of |
(* |
visit the children, and apply the given function to the result.
Consult the Plugin Development Guide for additional details. | *) |
| |
JustCopy |
(* |
visit the children, but only to make the necessary copies
(only useful for copy visitor).
Consult the Plugin Development Guide for additional details. | *) |
| |
JustCopyPost of |
(* |
same as JustCopy + applies the given function to the result.
Consult the Plugin Development Guide for additional details. | *) |
| |
ChangeTo of |
(* |
Replace the expression with the given one.
Consult the Plugin Development Guide for additional details. | *) |
| |
ChangeToPost of |
(* |
applies the expression to the function and gives back the result.
Useful to insert some actions in an inheritance chain.
Consult the Plugin Development Guide for additional details. | *) |
| |
ChangeDoChildrenPost of |
(* |
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.
Consult the Plugin Development Guide for additional details. | *) |
exp
, instr
,
etc.val mk_behavior : ?name:string ->
?assumes:Cil_types.identified_predicate list ->
?requires:Cil_types.identified_predicate list ->
?post_cond:(Cil_types.termination_kind * Cil_types.identified_predicate) list ->
?assigns:Cil_types.assigns ->
?allocation:Cil_types.allocation ->
?extended:Cil_types.acsl_extension list -> unit -> Cil_types.behavior
val default_behavior_name : string
val is_default_behavior : Cil_types.behavior -> bool
val find_default_behavior : Cil_types.funspec -> Cil_types.funbehavior option
val find_default_requires : Cil_types.behavior list -> Cil_types.identified_predicate list
class type cilVisitor =object
..end
val register_behavior_extension : string ->
(cilVisitor ->
Cil_types.acsl_extension_kind ->
Cil_types.acsl_extension_kind visitAction) ->
unit
DoChildren
, which ends up visiting
each identified predicate in the list and leave the id as is.class genericCilVisitor :Visitor_behavior.t ->
cilVisitor
class nopCilVisitor :cilVisitor
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
mechanismval doVisitList : 'visitor ->
'visitor ->
('a -> 'a) ->
('a -> 'a list visitAction) -> ('visitor -> 'a -> 'a) -> 'a -> 'a list
val visitCilFileCopy : cilVisitor -> Cil_types.file -> Cil_types.file
Cil.visitCilFileSameGlobals
if your visitor will
not change the list of globals.val visitCilFile : cilVisitor -> Cil_types.file -> unit
val visitCilFileSameGlobals : cilVisitor -> Cil_types.file -> unit
Cil.visitCilFile
whenever appropriate because it is more efficient for long files.val visitCilGlobal : cilVisitor -> Cil_types.global -> Cil_types.global list
val visitCilFunction : cilVisitor -> Cil_types.fundec -> Cil_types.fundec
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
val visitCilOffset : cilVisitor -> Cil_types.offset -> Cil_types.offset
val visitCilInitOffset : cilVisitor -> Cil_types.offset -> Cil_types.offset
val visitCilLocal_init : cilVisitor ->
Cil_types.varinfo -> Cil_types.local_init -> Cil_types.local_init
val visitCilInstr : cilVisitor -> Cil_types.instr -> Cil_types.instr list
val visitCilStmt : cilVisitor -> Cil_types.stmt -> Cil_types.stmt
val visitCilBlock : cilVisitor -> Cil_types.block -> Cil_types.block
val transient_block : Cil_types.block -> Cil_types.block
Fatal
error if the given block attempts to declare local variables
and contain definitions of local variables that are not part of the block.val is_transient_block : Cil_types.block -> bool
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 possibleval visitCilType : cilVisitor -> Cil_types.typ -> Cil_types.typ
val visitCilVarDecl : cilVisitor -> Cil_types.varinfo -> Cil_types.varinfo
val visitCilInit : cilVisitor ->
Cil_types.varinfo -> Cil_types.offset -> Cil_types.init -> Cil_types.init
val visitCilAttributes : cilVisitor -> Cil_types.attribute list -> Cil_types.attribute list
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
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
val visitCilTermLval : cilVisitor -> Cil_types.term_lval -> Cil_types.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
val childrenBehavior : cilVisitor -> Cil_types.funbehavior -> Cil_types.funbehavior
val is_skip : Cil_types.stmtkind -> bool
val constFoldVisitor : bool -> cilVisitor
module CurrentLoc:State_builder.Ref
with type data = location
val pp_thisloc : Format.formatter -> unit
(Cil.CurrentLoc.get ())
val empty_funspec : unit -> Cil_types.funspec
val is_empty_funspec : Cil_types.funspec -> bool
val is_empty_behavior : Cil_types.funbehavior -> bool
val uniqueVarNames : Cil_types.file -> unit
val peepHole2 : aggressive:bool ->
(Cil_types.stmt * Cil_types.stmt -> Cil_types.stmt list option) ->
Cil_types.stmt list -> Cil_types.stmt list
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
peepHole2
except that the optimization window consists of
one statement, not twoexception SizeOfError of string * Cil_types.typ
val empty_size_cache : unit -> Cil_types.bitsSizeofTypCache
Not_Computed
val unsignedVersionOf : Cil_types.ikind -> Cil_types.ikind
val intKindForSize : int -> bool -> Cil_types.ikind
val floatKindForSize : int -> Cil_types.fkind
val bitsSizeOf : Cil_types.typ -> int
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
Cil.SizeOfError
when it cannot
compute the size.val bytesSizeOfInt : Cil_types.ikind -> int
val bitsSizeOfInt : Cil_types.ikind -> int
val isSigned : Cil_types.ikind -> bool
val bitsSizeOfBitfield : Cil_types.typ -> int
val rank : Cil_types.ikind -> int
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
val truncateInteger64 : Cil_types.ikind -> Integer.t -> Integer.t * bool
val max_signed_number : int -> Integer.t
val min_signed_number : int -> Integer.t
val max_unsigned_number : int -> Integer.t
val fitsInInt : Cil_types.ikind -> Integer.t -> bool
exception Not_representable
Cil.intKindForValue
.val intKindForValue : Integer.t -> bool -> Cil_types.ikind
Not_representable
if the bigint is not representable.val sizeOf : loc:Cil_types.location -> Cil_types.typ -> Cil_types.exp
Cil.initCIL
.val bytesAlignOf : Cil_types.typ -> int
Cil.initCIL
.val intOfAttrparam : Cil_types.attrparam -> int option
intOfAttrparam a
tries to const-fold a
into a numeric value.
Returns Some n
if it succeeds, None
otherwise.val bitsOffset : Cil_types.typ -> Cil_types.offset -> int * int
Cil.SizeOfError
when it cannot compute
the size. This function is architecture dependent, so you should only call
this after you call Cil.initCIL
.val mapNoCopy : ('a -> 'a) -> 'a list -> 'a list
val optMapNoCopy : ('a -> 'a) -> 'a option -> 'a option
val mapNoCopyList : ('a -> 'a list) -> 'a list -> 'a list
val startsWith : string -> string -> bool
type
formatArg =
| |
Fe of |
|||
| |
Feo of |
(* |
For array lengths
| *) |
| |
Fu of |
|||
| |
Fb of |
|||
| |
Fk of |
|||
| |
FE of |
(* |
For arguments in a function call
| *) |
| |
Ff of |
(* |
For a formal argument
| *) |
| |
FF of |
(* |
For formal argument lists
| *) |
| |
Fva of |
(* |
For the ellipsis in a function type
| *) |
| |
Fv of |
|||
| |
Fl of |
|||
| |
Flo of |
|||
| |
Fo of |
|||
| |
Fc of |
|||
| |
Fi of |
|||
| |
FI of |
|||
| |
Ft of |
|||
| |
Fd of |
|||
| |
Fg of |
|||
| |
Fs of |
|||
| |
FS of |
|||
| |
FA of |
|||
| |
Fp of |
|||
| |
FP of |
|||
| |
FX of |
val d_formatarg : Format.formatter -> formatArg -> unit
val stmt_of_instr_list : ?loc:Cil_types.location -> Cil_types.instr list -> Cil_types.stmtkind
bscoping=false
val cvar_to_lvar : Cil_types.varinfo -> Cil_types.logic_var
val make_temp_logic_var : Cil_types.logic_type -> Cil_types.logic_var
val lzero : ?loc:Cil_types.location -> unit -> Cil_types.term
val lone : ?loc:Cil_types.location -> unit -> Cil_types.term
val lmone : ?loc:Cil_types.location -> unit -> Cil_types.term
val lconstant : ?loc:Cil_types.location -> Integer.t -> Cil_types.term
val close_predicate : Cil_types.predicate -> Cil_types.predicate
val extract_varinfos_from_exp : Cil_types.exp -> Cil_datatype.Varinfo.Set.t
varinfo
elements from an exp
val extract_varinfos_from_lval : Cil_types.lval -> Cil_datatype.Varinfo.Set.t
varinfo
elements from an lval
val extract_free_logicvars_from_term : Cil_types.term -> Cil_datatype.Logic_var.Set.t
logic_var
elements from a term
val extract_free_logicvars_from_predicate : Cil_types.predicate -> Cil_datatype.Logic_var.Set.t
logic_var
elements from a predicate
val extract_labels_from_annot : Cil_types.code_annotation -> Cil_datatype.Logic_label.Set.t
logic_label
elements from a code_annotation
val extract_labels_from_term : Cil_types.term -> Cil_datatype.Logic_label.Set.t
logic_label
elements from a term
val extract_labels_from_pred : Cil_types.predicate -> Cil_datatype.Logic_label.Set.t
logic_label
elements from a pred
val extract_stmts_from_labels : Cil_datatype.Logic_label.Set.t -> Cil_datatype.Stmt.Set.t
stmt
elements from logic_label
elementsval create_alpha_renaming : Cil_types.varinfo list -> Cil_types.varinfo list -> cilVisitor
Invalid_argument
if the lists have different lengths.val separate_switch_succs : Cil_types.stmt -> Cil_types.stmt list * Cil_types.stmt
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
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.