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 : 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 getGlobInit : ?main_name:string -> Cil_types.file -> Cil_types.fundec
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.
module Sid:sig
..end
module Eid:sig
..end
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 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
val copyCompInfo : ?fresh:bool -> Cil_types.compinfo -> string -> Cil_types.compinfo
Cil_types.compinfo
changing the name. It also
copies the fields, and makes sure that the copied field points back to the
copied compinfo.
If fresh
is true
(the default), it will also give a fresh id to the
copy.val missingFieldName : string
val compFullName : Cil_types.compinfo -> string
val isCompleteType : ?allowZeroSizeArrays:bool -> Cil_types.typ -> bool
allowZeroSizeArrays
: defaults to false
. When true
, arrays of
size 0 (a gcc extension) are considered as completeval 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 isCharType : Cil_types.typ -> bool
val isShortType : Cil_types.typ -> bool
val isCharPtrType : Cil_types.typ -> bool
val isCharArrayType : Cil_types.typ -> bool
val isIntegralType : Cil_types.typ -> bool
val isIntegralOrPointerType : Cil_types.typ -> bool
val isLogicIntegralType : 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 isPointerType : Cil_types.typ -> bool
val isTypeTagType : Cil_types.logic_type -> bool
val isFunctionType : Cil_types.typ -> 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 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 -> 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 first unnamed 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
val makeLocalVar : Cil_types.fundec ->
?scope:Cil_types.block ->
?temp:bool -> ?insert:bool -> 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.val makeTempVar : Cil_types.fundec ->
?insert:bool ->
?name:string ->
?descr:string -> ?descrpure:bool -> 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 -> 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 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 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 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 -> 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 -> Cil_types.instr -> Cil_types.stmt
Cil.mkStmt
for the signification of the optional args.val mkEmptyStmt : ?ghost:bool ->
?valid_sid:bool -> ?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 ->
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.
As usual, ghost
defaults to false
. loc
defaults to the location of
the expression itself.
val mkWhile : guard:Cil_types.exp -> body:Cil_types.stmt list -> Cil_types.stmt list
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 typeDeepDropAttributes : string list -> Cil_types.typ -> Cil_types.typ
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.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 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
exception NotAnAttrParam of Cil_types.exp
val isVolatileType : Cil_types.typ -> bool
"volatile"
qualifier from the type of an l-value (do not follow pointer)val 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
type
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
val copy_visit : Project.t -> visitor_behavior
val refresh_visit : Project.t -> visitor_behavior
Cil.copy_visit
, only
varinfo that are declared in the scope of the visit will be copied and
provided with a new id.val is_fresh_behavior : visitor_behavior -> bool
false
for an inplace visitor.val is_copy_behavior : visitor_behavior -> bool
val reset_behavior_varinfo : visitor_behavior -> unit
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
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
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
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
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 unset_varinfo : visitor_behavior -> Cil_types.varinfo -> unit
val unset_compinfo : visitor_behavior -> Cil_types.compinfo -> unit
val unset_enuminfo : visitor_behavior -> Cil_types.enuminfo -> unit
val unset_enumitem : visitor_behavior -> Cil_types.enumitem -> unit
val unset_typeinfo : visitor_behavior -> Cil_types.typeinfo -> unit
val unset_stmt : visitor_behavior -> Cil_types.stmt -> unit
val unset_logic_info : visitor_behavior -> Cil_types.logic_info -> unit
val unset_logic_type_info : visitor_behavior -> Cil_types.logic_type_info -> unit
val unset_fieldinfo : visitor_behavior -> Cil_types.fieldinfo -> unit
val unset_model_info : visitor_behavior -> Cil_types.model_info -> unit
val unset_logic_var : visitor_behavior -> Cil_types.logic_var -> unit
val unset_kernel_function : visitor_behavior -> Cil_types.kernel_function -> unit
val unset_fundec : visitor_behavior -> Cil_types.fundec -> unit
val unset_orig_varinfo : visitor_behavior -> Cil_types.varinfo -> unit
val unset_orig_compinfo : visitor_behavior -> Cil_types.compinfo -> unit
val unset_orig_enuminfo : visitor_behavior -> Cil_types.enuminfo -> unit
val unset_orig_enumitem : visitor_behavior -> Cil_types.enumitem -> unit
val unset_orig_typeinfo : visitor_behavior -> Cil_types.typeinfo -> unit
val unset_orig_stmt : visitor_behavior -> Cil_types.stmt -> unit
val unset_orig_logic_info : visitor_behavior -> Cil_types.logic_info -> unit
val unset_orig_logic_type_info : visitor_behavior -> Cil_types.logic_type_info -> unit
val unset_orig_fieldinfo : visitor_behavior -> Cil_types.fieldinfo -> unit
val unset_orig_model_info : visitor_behavior -> Cil_types.model_info -> unit
val unset_orig_logic_var : visitor_behavior -> Cil_types.logic_var -> unit
val unset_orig_kernel_function : visitor_behavior -> Cil_types.kernel_function -> unit
val unset_orig_fundec : visitor_behavior -> Cil_types.fundec -> unit
val memo_varinfo : visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo
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.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.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
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 ->
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
(in which case it can't be marked as transient anyways).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 block_of_transient : Cil_types.block -> Cil_types.block
val dependency_on_ast : State.t -> unit
val set_dependencies_of_ast : State.t -> unit
Cil.dependency_on_ast
depend on the given state. Should only be used
once when creating the AST state.val pp_typ_ref : (Format.formatter -> Cil_types.typ -> unit) Pervasives.ref
val pp_global_ref : (Format.formatter -> Cil_types.global -> unit) Pervasives.ref
val pp_exp_ref : (Format.formatter -> Cil_types.exp -> unit) Pervasives.ref
val pp_lval_ref : (Format.formatter -> Cil_types.lval -> unit) Pervasives.ref
val pp_ikind_ref : (Format.formatter -> Cil_types.ikind -> unit) Pervasives.ref
val pp_attribute_ref : (Format.formatter -> Cil_types.attribute -> unit) Pervasives.ref
val pp_attributes_ref : (Format.formatter -> Cil_types.attribute list -> unit) Pervasives.ref