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 stripConstLocalType : Cil_types.typ -> Cil_types.typ
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' t' acc -> myInit (addOffsetLval lv off') i' acc) ~ct:ct ~initl:initl ~acc: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 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
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 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 mkPureExpr : ?ghost:bool ->
fundec:Cil_types.fundec ->
?loc:Cil_types.location -> Cil_types.exp -> Cil_types.stmt
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
type
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 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
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.identified_term Cil_types.assigns ->
?allocation:Cil_types.identified_term 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 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 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 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.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
val visitCilAllocates : cilVisitor ->
Cil_types.identified_term list -> Cil_types.identified_term list
val visitCilAllocation : cilVisitor ->
Cil_types.identified_term Cil_types.allocation ->
Cil_types.identified_term 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 : agressive:bool ->
(Cil_types.stmt * Cil_types.stmt -> Cil_types.stmt list option) ->
Cil_types.stmt list -> Cil_types.stmt list
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
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 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 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
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.