module Cil_types:sig
..end
Ast.get
.type
file = {
|
mutable fileName : |
(* |
The complete file name
| *) |
|
mutable globals : |
(* |
List of globals as they will appear in the printed file
| *) |
|
mutable globinit : |
(* |
An optional global initializer function. This is a function where you
can put stuff that must be executed before the program is
started. This function, is conceptually at the end of the file,
although it is not part of the globals list. Use
Cil.getGlobInit to
create/get one. | *) |
|
mutable globinitcalled : |
(* |
Whether the global initialization function is called in main. This
should always be false if there is no global initializer. When you
create a global initialization CIL will try to insert code in main to
call it.
| *) |
Cil_types.file
using the following iterators: Cil.mapGlobals
,
Cil.iterGlobals
and Cil.foldGlobals
. You can also use the
Cil.dummyFile
when you need a Cil_types.file
as a placeholder. For
each global item CIL stores the source location where it appears (using the
type Cil_types.location
)type
global =
| |
GType of |
(* |
A typedef. All uses of type names (through the
TNamed constructor)
must be preceded in the file by a definition of the name. The string
is the defined name and always not-empty. | *) |
| |
GCompTag of |
(* |
Defines a struct/union tag with some fields. There must be one of
these for each struct/union tag that you use (through the
TComp
constructor) since this is the only context in which the fields are
printed. Consequently nested structure tag definitions must be
broken into individual definitions with the innermost structure
defined first. | *) |
| |
GCompTagDecl of |
(* |
Declares a struct/union tag. Use as a forward declaration. This is
printed without the fields.
| *) |
| |
GEnumTag of |
(* |
Declares an enumeration tag with some fields. There must be one of
these for each enumeration tag that you use (through the
TEnum
constructor) since this is the only context in which the items are
printed. | *) |
| |
GEnumTagDecl of |
(* |
Declares an enumeration tag. Use as a forward declaration. This is
printed without the items.
| *) |
| |
GVarDecl of |
(* |
A variable declaration (not a definition) for a variable with object
type. There can be several declarations and at most one definition for
a given variable. If both forms appear then they must share the same
varinfo structure. Either has storage Extern or there must be a
definition in this file
| *) |
| |
GFunDecl of |
(* |
A variable declaration (not a definition) for a function, i.e. a
prototype. There can be several declarations and at most one definition
for a given function. If both forms appear then they must share the same
varinfo structure. A prototype shares the varinfo with the fundec of the
definition. Either has storage Extern or there must be a definition in
this file.
| *) |
| |
GVar of |
(* |
A variable definition. Can have an initializer. The initializer is
updateable so that you can change it without requiring to recreate the
list of globals. There can be at most one definition for a variable in an
entire program. Cannot have storage Extern or function type.
| *) |
| |
GFun of |
(* |
A function definition.
| *) |
| |
GAsm of |
(* |
Global asm statement. These ones can contain only a template
| *) |
| |
GPragma of |
(* |
Pragmas at top level. Use the same syntax as attributes
| *) |
| |
GText of |
(* |
Some text (printed verbatim) at top level. E.g., this way you can put
comments in the output.
| *) |
| |
GAnnot of |
(* |
a global annotation. Can be
| *) |
Cil_types.typ
. Among types
we differentiate the integral types (with different kinds denoting the sign
and precision), floating point types, enumeration types, array and pointer
types, and function types. Every type is associated with a list of
attributes, which are always kept in sorted order. Use Cil.addAttribute
and Cil.addAttributes
to construct list of attributes. If you want to
inspect a type, you should use Cil.unrollType
or Cil.unrollTypeDeep
to
see through the uses of named types.
CIL is configured at build-time with the sizes and alignments of the
underlying compiler (GCC or MSVC). CIL contains functions that can compute
the size of a type (in bits) Cil.bitsSizeOf
, the alignment of a type (in
bytes) Cil.alignOf_int
, and can convert an offset into a start and width
(both in bits) using the function Cil.bitsOffset
. At the moment these
functions do not take into account the packed
attributes and pragmas.
type
typ =
| |
TVoid of |
(* |
Void type. Also predefined as
Cil.voidType | *) |
| |
TInt of |
(* |
An integer type. The kind specifies the sign and width. Several useful
variants are predefined as
Cil.intType , Cil.uintType ,
Cil.longType , Cil.charType . | *) |
| |
TFloat of |
(* |
A floating-point type. The kind specifies the precision. You can also use
the predefined constant
Cil.doubleType . | *) |
| |
TPtr of |
(* |
Pointer type. Several useful variants are predefined as
Cil.charPtrType , Cil.charConstPtrType (pointer to a constant
character), Cil.voidPtrType , Cil.intPtrType | *) |
| |
TArray of |
(* |
Array type. It indicates the base type and the array length.
| *) |
| |
TFun of |
(* |
Function type. Indicates the type of the result, the name, type
and name attributes of the formal arguments (
None if no arguments
were specified, as in a function whose definition or prototype we
have not seen; Some [] means void). Use Cil.argsToList to
obtain a list of arguments. The boolean indicates if it is a
variable-argument function. If this is the type of a varinfo for
which we have a function declaration then the information for the
formals must match that in the function's sformals. Use
Cil.setFormals , or Cil.setFunctionType , or
Cil.makeFormalVar for this purpose. | *) |
| |
TNamed of |
(* |
The use of a named type. All uses of the same type name must share the
typeinfo. Each such type name must be preceded in the file by a
GType
global. This is printed as just the type name. The actual referred type
is not printed here and is carried only to simplify processing. To see
through a sequence of named type references, use Cil.unrollType . The
attributes are in addition to those given when the type name was
defined. | *) |
| |
TComp of |
(* |
A reference to a struct or a union type. All references to the
same struct or union must share the same compinfo among them and
with a
GCompTag global that precedes all uses (except maybe
those that are pointers to the composite type). The attributes
given are those pertaining to this use of the type and are in
addition to the attributes that were given at the definition of
the type and which are stored in the compinfo. | *) |
| |
TEnum of |
(* |
A reference to an enumeration type. All such references must
share the enuminfo among them and with a
GEnumTag global that
precedes all uses. The attributes refer to this use of the
enumeration and are in addition to the attributes of the
enumeration itself, which are stored inside the enuminfo | *) |
| |
TBuiltin_va_list of |
(* |
This is the same as the gcc's type with the same name
| *) |
type
ikind =
| |
IBool |
(* | _Bool | *) |
| |
IChar |
(* | char | *) |
| |
ISChar |
(* | signed char | *) |
| |
IUChar |
(* | unsigned char | *) |
| |
IInt |
(* | int | *) |
| |
IUInt |
(* | unsigned int | *) |
| |
IShort |
(* | short | *) |
| |
IUShort |
(* | unsigned short | *) |
| |
ILong |
(* | long | *) |
| |
IULong |
(* | unsigned long | *) |
| |
ILongLong |
(* | long long (or _int64 on Microsoft Visual C) | *) |
| |
IULongLong |
(* | unsigned long long (or unsigned _int64 on Microsoft
Visual C) | *) |
type
fkind =
| |
FFloat |
(* | float | *) |
| |
FDouble |
(* | double | *) |
| |
FLongDouble |
(* | long double | *) |
type
bitsSizeofTyp =
| |
Not_Computed |
|||
| |
Computed of |
|||
| |
Not_Computable of |
(* |
Explanation of the error
| *) |
type
bitsSizeofTypCache = {
|
mutable scache : |
type
attribute =
| |
Attr of |
(* |
An attribute has a name and some optional parameters. The name should not
start or end with underscore. When CIL parses attribute names it will
strip leading and ending underscores (to ensure that the multitude of GCC
attributes such as const, __const and __const__ all mean the same
thing.)
| *) |
| |
AttrAnnot of |
typeattributes =
attribute list
Cil.addAttribute
and Cil.addAttributes
to insert attributes in an
attribute list and maintain the sortedness.type
attrparam =
| |
AInt of |
(* |
An integer constant
| *) |
| |
AStr of |
(* |
A string constant
| *) |
| |
ACons of |
(* |
Constructed attributes. These are printed
foo(a1,a2,...,an) . The list
of parameters can be empty and in that case the parentheses are not
printed.
There are some Frama-C builtins that are used to account for OSX's peculiarities:
| *) |
| |
ASizeOf of |
(* |
A way to talk about types
| *) |
| |
ASizeOfE of |
|||
| |
AAlignOf of |
|||
| |
AAlignOfE of |
|||
| |
AUnOp of |
|||
| |
ABinOp of |
|||
| |
ADot of |
(* |
a.foo *
| *) |
| |
AStar of |
(* |
a
| *) |
| |
AAddrOf of |
(* |
& a *
| *) |
| |
AIndex of |
(* |
a1
a2 | *) |
| |
AQuestion of |
(* |
a1 ? a2 : a3 *
| *) |
Cil_types.compinfo
describes the definition of a structure or union
type. Each such Cil_types.compinfo
must be defined at the top-level using
the GCompTag
constructor and must be shared by all references to this type
(using either the TComp
type constructor or from the definition of the
fields.
If all you need is to scan the definition of each composite type once, you
can do that by scanning all top-level GCompTag
.
Constructing a Cil_types.compinfo
can be tricky since it must contain
fields that might refer to the host Cil_types.compinfo
and furthermore
the type of the field might need to refer to the Cil_types.compinfo
for
recursive types. Use the Cil.mkCompInfo
function to create a
Cil_types.compinfo
. You can easily fetch the Cil_types.fieldinfo
for a
given field in a structure with Cil.getCompField
.
type
compinfo = {
|
mutable cstruct : |
(* | true if struct, false if union | *) |
|
corig_name : |
(* |
Original name as found in C file. Will never be changed
| *) |
|
mutable cname : |
(* |
The name. Always non-empty. Use
Cil.compFullName to get the full name
of a comp (along with the struct or union) | *) |
|
mutable ckey : |
(* |
A unique integer. This is assigned by
Cil.mkCompInfo using a global
variable in the Cil module. Thus two identical structs in two different
files might have different keys. Use Cil.copyCompInfo to copy
structures so that a new key is assigned. | *) |
|
mutable cfields : |
(* |
Information about the fields. Notice that each fieldinfo has a pointer
back to the host compinfo. This means that you should not share
fieldinfo's between two compinfo's
| *) |
|
mutable cattr : |
(* |
The attributes that are defined at the same time as the composite
type. These attributes can be supplemented individually at each
reference to this
compinfo using the TComp type constructor. | *) |
|
mutable cdefined : |
(* |
This boolean flag can be used to distinguish between structures
that have not been defined and those that have been defined but have
no fields (such things are allowed in gcc).
| *) |
|
mutable creferenced : |
(* | true if used. Initially set to false . | *) |
Cil.mkCompInfo
to make
one and use Cil.copyCompInfo
to copy one (this ensures that a new key is
assigned and that the fields have the right pointers to parents.).Cil_types.fieldinfo
structure is used to describe a structure or
union field. Fields, just like variables, can have attributes associated
with the field itself or associated with the type of the field (stored along
with the type of the field).type
fieldinfo = {
|
mutable fcomp : |
(* |
The host structure that contains this field. There can be only one
compinfo that contains the field. | *) |
|
forig_name : |
(* |
original name as found in C file.
| *) |
|
mutable fname : |
(* |
The name of the field. Might be the value of
Cil.missingFieldName in
which case it must be a bitfield and is not printed and it does not
participate in initialization | *) |
|
mutable ftype : |
(* |
The type. If the field is a bitfield, a special attribute
FRAMA_C_BITFIELD_SIZE indicating the width of the bitfield is added. | *) |
|
mutable fbitfield : |
(* |
If a bitfield then ftype should be an integer type and the width of the
bitfield must be 0 or a positive integer smaller or equal to the width of
the integer type. A field of width 0 is used in C to control the alignment
of fields.
| *) |
|
mutable fattr : |
(* |
The attributes for this field (not for its type)
| *) |
|
mutable floc : |
(* |
The location where this field is defined
| *) |
|
mutable faddrof : |
(* |
Adapted from CIL
vaddrof field for variables. Only set for non-array
fields. Variable whose field address is taken is not marked anymore as
having its own address taken. True if the address of this field is
taken. CIL will set these flags when it parses C, but you should make
sure to set the flag whenever your transformation create AddrOf
expression. | *) |
|
mutable fsize_in_bits : |
(* |
Deprecated.only Jessie uses this
(Deprecated. Use Cil.bitsOffset instead.) Similar to fbitfield for
all types of fields. | *) |
|
mutable foffset_in_bits : |
(* |
Offset at which the field starts in the structure. Do not read directly,
but use
Cil.bitsOffset instead. | *) |
|
mutable fpadding_in_bits : |
(* |
Deprecated.only Jessie uses this
(Deprecated.) Store the size of the padding that follows the field, if any. | *) |
GEnumTag
for each of these.type
enuminfo = {
|
eorig_name : |
(* |
original name as found in C file.
| *) |
|
mutable ename : |
(* |
The name. Always non-empty.
| *) |
|
mutable eitems : |
(* |
Items. The list must be non-empty
| *) |
|
mutable eattr : |
(* |
The attributes that are defined at the same time as the enumeration
type. These attributes can be supplemented individually at each
reference to this
enuminfo using the TEnum type constructor. | *) |
|
mutable ereferenced : |
(* | true if used. Initially set to false . | *) |
|
mutable ekind : |
(* |
The integer kind used to represent this enum. MSVC
always assumes IInt but this is not the case
for gcc. See ISO C 6.7.2.2
| *) |
type
enumitem = {
|
eiorig_name : |
(* |
original name as found in C file.
| *) |
|
mutable einame : |
(* |
the name, always non-empty.
| *) |
|
mutable eival : |
(* |
value of the item. Must be a compile-time constant
| *) |
|
mutable eihost : |
(* |
the host enumeration in which the item is
declared.
| *) |
|
eiloc : |
type
typeinfo = {
|
torig_name : |
(* |
original name as found in C file.
| *) |
|
mutable tname : |
(* |
The name. Can be empty only in a
GType when introducing a composite or
enumeration tag. If empty cannot be referred to from the file | *) |
|
mutable ttype : |
(* |
The actual type. This includes the attributes that were present in the
typedef
| *) |
|
mutable treferenced : |
(* | true if used. Initially set to false . | *) |
Cil_types.varinfo
structure. A global Cil_types.varinfo
can be
introduced with the GVarDecl
or GVar
, GFunDecl
or GFun
globals.
A local varinfo can be introduced as part of a function definition
Cil_types.fundec
.
All references to a given global or local variable must refer to the same
copy of the varinfo
. Each varinfo
has a globally unique identifier that
can be used to index maps and hashtables (the name can also be used for this
purpose, except for locals from different functions). This identifier is
constructor using a global counter.
It is very important that you construct varinfo
structures using only one
of the following functions:
Cil.makeGlobalVar
: to make a global variableCil.makeTempVar
: to make a temporary local variable whose name
will be generated so that to avoid conflict with other locals.Cil.makeLocalVar
: like Cil.makeTempVar
but you can specify the
exact name to be used.Cil.copyVarinfo
: make a shallow copy of a varinfo assigning a new name
and a new unique identifiervarinfo
is also used in a function type to denote the list of
formals.type
varinfo = {
|
mutable vname : |
(* |
The name of the variable. Cannot be empty. It is primarily your
responsibility to ensure the uniqueness of a variable name. For local
variables
Cil.makeTempVar helps you ensure that the name is
unique. | *) |
|
vorig_name : |
(* |
the original name of the variable. Need not be unique.
| *) |
|
mutable vtype : |
(* |
The declared type of the variable.
| *) |
|
mutable vattr : |
(* |
A list of attributes associated with the variable.
| *) |
|
mutable vstorage : |
(* |
The storage-class
| *) |
|
mutable vglob : |
(* |
True if this is a global variable
| *) |
|
mutable vdefined : |
(* |
- For global variables, true iff the variable or function
is defined in the file.
| *) |
|
mutable vformal : |
(* |
True if the variable is a formal parameter of a function.
| *) |
|
mutable vinline : |
(* |
Whether this varinfo is for an inline function.
| *) |
|
mutable vdecl : |
(* |
Location of variable declaration.
| *) |
|
mutable vid : |
(* |
A unique integer identifier. This field will be set for you if you use
one of the
Cil.makeFormalVar , Cil.makeLocalVar ,
Cil.makeTempVar , Cil.makeGlobalVar , or Cil.copyVarinfo . | *) |
|
mutable vaddrof : |
(* | true if the address of this variable is taken. CIL will set these
flags when it parses C, but you should make sure to set the flag
whenever your transformation create AddrOf expression. | *) |
|
mutable vreferenced : |
(* | true if this variable is ever referenced. This is computed by
removeUnusedVars . It is safe to just initialize this to false . | *) |
|
vtemp : |
(* | true for temporary variables generated by CIL normalization. false
for all the other variables. | *) |
|
mutable vdescr : |
(* |
For most temporary variables, a description of what the var holds.
(e.g. for temporaries used for function call results, this string is a
representation of the function call.)
| *) |
|
mutable vdescrpure : |
(* |
Indicates whether the vdescr above is a pure expression or call. True
for all CIL expressions and Lvals, but false for e.g. function calls.
Printing a non-pure vdescr more than once may yield incorrect
results.
| *) |
|
mutable vghost : |
(* |
Indicates if the variable is declared in ghost code
| *) |
|
vsource : |
(* | true iff this variable appears in the source of the program, which is
the case of all the variables in the initial AST. Plugins may create
variables with vsource=false , for example to handle dynamic allocation.
Those variables do *not* have an associated GVar or GVarDecl . | *) |
|
mutable vlogic_var_assoc : |
(* |
Logic variable representing this variable in the logic world. Do not
access this field directly. Instead, call
Cil.cvar_to_lvar . | *) |
type
storage =
| |
NoStorage |
(* |
The default storage. Nothing is printed
| *) |
| |
Static |
|||
| |
Register |
|||
| |
Extern |
Cil_types.exp
. There are several
interesting aspects of CIL expressions:
Integer and floating point constants can carry their textual representation. This way the integer 15 can be printed as 0xF if that is how it occurred in the source.
CIL uses arbitrary precision integers
to represent the integer constants and also stores the
width of the integer type. Care must be taken to ensure that the constant is
representable with the given width. Use the functions Cil.kinteger
,
Cil.kinteger64
and Cil.integer
to construct constant expressions. CIL
predefines the constants Cil.zero
, Cil.one
and Cil.mone
(for -1).
Use the functions Cil.isConstant
and Cil.isInteger
to test if an
expression is a constant and a constant integer respectively.
CIL keeps the type of all unary and binary expressions. You can think of that type qualifying the operator. Furthermore there are different operators for arithmetic and comparisons on arithmetic types and on pointers.
Another unusual aspect of CIL is that the implicit conversion between an
expression of array type and one of pointer type is made explicit, using the
StartOf
expression constructor (which is not printed). If you apply the
AddrOf
constructor to an lvalue of type T
then you will be getting an
expression of type TPtr(T)
.
You can find the type of an expression with Cil.typeOf
.
You can perform constant folding on expressions using the function
Cil.constFold
.
type
exp = {
|
eid : |
(* |
unique identifier
| *) |
|
enode : |
(* |
the expression itself
| *) |
|
eloc : |
(* |
location of the expression.
| *) |
type
exp_node =
| |
Const of |
(* |
Constant
| *) |
| |
Lval of |
(* |
Lvalue
| *) |
| |
SizeOf of |
(* |
sizeof(<type>). Has
unsigned int type (ISO 6.5.3.4). This is not
turned into a constant because some transformations might want to change
types | *) |
| |
SizeOfE of |
(* |
sizeof(<expression>)
| *) |
| |
SizeOfStr of |
(* |
sizeof(string_literal). We separate this case out because this is the
only instance in which a string literal should not be treated as having
type pointer to character.
| *) |
| |
AlignOf of |
(* |
This corresponds to the GCC __alignof_. Has
unsigned int type | *) |
| |
AlignOfE of |
|||
| |
UnOp of |
(* |
Unary operation. Includes the type of the result.
| *) |
| |
BinOp of |
(* |
Binary operation. Includes the type of the result. The arithmetic
conversions are made explicit for the arguments.
Consult the Plugin Development Guide for additional details. | *) |
| |
CastE of |
(* |
Use
Cil.mkCast to make casts. | *) |
| |
AddrOf of |
(* |
Always use
Cil.mkAddrOf to construct one of these. Apply to an lvalue
of type T yields an expression of type TPtr(T) | *) |
| |
StartOf of |
(* |
Conversion from an array to a pointer to the beginning of the array.
Given an lval of type
TArray(T) produces an expression of type
TPtr(T) . In C this operation is implicit, the StartOf operator is not
printed. We have it in CIL because it makes the typing rules simpler. | *) |
| |
Info of |
(* |
Additional information on the underlying expression
| *) |
type
exp_info = {
|
exp_type : |
(* |
when used as placeholder for a term
| *) |
|
exp_name : |
type
constant =
| |
CInt64 of |
(* |
Integer constant. Give the ikind (see ISO9899 6.1.3.2) and the
textual representation. Textual representation is always set to Some s
when it comes from user code. This allows us to print a
constant as it was represented in the code, for example,
0xF instead of 15. It is usually None for constant generated by Cil
itself. Use
Cil.integer or Cil.kinteger to create these. | *) |
| |
CStr of |
(* |
String constant. The escape characters inside the string have been already
interpreted. This constant has pointer to character type! The only case
when you would like a string literal to have an array type is when it is
an argument to sizeof. In that case you should use SizeOfStr.
| *) |
| |
CWStr of |
(* |
Wide character string constant. Note that the local interpretation of such
a literal depends on
Cil.theMachine.wcharType and
Cil.theMachine.wcharKind . Such a constant has type pointer to
Cil.theMachine.wcharType . The escape characters in the string have not
been "interpreted" in the sense that L"A\xabcd" remains "A\xabcd" rather
than being represented as the wide character list with two elements: 65
and 43981. That "interpretation" depends on the underlying wide character
type. | *) |
| |
CChr of |
(* |
Character constant. This has type int, so use charConstToInt to read the
value in case sign-extension is needed.
| *) |
| |
CReal of |
(* |
Floating point constant. Give the fkind (see ISO 6.4.4.2) and also the
textual representation, if available.
| *) |
| |
CEnum of |
(* |
An enumeration constant. Use
Cillower.lowerEnumVisitor to replace these
with integer constants. | *) |
type
unop =
| |
Neg |
(* |
Unary minus
| *) |
| |
BNot |
(* |
Bitwise complement (~)
| *) |
| |
LNot |
(* |
Logical Not (!)
| *) |
type
binop =
| |
PlusA |
(* |
arithmetic +
| *) |
| |
PlusPI |
(* |
pointer + integer
| *) |
| |
IndexPI |
(* |
pointer + integer but only when it arises from an expression
e[i] when e is a pointer and
not an array. This is semantically
the same as PlusPI but CCured uses
this as a hint that the integer is
probably positive. | *) |
| |
MinusA |
(* |
arithmetic -
| *) |
| |
MinusPI |
(* |
pointer - integer
| *) |
| |
MinusPP |
(* |
pointer - pointer
| *) |
| |
Mult |
(* | *) |
|
| |
Div |
(* | *) |
|
| |
Mod |
(* | *) |
|
| |
Shiftlt |
(* |
shift left
| *) |
| |
Shiftrt |
(* |
shift right
| *) |
| |
Lt |
(* |
< (arithmetic comparison)
| *) |
| |
Gt |
(* |
> (arithmetic comparison)
| *) |
| |
Le |
(* |
<= (arithmetic comparison)
| *) |
| |
Ge |
(* |
>= (arithmetic comparison)
| *) |
| |
Eq |
(* |
== (arithmetic comparison)
| *) |
| |
Ne |
(* |
!= (arithmetic comparison)
| *) |
| |
BAnd |
(* |
bitwise and
| *) |
| |
BXor |
(* |
exclusive-or
| *) |
| |
BOr |
(* |
inclusive-or
| *) |
| |
LAnd |
(* |
logical and. Unlike other expressions this one does not always
evaluate both operands. If you want
to use these, you must set
Cil.useLogicalOperators . | *) |
| |
LOr |
(* |
logical or. Unlike other expressions this one does not always
evaluate both operands. If you
want to use these, you must set
Cil.useLogicalOperators . | *) |
a[0][1][2]might involve 1, 2 or 3 memory reads when used in an expression context, depending on the declared type of the variable
a
. If a
has type int [4][4][4]
then we have
one memory read from somewhere inside the area that stores the array a
. On
the other hand if a
has type int ***
then the expression really means *
( * ( * (a + 0) + 1) + 2)
, in which case it is clear that it involves three
separate memory operations.
An lvalue denotes the contents of a range of memory addresses. This range is
denoted as a host object along with an offset within the object. The host
object can be of two kinds: a local or global variable, or an object whose
address is in a pointer expression. We distinguish the two cases so that we
can tell quickly whether we are accessing some component of a variable
directly or we are accessing a memory location through a pointer. To make
it easy to tell what an lvalue means CIL represents lvalues as a host object
and an offset (see Cil_types.lval
). The host object (represented as
Cil_types.lhost
) can be a local or global variable or can be the object
pointed-to by a pointer expression. The offset (represented as
Cil_types.offset
) is a sequence of field or array index designators.
Both the typing rules and the meaning of an lvalue is very precisely specified in CIL.
The following are a few useful function for operating on lvalues:
Cil.mkMem
- makes an lvalue of Mem
kind. Use this to ensure
that certain equivalent forms of lvalues are canonized.
For example, *&x = x
.Cil.typeOfLval
- the type of an lvalueCil.typeOffset
- the type of an offset, given the type of the
host.Cil.addOffset
and Cil.addOffsetLval
- extend sequences
of offsets.Cil.removeOffset
and Cil.removeOffsetLval
- shrink sequences
of offsets.Mem(AddrOf(Mem a, aoff)), off = Mem a, aoff + off Mem(AddrOf(Var v, aoff)), off = Var v, aoff + off AddrOf (Mem a, NoOffset) = a
typelval =
lhost * offset
type
lhost =
| |
Var of |
(* |
The host is a variable.
| *) |
| |
Mem of |
(* |
The host is an object of type
T when the expression has pointer
TPtr(T) . | *) |
Cil_types.lval
.type
offset =
| |
NoOffset |
(* |
No offset. Can be applied to any lvalue and does not change either the
starting address or the type. This is used when the lval consists of just
a host or as a terminator in a list of other kinds of offsets.
| *) |
| |
Field of |
(* |
A field offset. Can be applied only to an lvalue that denotes a structure
or a union that contains the mentioned field. This advances the offset to
the beginning of the mentioned field and changes the type to the type of
the mentioned field.
| *) |
| |
Index of |
(* |
An array index offset. Can be applied only to an lvalue that denotes an
array. This advances the starting address of the lval to the beginning of
the mentioned array element and changes the denoted type to be the type of
the array element
| *) |
Cil_types.lval
. Each offset can be applied to
certain kinds of lvalues and its effect is that it advances the starting
address of the lvalue and changes the denoted type, essentially focussing
to some smaller lvalue that is contained in the original one.Cil_types.init
. You can create initializers with Cil.makeZeroInit
and
you can conveniently scan compound initializers them with
Cil.foldLeftCompound
.type
init =
| |
SingleInit of |
(* |
A single initializer
| *) |
| |
CompoundInit of |
(* |
Used only for initializers of structures, unions and arrays. The offsets
are all of the form
Field(f, NoOffset) or Index(i, NoOffset) and
specify the field or the index being initialized. For structures all fields
must have an initializer (except the unnamed bitfields), in the proper
order. This is necessary since the offsets are not printed. For arrays the
list must contain a prefix of the initializers; the rest are 0-initialized.
For unions there must be exactly one initializer. If the initializer is not
for the first field then a field designator is printed, so you better be on
GCC since MSVC does not understand this. You can scan an initializer list
with Cil.foldLeftCompound . | *) |
type
initinfo = {
|
mutable init : |
type
constructor_kind =
| |
Plain_func |
(* |
plain function call, whose result is used for initializing
the variable.
| *) |
| |
Constructor |
(* |
C++-like constructor: the function takes as first argument
the address of the variable to be initialized, and
returns
void . | *) |
type
local_init =
| |
AssignInit of |
(* |
normal initialization
| *) |
| |
ConsInit of |
(* | ConsInit(f,args,kind) indicates that the corresponding
local is initialized via a call to f , of kind kind
with the given args . | *) |
GFun
constructor at the
top level. All the information about the function is stored into a
Cil_types.fundec
. Some of the information (e.g. its name, type, storage,
attributes) is stored as a Cil_types.varinfo
that is a field of the
fundec
. To refer to the function from the expression language you must use
the varinfo
.
The function definition contains, in addition to the body, a list of all the
local variables and separately a list of the formals. Both kind of variables
can be referred to in the body of the function. The formals must also be
shared with the formals that appear in the function type. For that reason,
to manipulate formals you should use the provided functions
Cil.makeFormalVar
and Cil.setFormals
.
type
fundec = {
|
mutable svar : |
(* |
Holds the name and type as a variable, so we can refer to it easily
from the program. All references to this function either in a function
call or in a prototype must point to the same
varinfo . | *) |
|
mutable sformals : |
(* |
Formals. These must be in the same order and with the same information
as the formal information in the type of the function. Use
Cil.setFormals or Cil.setFunctionType to set these formals and
ensure that they are reflected in the function type. Do not make
copies of these because the body refers to them. | *) |
|
mutable slocals : |
(* |
Locals. Does NOT include the sformals. Do not make copies of these
because the body refers to them.
| *) |
|
mutable smaxid : |
(* |
Max local id. Starts at 0. Used for creating the names of new
temporary variables. Updated by
Cil.makeLocalVar and
Cil.makeTempVar . You can also use Cil.setMaxId to set it after
you have added the formals and locals. | *) |
|
mutable sbody : |
(* |
The function body.
| *) |
|
mutable smaxstmtid : |
(* |
max id of a (reachable) statement in this function, if we have
computed it. range = 0 ... (smaxstmtid-1). This is computed by
Cfg.computeCFGInfo . | *) |
|
mutable sallstmts : |
(* |
After you call
Cfg.computeCFGInfo this field is set to contain all
statements in the function. | *) |
|
mutable sspec : |
type
block = {
|
mutable battrs : |
(* |
Attributes for the block
| *) |
|
mutable bscoping : |
(* |
Whether the block is used to determine the scope of local variables.
| *) |
|
mutable blocals : |
(* |
variables that are local to the block. It is a subset of the slocals of
the enclosing function.
| *) |
|
mutable bstmts : |
(* |
The statements comprising the block.
| *) |
blocals
that have
their vdefined
field set to true
must appear as the target of a
Local_init
instruction directly in the bstmts
, with two exceptions: the
Local_init
instruction can be part of an UnspecifiedSequence
, or of
a block that has bscoping
set to false
. Such block _must not_
itself have local variables: it denotes a simple list of statements grouped
together (e.g. to stay in scope of an annotation extending to the
whole list).Cil_types.stmt
. Every statement has a
(possibly empty) list of labels. The Cil_types.stmtkind
field of a
statement indicates what kind of statement it is.
Use Cil.mkStmt
to make a statement and the fill-in the fields.
CIL also comes with support for control-flow graphs. The sid
field in
stmt
can be used to give unique numbers to statements, and the succs
and
preds
fields can be used to maintain a list of successors and predecessors
for every statement. The CFG information is not computed by default. Instead
you must explicitly use the functions Cfg.prepareCFG
and
Cfg.computeCFGInfo
to do it.
type
stmt = {
|
mutable labels : |
(* |
Whether the statement starts with some labels, case statements or
default statements.
| *) |
|
mutable skind : |
(* |
The kind of statement
| *) |
|
mutable sid : |
(* |
A number (>= 0) that is unique in a function. Filled in only after the
CFG is computed.
| *) |
|
mutable succs : |
(* |
The successor statements. They can always be computed from the skind and
the context in which this statement appears. Filled in only after the CFG
is computed.
| *) |
|
mutable preds : |
(* |
The inverse of the succs function.
| *) |
|
mutable ghost : |
type
label =
| |
Label of |
(* |
A real label. If the bool is "true", the label is from the input source
program. If the bool is "false", the label was created by CIL or some
other transformation
| *) |
| |
Case of |
(* |
A case statement. This expression is lowered into a constant if
Cil.lowerConstants is set to true . | *) |
| |
Default of |
(* |
A default statement
| *) |
type
stmtkind =
| |
Instr of |
(* |
An instruction that does not contain control flow. Control implicitly
falls through.
Consult the Plugin Development Guide for additional details. | *) |
| |
Return of |
(* |
The return statement. This is a leaf in the CFG.
Consult the Plugin Development Guide for additional details. | *) |
| |
Goto of |
(* |
A goto statement. Appears from actual goto's in the code or from goto's
that have been inserted during elaboration. The reference points to the
statement that is the target of the Goto. This means that you have to
update the reference whenever you replace the target statement. The
target statement MUST have at least a label.
Consult the Plugin Development Guide for additional details. | *) |
| |
Break of |
(* |
A break to the end of the nearest enclosing Loop or Switch.
Consult the Plugin Development Guide for additional details. | *) |
| |
Continue of |
(* |
A continue to the start of the nearest enclosing
Loop .Consult the Plugin Development Guide for additional details. | *) |
| |
If of |
(* |
A conditional. Two successors, the "then" and the "else" branches (in
this order).
Both branches fall-through to the successor of the If statement.
Consult the Plugin Development Guide for additional details. | *) |
| |
Switch of |
(* |
A switch statement.
exp is the index of the switch. block is
the body of the switch. stmt list contains the set of
statements whose labels are cases of the switch (i.e. for each
case, the corresponding statement is in stmt list , a statement
cannot appear more than once in the list, and statements in
stmt list can have several labels corresponding to several
cases.Consult the Plugin Development Guide for additional details. | *) |
| |
Loop of |
(* |
A
while(1) loop. The termination test is implemented in the body of a
loop using a Break statement. If Cfg.prepareCFG has been called, the
first stmt option will point to the stmt containing the continue label
for this loop and the second will point to the stmt containing the break
label for this loop.Consult the Plugin Development Guide for additional details. | *) |
| |
Block of |
(* |
Just a block of statements. Use it as a way to keep some block attributes
local.
Consult the Plugin Development Guide for additional details. | *) |
| |
UnspecifiedSequence of |
(* |
statements whose order of execution is not specified by
ISO/C. This is important for the order of side effects
during evaluation of expressions. Each statement comes
together with three list of lval, in this order.
In case you do not care about this feature just handle it
like a block (see | *) |
| |
Throw of |
(* |
Throws an exception, C++ style.
We keep the type of the expression, to match
it against the appropriate catch clause. A Throw node has
no successor, even if it is in try-catch block that will catch
the exception: we keep normal and exceptional control-flow
completely separate, as in Jo and Chang, ICSSA 2004.
| *) |
| |
TryCatch of |
|||
| |
TryFinally of |
(* |
On MSVC we support structured exception handling. This is what you might
expect. Control can get into the finally block either from the end of the
body block, or if an exception is thrown.
Consult the Plugin Development Guide for additional details. | *) |
| |
TryExcept of |
(* |
On MSVC we support structured exception handling. The try/except
statement is a bit tricky:
__try { blk } __except (e) { handler }
The argument to __except must be an expression. However, we keep a
list of instructions AND an expression in case you need to make
function calls. We'll print those as a comma expression. The control
can get to the __except expression only if an exception is thrown.
After that, depending on the value of the expression the control
goes to the handler, propagates the exception, or retries the
exception. The location corresponds to the try keyword. | *) |
type
catch_binder =
| |
Catch_exn of |
(* |
catch exception of given type(s).
If the list is empty, only exceptions with the same type as the
varinfo can be caught. If the list is non-empty, only exceptions
matching one of the type of a varinfo in the list are caught.
The associated block contains the operations necessary to transform
the matched varinfo into the principal one.
Semantics is by value (i.e. the varinfo is bound to a copy of the
caught object).
This clause is a declaration point for the varinfo(s)
mentioned in it. More precisely, for
| *) |
| |
Catch_all |
(* |
default catch clause: all exceptions are caught.
| *) |
type
instr =
| |
Set of |
(* |
An assignment. A cast is present if the exp has different type from
lval
| *) |
| |
Call of |
(* |
optional: result is an lval. A cast might be necessary if the declared
result type of the function is not the same as that of the destination.
Actual arguments must have a type equivalent (i.e.
Cil.need_cast must
return false ) to the one of the formals of the function.
If the type of the result variable is not the same as the declared type of
the function result then an implicit cast exists. | *) |
| |
Local_init of |
(* |
initialization of a local variable. The corresponding varinfo must
belong to the
blocals list of the innermost enclosing block that does
not have attribute Cil.block_no_scope_attr . Such blocks are purely
here for grouping statements and do not play a role for scoping
variables. See Cil_types.block definition for more informationSince Phosphorus-20170501-beta1 | *) |
| |
Asm of |
(* |
An inline assembly instruction. The arguments are
(1) a list of attributes (only const and volatile can appear here and only
for GCC)
(2) templates (CR-separated)
(3) GCC extended asm information if any
(4) location information
| *) |
| |
Skip of |
|||
| |
Code_annot of |
type
extended_asm = {
|
asm_outputs : |
(* |
outputs must be lvals with optional names and constraints. I would
like these to be actually variables, but I run into some trouble with
ASMs in the Linux sources
| *) |
|
asm_inputs : |
(* |
inputs with optional names and constraints
| *) |
|
asm_clobbers : |
(* |
register clobbers
| *) |
|
asm_gotos : |
(* |
list of statements this asm section may jump to. Destination
must have a label.
| *) |
typelocation =
Lexing.position * Lexing.position
type
logic_constant =
| |
Integer of |
(* |
Integer constant with a textual representation.
| *) |
| |
LStr of |
(* |
String constant.
| *) |
| |
LWStr of |
(* |
Wide character string constant.
| *) |
| |
LChr of |
(* |
Character constant.
| *) |
| |
LReal of |
|||
| |
LEnum of |
(* |
An enumeration constant.
| *) |
type
logic_real = {
|
r_literal : |
(* |
Initial string representation
s . | *) |
|
r_nearest : |
(* |
Nearest approximation of
s in double precision. | *) |
|
r_upper : |
(* |
Smallest double
u such that s <= u . | *) |
|
r_lower : |
(* |
Greatest double
l such that l <= s . | *) |
type
logic_type =
| |
Ctype of |
(* |
a C type
| *) |
| |
Ltype of |
(* |
an user-defined logic type with its parameters
| *) |
| |
Lvar of |
(* |
a type variable.
| *) |
| |
Linteger |
(* |
mathematical integers, i.e. Z
| *) |
| |
Lreal |
(* |
mathematical reals, i.e. R
| *) |
| |
Larrow of |
(* |
(n-ary) function type
| *) |
type
identified_term = {
|
it_id : |
(* |
the identifier.
| *) |
|
it_content : |
(* |
the term
| *) |
Logic_const.new_location
to generate a new id.type
logic_label =
| |
StmtLabel of |
(* |
label of a C statement.
| *) |
| |
FormalLabel of |
(* |
label of global annotation.
| *) |
| |
BuiltinLabel of |
type
logic_builtin_label =
| |
Here |
| |
Old |
| |
Pre |
| |
Post |
| |
LoopEntry |
| |
LoopCurrent |
| |
Init |
type
term = {
|
term_node : |
(* |
kind of term.
| *) |
|
term_loc : |
(* |
position in the source file.
| *) |
|
term_type : |
(* |
type of the term.
| *) |
|
term_name : |
(* |
names of the term if any. A name can be an arbitrary string, where
'"' and '\'' are escaped by a \, and which does not end with a \.
Hence, "name" and 'name' should be recognized as a unique label by most
tools.
| *) |
type
term_node =
| |
TConst of |
(* |
a constant.
| *) |
| |
TLval of |
(* |
an L-value
| *) |
| |
TSizeOf of |
(* |
size of a given C type.
| *) |
| |
TSizeOfE of |
(* |
size of the type of an expression.
| *) |
| |
TSizeOfStr of |
(* |
size of a string constant.
| *) |
| |
TAlignOf of |
(* |
alignment of a type.
| *) |
| |
TAlignOfE of |
(* |
alignment of the type of an expression.
| *) |
| |
TUnOp of |
(* |
unary operator.
| *) |
| |
TBinOp of |
(* |
binary operators.
| *) |
| |
TCastE of |
(* |
cast to a C type.
| *) |
| |
TAddrOf of |
(* |
address of a term.
| *) |
| |
TStartOf of |
(* |
beginning of an array.
| *) |
| |
Tapp of |
(* |
application of a logic function.
| *) |
| |
Tlambda of |
(* |
lambda abstraction.
| *) |
| |
TDataCons of |
(* |
constructor of logic sum-type.
| *) |
| |
Tif of |
(* |
conditional operator
| *) |
| |
Tat of |
(* |
term refers to a particular program point.
| *) |
| |
Tbase_addr of |
(* |
base address of a pointer.
| *) |
| |
Toffset of |
(* |
offset from the base address of a pointer.
| *) |
| |
Tblock_length of |
(* |
length of the block pointed to by the term.
| *) |
| |
Tnull |
(* |
the null pointer.
| *) |
| |
TLogic_coerce of |
(* |
implicit conversion from a C type to a logic type.
The logic type must not be a Ctype. In particular, used to denote
lifting to Linteger and Lreal.
| *) |
| |
TCoerce of |
(* |
coercion to a given C type.
| *) |
| |
TCoerceE of |
(* |
coercion to the type of a given term.
| *) |
| |
TUpdate of |
(* |
functional update of a field.
| *) |
| |
Ttypeof of |
(* |
type tag for a term.
| *) |
| |
Ttype of |
(* |
type tag for a C type.
| *) |
| |
Tempty_set |
(* |
the empty set.
| *) |
| |
Tunion of |
(* |
union of terms.
| *) |
| |
Tinter of |
(* |
intersection of terms.
| *) |
| |
Tcomprehension of |
(* |
set defined in comprehension ()
| *) |
| |
Trange of |
(* |
range of integers.
| *) |
| |
Tlet of |
(* |
local binding
| *) |
typeterm_lval =
term_lhost * term_offset
type
term_lhost =
| |
TVar of |
(* |
a variable.
| *) |
| |
TResult of |
(* |
value returned by a C function.
Only used in post-conditions or assigns
| *) |
| |
TMem of |
(* |
memory access.
| *) |
type
model_info = {
|
mi_name : |
(* |
name
| *) |
|
mi_field_type : |
(* |
type of the field
| *) |
|
mi_base_type : |
(* |
type to which the field is associated.
| *) |
|
mi_decl : |
(* |
where the field has been declared.
| *) |
|
mutable mi_attr : |
(* |
attributes tied to the field.
Since Phosphorus-20170501-beta1 | *) |
type
term_offset =
| |
TNoOffset |
(* |
no further offset.
| *) |
| |
TField of |
(* |
access to the field of a compound type.
| *) |
| |
TModel of |
(* |
access to a model field.
| *) |
| |
TIndex of |
(* |
index. Note that a range is denoted by
TIndex(Trange(i1,i2),ofs) | *) |
type
logic_info = {
|
mutable l_var_info : |
(* |
we use only fields lv_name and lv_id of l_var_info
we should factorize lv_type and l_type+l_profile below
| *) |
|
mutable l_labels : |
(* |
label arguments of the function.
| *) |
|
mutable l_tparams : |
(* |
type parameters
| *) |
|
mutable l_type : |
(* |
return type. None for predicates
| *) |
|
mutable l_profile : |
(* |
type of the arguments.
| *) |
|
mutable l_body : |
(* |
body of the function.
| *) |
type
builtin_logic_info = {
|
mutable bl_name : |
|
mutable bl_labels : |
|
mutable bl_params : |
|
mutable bl_type : |
|
mutable bl_profile : |
type
logic_body =
| |
LBnone |
(* |
no definition and no reads clause
| *) |
| |
LBreads of |
(* |
read accesses performed by a function.
| *) |
| |
LBterm of |
(* |
direct definition of a function.
| *) |
| |
LBpred of |
(* |
direct definition of a predicate.
| *) |
| |
LBinductive of |
(* |
inductive definition
| *) |
type
logic_type_info = {
|
lt_name : |
|||
|
lt_params : |
(* |
type parameters
| *) |
|
mutable lt_def : |
(* |
definition of the type. None for abstract types.
| *) |
|
mutable lt_attr : |
(* |
attributes associated to the logic type.
Since Phosphorus-20170501-beta1 | *) |
type
logic_type_def =
| |
LTsum of |
(* |
sum type with its constructors.
| *) |
| |
LTsyn of |
(* |
Synonym of another type.
| *) |
type
logic_var_kind =
| |
LVGlobal |
(* |
global logic function or predicate.
| *) |
| |
LVC |
(* |
Logic counterpart of a C variable.
| *) |
| |
LVFormal |
(* |
formal parameter of a logic function / predicate
or \lambda abstraction
| *) |
| |
LVQuant |
(* |
Bound by a quantifier (\exists or \forall)
| *) |
| |
LVLocal |
(* |
local \let
| *) |
type
logic_var = {
|
mutable lv_name : |
(* |
name of the variable.
| *) |
|
mutable lv_id : |
(* |
unique identifier
| *) |
|
mutable lv_type : |
(* |
type of the variable.
| *) |
|
mutable lv_kind : |
(* |
kind of the variable
| *) |
|
mutable lv_origin : |
(* |
when the logic variable stems from a C variable, set to the original C
variable.
| *) |
|
mutable lv_attr : |
(* |
attributes tied to the logic variable
Since Phosphorus-20170501-beta1 | *) |
type
logic_ctor_info = {
|
ctor_name : |
(* |
name of the constructor.
| *) |
|
ctor_type : |
(* |
type to which the constructor belongs.
| *) |
|
ctor_params : |
(* |
types of the parameters of the constructor.
| *) |
typequantifiers =
logic_var list
type
relation =
| |
Rlt |
|||
| |
Rgt |
|||
| |
Rle |
|||
| |
Rge |
|||
| |
Req |
|||
| |
Rneq |
(* |
Consult the Plugin Development Guide for additional details.
| *) |
type
predicate_node =
| |
Pfalse |
(* |
always-false predicate.
| *) |
| |
Ptrue |
(* |
always-true predicate.
| *) |
| |
Papp of |
(* |
application of a predicate.
| *) |
| |
Pseparated of |
|||
| |
Prel of |
(* |
comparison of two terms.
| *) |
| |
Pand of |
(* |
conjunction
| *) |
| |
Por of |
(* |
disjunction.
| *) |
| |
Pxor of |
(* |
logical xor.
| *) |
| |
Pimplies of |
(* |
implication.
| *) |
| |
Piff of |
(* |
equivalence.
| *) |
| |
Pnot of |
(* |
negation.
| *) |
| |
Pif of |
(* |
conditional
| *) |
| |
Plet of |
(* |
definition of a local variable
| *) |
| |
Pforall of |
(* |
universal quantification.
| *) |
| |
Pexists of |
(* |
existential quantification.
| *) |
| |
Pat of |
(* |
predicate refers to a particular program point.
| *) |
| |
Pvalid_read of |
(* |
the given locations are valid for reading.
| *) |
| |
Pvalid of |
(* |
the given locations are valid.
| *) |
| |
Pvalid_function of |
(* |
the pointed function has a type compatible with the one of pointer.
| *) |
| |
Pinitialized of |
(* |
the given locations are initialized.
| *) |
| |
Pdangling of |
(* |
the given locations contain dangling
addresses.
| *) |
| |
Pallocable of |
(* |
the given locations can be allocated.
| *) |
| |
Pfreeable of |
(* |
the given locations can be free.
| *) |
| |
Pfresh of |
(* |
\fresh(pointer, n)
A memory block of n bytes is newly allocated to the pointer.
| *) |
| |
Psubtype of |
(* |
First term is a type tag that is a subtype of the second.
| *) |
type
identified_predicate = {
|
ip_id : |
(* |
identifier
| *) |
|
ip_content : |
(* |
the predicate itself
| *) |
Logic_const.new_predicate
to
create fresh predicatestype
predicate = {
|
pred_name : |
(* |
list of given names
| *) |
|
pred_loc : |
(* |
position in the source code.
| *) |
|
pred_content : |
(* |
content
| *) |
typevariant =
term * string option
type
allocation =
| |
FreeAlloc of |
(* |
tsets. Empty list means \nothing.
| *) |
| |
FreeAllocAny |
(* |
Nothing specified. Semantics depends on where it
is written.
| *) |
type
deps =
| |
From of |
(* |
tsets. Empty list means \nothing.
| *) |
| |
FromAny |
(* |
Nothing specified. Any location can be involved.
| *) |
typefrom =
identified_term * deps
type
assigns =
| |
WritesAny |
(* |
Nothing specified. Anything can be written.
| *) |
| |
Writes of |
(* |
list of locations that can be written. Empty list means \nothing.
| *) |
type
spec = {
|
mutable spec_behavior : |
(* |
behaviors
| *) |
|
mutable spec_variant : |
(* |
variant for recursive functions.
| *) |
|
mutable spec_terminates : |
(* |
termination condition.
| *) |
|
mutable spec_complete_behaviors : |
(* |
list of complete behaviors.
It is possible to have more than one set of complete behaviors
| *) |
|
mutable spec_disjoint_behaviors : |
(* |
list of disjoint behaviors.
It is possible to have more than one set of disjoint behaviors
| *) |
Logic_ptree.spec
.typeacsl_extension =
string * acsl_extension_kind
Logic_typing.register_behavior_extension
for parsing and type-checkingCil_printer.register_behavior_extension
for pretty-printing an
extended clauseCil.register_behavior_extension
for visiting an extended clausetype
acsl_extension_kind =
| |
Ext_id of |
(* |
id used internally by the extension itself.
| *) |
| |
Ext_terms of |
|||
| |
Ext_preds of |
(* |
a list of predicates, the most common case of for extensions
| *) |
type
behavior = {
|
mutable b_name : |
(* |
name of the behavior.
| *) |
|
mutable b_requires : |
(* |
require clauses.
| *) |
|
mutable b_assumes : |
(* |
assume clauses.
| *) |
|
mutable b_post_cond : |
(* |
post-condition.
| *) |
|
mutable b_assigns : |
(* |
assignments.
| *) |
|
mutable b_allocation : |
(* |
frees, allocates.
| *) |
|
mutable b_extended : |
(* | *) |
Logic_ptree.behavior
.b_ensures
is replaced by b_post_cond
.
Old b_ensures
represent the Normal
case of b_post_cond
.type
termination_kind =
| |
Normal |
| |
Exits |
| |
Breaks |
| |
Continues |
| |
Returns |
type
loop_pragma =
| |
Unroll_specs of |
| |
Widen_hints of |
| |
Widen_variables of |
type
slice_pragma =
| |
SPexpr of |
| |
SPctrl |
| |
SPstmt |
type
impact_pragma =
| |
IPexpr of |
| |
IPstmt |
type
pragma =
| |
Loop_pragma of |
| |
Slice_pragma of |
| |
Impact_pragma of |
type
code_annotation_node =
| |
AAssert of |
(* |
assertion to be checked. The list of strings is the list of
behaviors to which this assertion applies.
| *) |
| |
AStmtSpec of |
(* |
statement contract
(potentially restricted to some enclosing behaviors).
| *) |
| |
AInvariant of |
(* |
loop/code invariant. The list of strings is the list of behaviors to which
this invariant applies. The boolean flag is true for normal loop
invariants and false for invariant-as-assertions.
| *) |
| |
AVariant of |
(* |
loop variant. Note that there can be at most one variant associated to a
given statement
| *) |
| |
AAssigns of |
(* |
loop assigns. (see
b_assigns in the behaviors for other assigns). At
most one clause associated to a given (statement, behavior) couple. | *) |
| |
AAllocation of |
(* |
loop allocation clause. (see
b_allocation in the behaviors for other
allocation clauses).
At most one clause associated to a given (statement, behavior) couple.Since Oxygen-20120901 when [b_allocation] has been added. | *) |
| |
APragma of |
(* |
pragma.
| *) |
| |
AExtended of |
(* |
extension in a loop annotation.
Since Silicon-20161101 | *) |
Logic_ptree.code_annot
.typefunspec =
spec
type
code_annotation = {
|
annot_id : |
(* |
identifier.
| *) |
|
annot_content : |
(* |
content of the annotation.
| *) |
Logic_const.new_code_annotation
to create new code annotations with
a fresh id.typefunbehavior =
behavior
type
global_annotation =
| |
Dfun_or_pred of |
|||
| |
Dvolatile of |
(* |
associated terms, reading function, writing function
| *) |
| |
Daxiomatic of |
|||
| |
Dtype of |
(* |
declaration of a logic type.
| *) |
| |
Dlemma of |
(* |
definition of a lemma. The boolean flag is
true if the property should
be taken as an axiom and false if it must be proved. | *) |
| |
Dinvariant of |
(* |
global invariant. The predicate does not have any argument.
| *) |
| |
Dtype_annot of |
(* |
type invariant. The predicate has exactly one argument.
| *) |
| |
Dmodel_annot of |
(* |
Model field for a type t, seen as a logic function with one
argument of type t
| *) |
| |
Dcustom_annot of |
type
custom_tree =
| |
CustomDummy |
type
kinstr =
| |
Kstmt of |
| |
Kglobal |
type
cil_function =
| |
Definition of |
(* |
defined function
| *) |
| |
Declaration of |
(* |
Declaration(spec,f,args,loc) represents a leaf function
f with
specification spec and arguments args , at location loc . As
with the TFun constructor of Cil_types.typ , the arg list is
optional, to distinguish void f() (None ) from
void f(void) (Some [] ). | *) |
type
kernel_function = {
|
mutable fundec : |
|
mutable spec : |
fundec
can be used directly. Use Annotations.funspec
,
Annotations.add_*
and Annotations.remove_*
to query or modify field
spec
.type
localisation =
| |
VGlobal |
| |
VLocal of |
| |
VFormal of |
type
mach = {
|
sizeof_short : |
|
sizeof_int : |
|
sizeof_long : |
|
sizeof_longlong : |
|
sizeof_ptr : |
|
sizeof_float : |
|
sizeof_double : |
|
sizeof_longdouble : |
|
sizeof_void : |
|
sizeof_fun : |
|
size_t : |
|
wchar_t : |
|
ptrdiff_t : |
|
alignof_short : |
|
alignof_int : |
|
alignof_long : |
|
alignof_longlong : |
|
alignof_ptr : |
|
alignof_float : |
|
alignof_double : |
|
alignof_longdouble : |
|
alignof_str : |
|
alignof_fun : |
|
char_is_unsigned : |
|
underscore_name : |
|
const_string_literals : |
|
little_endian : |
|
alignof_aligned : |
|
has__builtin_va_list : |
|
__thread_is_keyword : |
|
compiler : |
|
cpp_arch_flags : |
|
version : |