diff options
Diffstat (limited to 'cil/src/cil.mli')
| -rw-r--r-- | cil/src/cil.mli | 2455 |
1 files changed, 0 insertions, 2455 deletions
diff --git a/cil/src/cil.mli b/cil/src/cil.mli deleted file mode 100644 index 31c4e65..0000000 --- a/cil/src/cil.mli +++ /dev/null @@ -1,2455 +0,0 @@ -(* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) - -(* - * - * Copyright (c) 2001-2002, - * George C. Necula <necula@cs.berkeley.edu> - * Scott McPeak <smcpeak@cs.berkeley.edu> - * Wes Weimer <weimer@cs.berkeley.edu> - * All rights reserved. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * 1. Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * - * 2. Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in the - * documentation and/or other materials provided with the distribution. - * - * 3. The names of the contributors may not be used to endorse or promote - * products derived from this software without specific prior written - * permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS - * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED - * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A - * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER - * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, - * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, - * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR - * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF - * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING - * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS - * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - * - *) - -(* - * CIL: An intermediate language for analyzing C programs. - * - * George Necula - * - *) - -(** CIL API Documentation. An html version of this document can be found at - * http://manju.cs.berkeley.edu/cil. *) - -(** Call this function to perform some initialization. Call if after you have - * set {!Cil.msvcMode}. *) -val initCIL: unit -> unit - - -(** This are the CIL version numbers. A CIL version is a number of the form - * M.m.r (major, minor and release) *) -val cilVersion: string -val cilVersionMajor: int -val cilVersionMinor: int -val cilVersionRevision: int - -(** This module defines the abstract syntax of CIL. It also provides utility - * functions for traversing the CIL data structures, and pretty-printing - * them. The parser for both the GCC and MSVC front-ends can be invoked as - * [Frontc.parse: string -> unit ->] {!Cil.file}. This function must be given - * the name of a preprocessed C file and will return the top-level data - * structure that describes a whole source file. By default the parsing and - * elaboration into CIL is done as for GCC source. If you want to use MSVC - * source you must set the {!Cil.msvcMode} to [true] and must also invoke the - * function [Frontc.setMSVCMode: unit -> unit]. *) - - -(** {b The Abstract Syntax of CIL} *) - - -(** The top-level representation of a CIL source file (and the result of the - * parsing and elaboration). Its main contents is the list of global - * declarations and definitions. You can iterate over the globals in a - * {!Cil.file} using the following iterators: {!Cil.mapGlobals}, - * {!Cil.iterGlobals} and {!Cil.foldGlobals}. You can also use the - * {!Cil.dummyFile} when you need a {!Cil.file} as a placeholder. For each - * global item CIL stores the source location where it appears (using the - * type {!Cil.location}) *) - -type file = - { mutable fileName: string; (** The complete file name *) - mutable globals: global list; (** List of globals as they will appear - in the printed file *) - mutable globinit: fundec option; - (** 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: bool; - (** 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. This will not happen if your file does not contain a - * function called "main" *) - } -(** Top-level representation of a C source file *) - -and comment = location * string - -(** {b Globals}. The main type for representing global declarations and - * definitions. A list of these form a CIL file. The order of globals in the - * file is generally important. *) - -(** A global declaration or definition *) -and global = - | GType of typeinfo * location - (** 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 compinfo * location - (** 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 compinfo * location - (** Declares a struct/union tag. Use as a forward declaration. This is - * printed without the fields. *) - - | GEnumTag of enuminfo * location - (** 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 enuminfo * location - (** Declares an enumeration tag. Use as a forward declaration. This is - * printed without the items. *) - - | GVarDecl of varinfo * location - (** A variable declaration (not a definition). If the variable has a - function type then this is a prototype. 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. 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 varinfo * initinfo * location - (** 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 fundec * location - (** A function definition. *) - - | GAsm of string * location (** Global asm statement. These ones - can contain only a template *) - | GPragma of attribute * location (** Pragmas at top level. Use the same - syntax as attributes *) - | GText of string (** Some text (printed verbatim) at - top level. E.g., this way you can - put comments in the output. *) - -(** {b Types}. A C type is represented in CIL using the type {!Cil.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. *) - -and typ = - TVoid of attributes (** Void type. Also predefined as {!Cil.voidType} *) - | TInt of ikind * attributes - (** 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 fkind * attributes - (** A floating-point type. The kind specifies the precision. You can - * also use the predefined constant {!Cil.doubleType}. *) - - | TPtr of typ * attributes - (** Pointer type. Several useful variants are predefined as - * {!Cil.charPtrType}, {!Cil.charConstPtrType} (pointer to a - * constant character), {!Cil.voidPtrType}, - * {!Cil.intPtrType} *) - - | TArray of typ * exp option * attributes - (** Array type. It indicates the base type and the array length. *) - - | TFun of typ * (string * typ * attributes) list option * bool * attributes - (** 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 typeinfo * attributes - (* The use of a named type. 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} or - * {!Cil.unrollTypeDeep}. The attributes are in addition to those - * given when the type name was defined. *) - - | TComp of compinfo * attributes -(** The most delicate issue for C types is that recursion that is possible by - * using structures and pointers. To address this issue we have a more - * complex representation for structured types (struct and union). Each such - * type is represented using the {!Cil.compinfo} type. For each composite - * type the {!Cil.compinfo} structure must be declared at top level using - * [GCompTag] and all references to it must share the same copy of the - * structure. 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 {!Cil.compinfo}. *) - - | TEnum of enuminfo * attributes - (** 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 attributes - (** This is the same as the gcc's type with the same name *) - -(** - There are a number of functions for querying the kind of a type. These are - {!Cil.isIntegralType}, - {!Cil.isArithmeticType}, - {!Cil.isPointerType}, - {!Cil.isFunctionType}, - {!Cil.isArrayType}. - - There are two easy ways to scan a type. First, you can use the -{!Cil.existsType} to return a boolean answer about a type. This function -is controlled by a user-provided function that is queried for each type that is -used to construct the current type. The function can specify whether to -terminate the scan with a boolean result or to continue the scan for the -nested types. - - The other method for scanning types is provided by the visitor interface (see - {!Cil.cilVisitor}). - - If you want to compare types (or to use them as hash-values) then you should -use instead type signatures (represented as {!Cil.typsig}). These -contain the same information as types but canonicalized such that simple Ocaml -structural equality will tell whether two types are equal. Use -{!Cil.typeSig} to compute the signature of a type. If you want to ignore -certain type attributes then use {!Cil.typeSigWithAttrs}. - -*) - - -(** Various kinds of integers *) -and ikind = - 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) *) - -(** Various kinds of floating-point numbers*) -and fkind = - FFloat (** [float] *) - | FDouble (** [double] *) - | FLongDouble (** [long double] *) - - -(** {b Attributes.} *) - -and attribute = Attr of string * attrparam list -(** 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.) *) - -(** Attributes are lists sorted by the attribute name. Use the functions - * {!Cil.addAttribute} and {!Cil.addAttributes} to insert attributes in an - * attribute list and maintain the sortedness. *) -and attributes = attribute list - -(** The type of parameters of attributes *) -and attrparam = - | AInt of int (** An integer constant *) - | AStr of string (** A string constant *) - | ACons of string * attrparam list (** 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. *) - | ASizeOf of typ (** A way to talk about types *) - | ASizeOfE of attrparam - | ASizeOfS of typsig (** Replacement for ASizeOf in type - signatures. Only used for - attributes inside typsigs.*) - | AAlignOf of typ - | AAlignOfE of attrparam - | AAlignOfS of typsig - | AUnOp of unop * attrparam - | ABinOp of binop * attrparam * attrparam - | ADot of attrparam * string (** a.foo **) - -(** {b Structures.} The {!Cil.compinfo} describes the definition of a - * structure or union type. Each such {!Cil.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.compinfo} can be tricky since it must contain fields - * that might refer to the host {!Cil.compinfo} and furthermore the type of - * the field might need to refer to the {!Cil.compinfo} for recursive types. - * Use the {!Cil.mkCompInfo} function to create a {!Cil.compinfo}. You can - * easily fetch the {!Cil.fieldinfo} for a given field in a structure with - * {!Cil.getCompField}. *) - -(** The definition of a structure or union type. Use {!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.). *) -and compinfo = { - mutable cstruct: bool; - (** True if struct, False if union *) - mutable cname: string; - (** The name. Always non-empty. Use {!Cil.compFullName} to get the full - * name of a comp (along with the struct or union) *) - mutable ckey: int; - (** 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: fieldinfo list; - (** 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: attributes; - (** 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: bool; - (** 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: bool; - (** True if used. Initially set to false. *) - } - -(** {b Structure fields.} The {!Cil.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). *) - -(** Information about a struct/union field *) -and fieldinfo = { - mutable fcomp: compinfo; - (** The host structure that contains this field. There can be only one - * [compinfo] that contains the field. *) - mutable fname: string; - (** 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: typ; - (** The type *) - mutable fbitfield: int option; - (** 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: attributes; - (** The attributes for this field (not for its type) *) - mutable floc: location; - (** The location where this field is defined *) -} - - - -(** {b Enumerations.} Information about an enumeration. This is shared by all - * references to an enumeration. Make sure you have a [GEnumTag] for each of - * of these. *) - -(** Information about an enumeration *) -and enuminfo = { - mutable ename: string; - (** The name. Always non-empty. *) - mutable eitems: (string * exp * location) list; - (** Items with names and values. This list should be non-empty. The item - * values must be compile-time constants. *) - mutable eattr: attributes; - (** 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: bool; - (** True if used. Initially set to false*) -} - -(** {b Enumerations.} Information about an enumeration. This is shared by all - * references to an enumeration. Make sure you have a [GEnumTag] for each of - * of these. *) - -(** Information about a defined type *) -and typeinfo = { - mutable tname: string; - (** 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: typ; - (** The actual type. This includes the attributes that were present in - * the typedef *) - mutable treferenced: bool; - (** True if used. Initially set to false*) -} - -(** {b Variables.} - Each local or global variable is represented by a unique {!Cil.varinfo} -structure. A global {!Cil.varinfo} can be introduced with the [GVarDecl] or -[GVar] or [GFun] globals. A local varinfo can be introduced as part of a -function definition {!Cil.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 variable -- {!Cil.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 identifier - - A [varinfo] is also used in a function type to denote the list of formals. - -*) - -(** Information about a variable. *) -and varinfo = { - mutable vname: string; - (** 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. - *) - - mutable vtype: typ; - (** The declared type of the variable. *) - - mutable vattr: attributes; - (** A list of attributes associated with the variable.*) - mutable vstorage: storage; - (** The storage-class *) - - mutable vglob: bool; - (** True if this is a global variable*) - - mutable vinline: bool; - (** Whether this varinfo is for an inline function. *) - - mutable vdecl: location; - (** Location of variable declaration. *) - - mutable vid: int; - (** 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: bool; - (** 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: bool; - (** True if this variable is ever referenced. This is computed by - * [removeUnusedVars]. It is safe to just initialize this to False *) -} - -(** Storage-class information *) -and storage = - NoStorage (** The default storage. Nothing is printed *) - | Static - | Register - | Extern - - -(** {b Expressions.} The CIL expression language contains only the side-effect free expressions of -C. They are represented as the type {!Cil.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 64 bits 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}. -*) - -(** Expressions (Side-effect free)*) -and exp = - Const of constant (** Constant *) - | Lval of lval (** Lvalue *) - | SizeOf of typ - (** 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 exp - (** sizeof(<expression>) *) - - | SizeOfStr of string - (** 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 typ - (** This corresponds to the GCC __alignof_. Has [unsigned int] type *) - | AlignOfE of exp - - - | UnOp of unop * exp * typ - (** Unary operation. Includes the type of the result. *) - - | BinOp of binop * exp * exp * typ - (** Binary operation. Includes the type of the result. The arithmetic - * conversions are made explicit for the arguments. *) - - | CastE of typ * exp - (** Use {!Cil.mkCast} to make casts. *) - - | AddrOf of lval - (** 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 lval - (** 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. *) - -(** {b Constants.} *) - -(** Literal constants *) -and constant = - | CInt64 of int64 * ikind * string option - (** Integer constant. Give the ikind (see ISO9899 6.1.3.2) and the - * textual representation, if available. (This allows us to print a - * constant as, for example, 0xF instead of 15.) Use {!Cil.integer} or - * {!Cil.kinteger} to create these. Watch out for integers that cannot be - * represented on 64 bits. OCAML does not give Overflow exceptions. *) - | CStr of string - (* 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 int64 list - (* Wide character string constant. Note that the local interpretation - * of such a literal depends on {!Cil.wcharType} and {!Cil.wcharKind}. - * Such a constant has type pointer to {!Cil.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 char - (** Character constant. This has type int, so use charConstToInt - * to read the value in case sign-extension is needed. *) - | CReal of float * fkind * string option - (** Floating point constant. Give the fkind (see ISO 6.4.4.2) and also - * the textual representation, if available. *) - | CEnum of exp * string * enuminfo - (** An enumeration constant with the given value, name, from the given - * enuminfo. This is used only if {!Cil.lowerConstants} is true - * (default). Use {!Cil.constFoldVisitor} to replace these with integer - * constants. *) - -(** Unary operators *) -and unop = - Neg (** Unary minus *) - | BNot (** Bitwise complement (~) *) - | LNot (** Logical Not (!) *) - -(** Binary operations *) -and 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}. *) - -(** {b Lvalues.} Lvalues are the sublanguage of expressions that can appear at the left of an assignment or as operand to the address-of operator. -In C the syntax for lvalues is not always a good indication of the meaning -of the lvalue. For example the C value -{v -a[0][1][2] - v} - 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.lval}). The host object (represented as -{!Cil.lhost}) can be a local or global variable or can be the object -pointed-to by a pointer expression. The offset (represented as -{!Cil.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 lvalue -- {!Cil.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. - -The following equivalences hold {v -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 - v} - -*) -(** An lvalue *) -and lval = - lhost * offset - -(** The host part of an {!Cil.lval}. *) -and lhost = - | Var of varinfo - (** The host is a variable. *) - - | Mem of exp - (** The host is an object of type [T] when the expression has pointer - * [TPtr(T)]. *) - - -(** The offset part of an {!Cil.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 focusing to some - * smaller lvalue that is contained in the original one. *) -and 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 fieldinfo * offset - (** 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 exp * offset - (** 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 *) - - -(** {b Initializers.} -A special kind of expressions are those that can appear as initializers for -global variables (initialization of local variables is turned into -assignments). The initializers are represented as type {!Cil.init}. You -can create initializers with {!Cil.makeZeroInit} and you can conveniently -scan compound initializers them with {!Cil.foldLeftCompound} or with {!Cil.foldLeftCompoundAll}. -*) -(** Initializers for global variables. *) -and init = - | SingleInit of exp (** A single initializer *) - | CompoundInit of typ * (offset * init) list - (** 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 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. - * For arrays, however, we allow you to give only a prefix of the - * initializers. You can scan an initializer list with - * {!Cil.foldLeftCompound} or with {!Cil.foldLeftCompoundAll}. *) - - -(** We want to be able to update an initializer in a global variable, so we - * define it as a mutable field *) -and initinfo = { - mutable init : init option; - } - -(** {b Function definitions.} -A function definition is always introduced with a [GFun] constructor at the -top level. All the information about the function is stored into a -{!Cil.fundec}. Some of the information (e.g. its name, type, -storage, attributes) is stored as a {!Cil.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} and {!Cil.makeFormalVar}. -*) -(** Function definitions. *) -and fundec = - { mutable svar: varinfo; - (** 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: varinfo list; - (** 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} or {!Cil.makeFormalVar} - * 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: varinfo list; - (** Locals. Does NOT include the sformals. Do not make copies of - * these because the body refers to them. *) - mutable smaxid: int; (** 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: block; (** The function body. *) - mutable smaxstmtid: int option; (** max id of a (reachable) statement - * in this function, if we have - * computed it. range = 0 ... - * (smaxstmtid-1). This is computed by - * {!Cil.computeCFGInfo}. *) - mutable sallstmts: stmt list; (** After you call {!Cil.computeCFGInfo} - * this field is set to contain all - * statements in the function *) - } - - -(** A block is a sequence of statements with the control falling through from - one element to the next *) -and block = - { mutable battrs: attributes; (** Attributes for the block *) - mutable bstmts: stmt list; (** The statements comprising the block*) - } - - -(** {b Statements}. -CIL statements are the structural elements that make the CFG. They are -represented using the type {!Cil.stmt}. Every -statement has a (possibly empty) list of labels. The -{!Cil.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 -{!Cil.prepareCFG} and {!Cil.computeCFGInfo} to do it. - -*) -(** Statements. *) -and stmt = { - mutable labels: label list; - (** Whether the statement starts with some labels, case statements or - * default statements. *) - - mutable skind: stmtkind; - (** The kind of statement *) - - mutable sid: int; - (** A number (>= 0) that is unique in a function. Filled in only after - * the CFG is computed. *) - mutable succs: stmt list; - (** 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: stmt list; - (** The inverse of the succs function. *) - } - -(** Labels *) -and label = - Label of string * location * bool - (** 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 exp * location (** A case statement. This expression - * is lowered into a constant if - * {!Cil.lowerConstants} is set to - * true. *) - | Default of location (** A default statement *) - - - -(** The various kinds of control-flow statements statements *) -and stmtkind = - | Instr of instr list - (** A group of instructions that do not contain control flow. Control - * implicitly falls through. *) - - | Return of exp option * location - (** The return statement. This is a leaf in the CFG. *) - - | Goto of stmt ref * location - (** 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. *) - - | Break of location - (** A break to the end of the nearest enclosing loop or Switch *) - - | Continue of location - (** A continue to the start of the nearest enclosing loop *) - | If of exp * block * block * location - (** A conditional. Two successors, the "then" and the "else" branches. - * Both branches fall-through to the successor of the If statement. *) - - | Switch of exp * block * (stmt list) * location - (** A switch statement. The statements that implement the cases can be - * reached through the provided list. For each such target you can find - * among its labels what cases it implements. The statements that - * implement the cases are somewhere within the provided [block]. *) - -(* - | Loop of block * location * (stmt option) * (stmt option) - (** A [while(1)] loop. The termination test is implemented in the body of - * a loop using a [Break] statement. If 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. *) -*) - - | While of exp * block * location - (** A [while] loop. *) - - | DoWhile of exp * block * location - (** A [do...while] loop. *) - - | For of block * exp * block * block * location - (** A [for] loop. *) - - | Block of block - (** Just a block of statements. Use it as a way to keep some block - * attributes local *) - - (** 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. *) - | TryFinally of block * block * location - - (** 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 !!! - *) - | TryExcept of block * (instr list * exp) * block * location - - -(** {b Instructions}. - An instruction {!Cil.instr} is a statement that has no local -(intraprocedural) control flow. It can be either an assignment, -function call, or an inline assembly instruction. *) - -(** Instructions. *) -and instr = - Set of lval * exp * location - (** An assignment. The type of the expression is guaranteed to be the same - * with that of the lvalue *) - | Call of lval option * exp * exp list * location - (** A function call with the (optional) result placed in an lval. It is - * possible that the returned type of the function is not identical to - * that of the lvalue. In that case a cast is printed. The type of the - * actual arguments are identical to those of the declared formals. The - * number of arguments is the same as that of the declared formals, except - * for vararg functions. This construct is also used to encode a call to - * "__builtin_va_arg". In this case the second argument (which should be a - * type T) is encoded SizeOf(T) *) - - | Asm of attributes * (* Really only const and volatile can appear - * here *) - string list * (* templates (CR-separated) *) - (string * lval) list * (* outputs must be lvals with - * constraints. I would like these - * to be actually variables, but I - * run into some trouble with ASMs - * in the Linux sources *) - (string * exp) list * (* inputs with constraints *) - string list * (* register clobbers *) - location - (** There are for storing inline assembly. They follow the GCC - * specification: -{v - asm [volatile] ("...template..." "..template.." - : "c1" (o1), "c2" (o2), ..., "cN" (oN) - : "d1" (i1), "d2" (i2), ..., "dM" (iM) - : "r1", "r2", ..., "nL" ); - v} - -where the parts are - - - [volatile] (optional): when present, the assembler instruction - cannot be removed, moved, or otherwise optimized - - template: a sequence of strings, with %0, %1, %2, etc. in the string to - refer to the input and output expressions. I think they're numbered - consecutively, but the docs don't specify. Each string is printed on - a separate line. This is the only part that is present for MSVC inline - assembly. - - "ci" (oi): pairs of constraint-string and output-lval; the - constraint specifies that the register used must have some - property, like being a floating-point register; the constraint - string for outputs also has "=" to indicate it is written, or - "+" to indicate it is both read and written; 'oi' is the - name of a C lvalue (probably a variable name) to be used as - the output destination - - "dj" (ij): pairs of constraint and input expression; the constraint - is similar to the "ci"s. the 'ij' is an arbitrary C expression - to be loaded into the corresponding register - - "rk": registers to be regarded as "clobbered" by the instruction; - "memory" may be specified for arbitrary memory effects - -an example (from gcc manual): -{v - asm volatile ("movc3 %0,%1,%2" - : /* no outputs */ - : "g" (from), "g" (to), "g" (count) - : "r0", "r1", "r2", "r3", "r4", "r5"); - v} -*) - -(** Describes a location in a source file. *) -and location = { - line: int; (** The line number. -1 means "do not know" *) - file: string; (** The name of the source file*) - byte: int; (** The byte position in the source file *) -} - - -(** Type signatures. Two types are identical iff they have identical - * signatures. These contain the same information as types but canonicalized. - * For example, two function types that are identical except for the name of - * the formal arguments are given the same signature. Also, [TNamed] - * constructors are unrolled. *) -and typsig = - TSArray of typsig * int64 option * attribute list - | TSPtr of typsig * attribute list - | TSComp of bool * string * attribute list - | TSFun of typsig * typsig list * bool * attribute list - | TSEnum of string * attribute list - | TSBase of typ - - - -(** {b Lowering Options} *) - -val lowerConstants: bool ref - (** Do lower constants (default true) *) - -val insertImplicitCasts: bool ref - (** Do insert implicit casts (default true) *) - -(** To be able to add/remove features easily, each feature should be package - * as an interface with the following interface. These features should be *) -type featureDescr = { - fd_enabled: bool ref; - (** The enable flag. Set to default value *) - - fd_name: string; - (** This is used to construct an option "--doxxx" and "--dontxxx" that - * enable and disable the feature *) - - fd_description: string; - (* A longer name that can be used to document the new options *) - - fd_extraopt: (string * Arg.spec * string) list; - (** Additional command line options *) - - fd_doit: (file -> unit); - (** This performs the transformation *) - - fd_post_check: bool; - (* Whether to perform a CIL consistency checking after this stage, if - * checking is enabled (--check is passed to cilly). Set this to true if - * your feature makes any changes for the program. *) -} - -(** Comparison function for locations. - ** Compares first by filename, then line, then byte *) -val compareLoc: location -> location -> int - -(** {b Values for manipulating globals} *) - -(** Make an empty function *) -val emptyFunction: string -> fundec - -(** Update the formals of a [fundec] and make sure that the function type - has the same information. Will copy the name as well into the type. *) -val setFormals: fundec -> varinfo list -> unit - -(** Set the types of arguments and results as given by the function type - * passed as the second argument. Will not copy the names from the function - * type to the formals *) -val setFunctionType: fundec -> typ -> unit - - -(** Set the type of the function and make formal arguments for them *) -val setFunctionTypeMakeFormals: fundec -> typ -> unit - -(** Update the smaxid after you have populated with locals and formals - * (unless you constructed those using {!Cil.makeLocalVar} or - * {!Cil.makeTempVar}. *) -val setMaxId: fundec -> unit - -(** A dummy function declaration handy when you need one as a placeholder. It - * contains inside a dummy varinfo. *) -val dummyFunDec: fundec - -(** A dummy file *) -val dummyFile: file - -(** Write a {!Cil.file} in binary form to the filesystem. The file can be - * read back in later using {!Cil.loadBinaryFile}, possibly saving parsing - * time. The second argument is the name of the file that should be - * created. *) -val saveBinaryFile : file -> string -> unit - -(** Write a {!Cil.file} in binary form to the filesystem. The file can be - * read back in later using {!Cil.loadBinaryFile}, possibly saving parsing - * time. Does not close the channel. *) -val saveBinaryFileChannel : file -> out_channel -> unit - -(** Read a {!Cil.file} in binary form from the filesystem. The first - * argument is the name of a file previously created by - * {!Cil.saveBinaryFile}. *) -val loadBinaryFile : string -> file - -(** Get the global initializer and create one if it does not already exist. - * When it creates a global initializer it attempts to place a call to it in - * the main function named by the optional argument (default "main") *) -val getGlobInit: ?main_name:string -> file -> fundec - -(** Iterate over all globals, including the global initializer *) -val iterGlobals: file -> (global -> unit) -> unit - -(** Fold over all globals, including the global initializer *) -val foldGlobals: file -> ('a -> global -> 'a) -> 'a -> 'a - -(** Map over all globals, including the global initializer and change things - in place *) -val mapGlobals: file -> (global -> global) -> unit - -val new_sid : unit -> int - -(** Prepare a function for CFG information computation by - * {!Cil.computeCFGInfo}. This function converts all [Break], [Switch], - * [Default] and [Continue] {!Cil.stmtkind}s and {!Cil.label}s into [If]s - * and [Goto]s, giving the function body a very CFG-like character. This - * function modifies its argument in place. *) -val prepareCFG: fundec -> unit - -(** Compute the CFG information for all statements in a fundec and return a - * list of the statements. The input fundec cannot have [Break], [Switch], - * [Default], or [Continue] {!Cil.stmtkind}s or {!Cil.label}s. Use - * {!Cil.prepareCFG} to transform them away. The second argument should - * be [true] if you wish a global statement number, [false] if you wish a - * local (per-function) statement numbering. The list of statements is set - * in the sallstmts field of a fundec. - * - * NOTE: unless you want the simpler control-flow graph provided by - * prepareCFG, or you need the function's smaxstmtid and sallstmt fields - * filled in, we recommend you use {!Cfg.computeFileCFG} instead of this - * function to compute control-flow information. - * {!Cfg.computeFileCFG} is newer and will handle switch, break, and - * continue correctly.*) -val computeCFGInfo: fundec -> bool -> unit - - -(** Create a deep copy of a function. There should be no sharing between the - * copy and the original function *) -val copyFunction: fundec -> string -> fundec - - -(** CIL keeps the types at the beginning of the file and the variables at the - * end of the file. This function will take a global and add it to the - * corresponding stack. Its operation is actually more complicated because if - * the global declares a type that contains references to variables (e.g. in - * sizeof in an array length) then it will also add declarations for the - * variables to the types stack *) -val pushGlobal: global -> types: global list ref - -> variables: global list ref -> unit - -(** An empty statement. Used in pretty printing *) -val invalidStmt: stmt - -(** A list of the GCC built-in functions. Maps the name to the result and - * argument types, and whether it is vararg *) -val gccBuiltins: (string, typ * typ list * bool) Hashtbl.t - - -(** A list of the MSVC built-in functions. Maps the name to the result and - * argument types, and whether it is vararg *) -val msvcBuiltins: (string, typ * typ list * bool) Hashtbl.t - -(** {b Values for manipulating initializers} *) - - -(** Make a initializer for zero-ing a data type *) -val makeZeroInit: typ -> init - - -(** Fold over the list of initializers in a Compound. [doinit] is called on - * every present initializer, even if it is of compound type. In the case of - * arrays there might be missing zero-initializers at the end of the list. - * These are not scanned. This is much like [List.fold_left] except we also - * pass the type of the initializer *) -val foldLeftCompound: - doinit: (offset -> init -> typ -> 'a -> 'a) -> - ct: typ -> - initl: (offset * init) list -> - acc: 'a -> 'a - - -(** Fold over the list of initializers in a Compound, like - * {!Cil.foldLeftCompound} but in the case of an array it scans even missing - * zero initializers at the end of the array *) -val foldLeftCompoundAll: - doinit: (offset -> init -> typ -> 'a -> 'a) -> - ct: typ -> - initl: (offset * init) list -> - acc: 'a -> 'a - - - -(** {b Values for manipulating types} *) - -(** void *) -val voidType: typ - -(* is the given type "void"? *) -val isVoidType: typ -> bool - -(* is the given type "void *"? *) -val isVoidPtrType: typ -> bool - -(** int *) -val intType: typ - -(** unsigned int *) -val uintType: typ - -(** long *) -val longType: typ - -(** unsigned long *) -val ulongType: typ - -(** char *) -val charType: typ - -(** char * *) -val charPtrType: typ - -(** wchar_t (depends on architecture) and is set when you call - * {!Cil.initCIL}. *) -val wcharKind: ikind ref -val wcharType: typ ref - -(** char const * *) -val charConstPtrType: typ - -(** void * *) -val voidPtrType: typ - -(** int * *) -val intPtrType: typ - -(** unsigned int * *) -val uintPtrType: typ - -(** double *) -val doubleType: typ - -(* An unsigned integer type that fits pointers. Depends on {!Cil.msvcMode} - * and is set when you call {!Cil.initCIL}. *) -val upointType: typ ref - -(* An unsigned integer type that is the type of sizeof. Depends on - * {!Cil.msvcMode} and is set when you call {!Cil.initCIL}. *) -val typeOfSizeOf: typ ref - -(** Returns true if and only if the given integer type is signed. *) -val isSigned: ikind -> bool - - -(** Creates a a (potentially recursive) composite type. The arguments are: - * (1) a boolean indicating whether it is a struct or a union, (2) the name - * (always non-empty), (3) a function that when given a representation of the - * structure type constructs the type of the fields recursive type (the first - * argument is only useful when some fields need to refer to the type of the - * structure itself), and (4) a list of attributes to be associated with the - * composite type. The resulting compinfo has the field "cdefined" only if - * the list of fields is non-empty. *) -val mkCompInfo: bool -> (* whether it is a struct or a union *) - string -> (* name of the composite type; cannot be empty *) - (compinfo -> - (string * typ * int option * attributes * location) list) -> - (* a function that when given a forward - representation of the structure type constructs the type of - the fields. The function can ignore this argument if not - constructing a recursive type. *) - attributes -> compinfo - -(** Makes a shallow copy of a {!Cil.compinfo} changing the name and the key.*) -val copyCompInfo: compinfo -> string -> compinfo - -(** This is a constant used as the name of an unnamed bitfield. These fields - do not participate in initialization and their name is not printed. *) -val missingFieldName: string - -(** Get the full name of a comp *) -val compFullName: compinfo -> string - -(** Returns true if this is a complete type. - This means that sizeof(t) makes sense. - Incomplete types are not yet defined - structures and empty arrays. *) -val isCompleteType: typ -> bool - -(** Unroll a type until it exposes a non - * [TNamed]. Will collect all attributes appearing in [TNamed]!!! *) -val unrollType: typ -> typ - -(** Unroll all the TNamed in a type (even under type constructors such as - * [TPtr], [TFun] or [TArray]. Does not unroll the types of fields in [TComp] - * types. Will collect all attributes *) -val unrollTypeDeep: typ -> typ - -(** Separate out the storage-modifier name attributes *) -val separateStorageModifiers: attribute list -> attribute list * attribute list - -(** True if the argument is an integral type (i.e. integer or enum) *) -val isIntegralType: typ -> bool - -(** True if the argument is an arithmetic type (i.e. integer, enum or - floating point *) -val isArithmeticType: typ -> bool - -(**True if the argument is a pointer type *) -val isPointerType: typ -> bool - -(** True if the argument is a function type *) -val isFunctionType: typ -> bool - -(** Obtain the argument list ([] if None) *) -val argsToList: (string * typ * attributes) list option - -> (string * typ * attributes) list - -(** True if the argument is an array type *) -val isArrayType: typ -> bool - -(** Raised when {!Cil.lenOfArray} fails either because the length is [None] - * or because it is a non-constant expression *) -exception LenOfArray - -(** Call to compute the array length as present in the array type, to an - * integer. Raises {!Cil.LenOfArray} if not able to compute the length, such - * as when there is no length or the length is not a constant. *) -val lenOfArray: exp option -> int - -(** Return a named fieldinfo in compinfo, or raise Not_found *) -val getCompField: compinfo -> string -> fieldinfo - - -(** A datatype to be used in conjunction with [existsType] *) -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 *) - -(** Scans a type by applying the function on all elements. - When the function returns ExistsTrue, the scan stops with - true. When the function returns ExistsFalse then the current branch is not - scanned anymore. Care is taken to - apply the function only once on each composite type, thus avoiding - circularity. When the function returns ExistsMaybe then the types that - construct the current type are scanned (e.g. the base type for TPtr and - TArray, the type of fields for a TComp, etc). *) -val existsType: (typ -> existsAction) -> typ -> bool - - -(** Given a function type split it into return type, - * arguments, is_vararg and attributes. An error is raised if the type is not - * a function type *) -val splitFunctionType: - typ -> typ * (string * typ * attributes) list option * bool * attributes -(** Same as {!Cil.splitFunctionType} but takes a varinfo. Prints a nicer - * error message if the varinfo is not for a function *) -val splitFunctionTypeVI: - varinfo -> typ * (string * typ * attributes) list option * bool * attributes - - -(** {b Type signatures} *) - -(** Type signatures. Two types are identical iff they have identical - * signatures. These contain the same information as types but canonicalized. - * For example, two function types that are identical except for the name of - * the formal arguments are given the same signature. Also, [TNamed] - * constructors are unrolled. You shoud use [Util.equals] to compare type - * signatures because they might still contain circular structures (through - * attributes, and sizeof) *) - -(** Print a type signature *) -val d_typsig: unit -> typsig -> Pretty.doc - -(** Compute a type signature *) -val typeSig: typ -> typsig - -(** Like {!Cil.typeSig} but customize the incorporation of attributes. - Use ~ignoreSign:true to convert all signed integer types to unsigned, - so that signed and unsigned will compare the same. *) -val typeSigWithAttrs: ?ignoreSign:bool -> (attributes -> attributes) -> typ -> typsig - -(** Replace the attributes of a signature (only at top level) *) -val setTypeSigAttrs: attributes -> typsig -> typsig - -(** Get the top-level attributes of a signature *) -val typeSigAttrs: typsig -> attributes - -(*********************************************************) -(** LVALUES *) - -(** Make a varinfo. Use this (rarely) to make a raw varinfo. Use other - * functions to make locals ({!Cil.makeLocalVar} or {!Cil.makeFormalVar} or - * {!Cil.makeTempVar}) and globals ({!Cil.makeGlobalVar}). Note that this - * function will assign a new identifier. The first argument specifies - * whether the varinfo is for a global. *) -val makeVarinfo: bool -> string -> typ -> varinfo - -(** Make a formal variable for a function. Insert it in both the sformals - and the type of the function. You can optionally specify where to insert - this one. If where = "^" then it is inserted first. If where = "$" then - it is inserted last. Otherwise where must be the name of a formal after - which to insert this. By default it is inserted at the end. *) -val makeFormalVar: fundec -> ?where:string -> string -> typ -> varinfo - -(** Make a local variable and add it to a function's slocals (only if insert = - true, which is the default). Make sure you know what you are doing if you - set insert=false. *) -val makeLocalVar: fundec -> ?insert:bool -> string -> typ -> varinfo - -(** Make a temporary variable and add it to a function's slocals. The name of - the temporary variable will be generated based on the given name hint so - that to avoid conflicts with other locals. *) -val makeTempVar: fundec -> ?name: string -> typ -> varinfo - - -(** Make a global variable. Your responsibility to make sure that the name - is unique *) -val makeGlobalVar: string -> typ -> varinfo - -(** Make a shallow copy of a [varinfo] and assign a new identifier *) -val copyVarinfo: varinfo -> string -> varinfo - - -(** Generate a new variable ID. This will be different than any variable ID - * that is generated by {!Cil.makeLocalVar} and friends *) -val newVID: unit -> int - -(** Add an offset at the end of an lvalue. Make sure the type of the lvalue - * and the offset are compatible. *) -val addOffsetLval: offset -> lval -> lval - -(** [addOffset o1 o2] adds [o1] to the end of [o2]. *) -val addOffset: offset -> offset -> offset - -(** Remove ONE offset from the end of an lvalue. Returns the lvalue with the - * trimmed offset and the final offset. If the final offset is [NoOffset] - * then the original [lval] did not have an offset. *) -val removeOffsetLval: lval -> lval * offset - -(** Remove ONE offset from the end of an offset sequence. Returns the - * trimmed offset and the final offset. If the final offset is [NoOffset] - * then the original [lval] did not have an offset. *) -val removeOffset: offset -> offset * offset - -(** Compute the type of an lvalue *) -val typeOfLval: lval -> typ - -(** Compute the type of an offset from a base type *) -val typeOffset: typ -> offset -> typ - - -(*******************************************************) -(** {b Values for manipulating expressions} *) - - -(* Construct integer constants *) - -(** 0 *) -val zero: exp - -(** 1 *) -val one: exp - -(** -1 *) -val mone: exp - - -(** Construct an integer of a given kind, using OCaml's int64 type. If needed - * it will truncate the integer to be within the representable range for the - * given kind. *) -val kinteger64: ikind -> int64 -> exp - -(** Construct an integer of a given kind. Converts the integer to int64 and - * then uses kinteger64. This might truncate the value if you use a kind - * that cannot represent the given integer. This can only happen for one of - * the Char or Short kinds *) -val kinteger: ikind -> int -> exp - -(** Construct an integer of kind IInt. You can use this always since the - OCaml integers are 31 bits and are guaranteed to fit in an IInt *) -val integer: int -> exp - - -(** True if the given expression is a (possibly cast'ed) - character or an integer constant *) -val isInteger: exp -> int64 option - -(** True if the expression is a compile-time constant *) -val isConstant: exp -> bool - -(** True if the given expression is a (possibly cast'ed) integer or character - constant with value zero *) -val isZero: exp -> bool - -(** Given the character c in a (CChr c), sign-extend it to 32 bits. - (This is the official way of interpreting character constants, according to - ISO C 6.4.4.4.10, which says that character constants are chars cast to ints) - Returns CInt64(sign-extened c, IInt, None) *) -val charConstToInt: char -> constant - -(** Do constant folding on an expression. If the first argument is true then - will also compute compiler-dependent expressions such as sizeof *) -val constFold: bool -> exp -> exp - -(** Do constant folding on a binary operation. The bulk of the work done by - [constFold] is done here. If the first argument is true then - will also compute compiler-dependent expressions such as sizeof *) -val constFoldBinOp: bool -> binop -> exp -> exp -> typ -> exp - -(** Increment an expression. Can be arithmetic or pointer type *) -val increm: exp -> int -> exp - - -(** Makes an lvalue out of a given variable *) -val var: varinfo -> lval - -(** Make an AddrOf. Given an lvalue of type T will give back an expression of - type ptr(T). It optimizes somewhat expressions like "& v" and "& v[0]" *) -val mkAddrOf: lval -> exp - - -(** Like mkAddrOf except if the type of lval is an array then it uses - StartOf. This is the right operation for getting a pointer to the start - of the storage denoted by lval. *) -val mkAddrOrStartOf: lval -> exp - -(** Make a Mem, while optimizing AddrOf. The type of the addr must be - TPtr(t) and the type of the resulting lval is t. Note that in CIL the - implicit conversion between an array and the pointer to the first - element does not apply. You must do the conversion yourself using - StartOf *) -val mkMem: addr:exp -> off:offset -> lval - -(** Make an expression that is a string constant (of pointer type) *) -val mkString: string -> exp - -(** Construct a cast when having the old type of the expression. If the new - * type is the same as the old type, then no cast is added. *) -val mkCastT: e:exp -> oldt:typ -> newt:typ -> exp - -(** Like {!Cil.mkCastT} but uses typeOf to get [oldt] *) -val mkCast: e:exp -> newt:typ -> exp - -(** Removes casts from this expression, but ignores casts within - other expression constructs. So we delete the (A) and (B) casts from - "(A)(B)(x + (C)y)", but leave the (C) cast. *) -val stripCasts: exp -> exp - -(** Compute the type of an expression *) -val typeOf: exp -> typ - -(** Convert a string representing a C integer literal to an expression. - * Handles the prefixes 0x and 0 and the suffixes L, U, UL, LL, ULL *) -val parseInt: string -> exp - - -(**********************************************) -(** {b Values for manipulating statements} *) - -(** Construct a statement, given its kind. Initialize the [sid] field to -1, - and [labels], [succs] and [preds] to the empty list *) -val mkStmt: stmtkind -> stmt - -(** Construct a block with no attributes, given a list of statements *) -val mkBlock: stmt list -> block - -(** Construct a statement consisting of just one instruction *) -val mkStmtOneInstr: instr -> stmt - -(** Try to compress statements so as to get maximal basic blocks *) -(* use this instead of List.@ because you get fewer basic blocks *) -val compactStmts: stmt list -> stmt list - -(** Returns an empty statement (of kind [Instr]) *) -val mkEmptyStmt: unit -> stmt - -(** A instr to serve as a placeholder *) -val dummyInstr: instr - -(** A statement consisting of just [dummyInstr] *) -val dummyStmt: stmt - -(** Make a while loop. Can contain Break or Continue *) -val mkWhile: guard:exp -> body:stmt list -> stmt list - -(** Make a for loop for(i=start; i<past; i += incr) \{ ... \}. The body - can contain Break but not Continue. Can be used with i a pointer - or an integer. Start and done must have the same type but incr - must be an integer *) -val mkForIncr: iter:varinfo -> first:exp -> stopat:exp -> incr:exp - -> body:stmt list -> stmt list - -(** Make a for loop for(start; guard; next) \{ ... \}. The body can - contain Break but not Continue !!! *) -val mkFor: start:stmt list -> guard:exp -> next: stmt list -> - body: stmt list -> stmt list - - - -(**************************************************) -(** {b Values for manipulating attributes} *) - -(** Various classes of attributes *) -type attributeClass = - AttrName of bool - (** 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 bool - (** 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 *) - -(** This table contains the mapping of predefined attributes to classes. - Extend this table with more attributes as you need. This table is used to - determine how to associate attributes with names or types *) -val attributeHash: (string, attributeClass) Hashtbl.t - -(** Partition the attributes into classes:name attributes, function type, - and type attributes *) -val partitionAttributes: default:attributeClass -> - attributes -> attribute list * (* AttrName *) - attribute list * (* AttrFunType *) - attribute list (* AttrType *) - -(** Add an attribute. Maintains the attributes in sorted order of the second - argument *) -val addAttribute: attribute -> attributes -> attributes - -(** Add a list of attributes. Maintains the attributes in sorted order. The - second argument must be sorted, but not necessarily the first *) -val addAttributes: attribute list -> attributes -> attributes - -(** Remove all attributes with the given name. Maintains the attributes in - sorted order. *) -val dropAttribute: string -> attributes -> attributes - -(** Remove all attributes with names appearing in the string list. - * Maintains the attributes in sorted order *) -val dropAttributes: string list -> attributes -> attributes - -(** Retains attributes with the given name *) -val filterAttributes: string -> attributes -> attributes - -(** True if the named attribute appears in the attribute list. The list of - attributes must be sorted. *) -val hasAttribute: string -> attributes -> bool - -(** Returns all the attributes contained in a type. This requires a traversal - of the type structure, in case of composite, enumeration and named types *) -val typeAttrs: typ -> attribute list - -val setTypeAttrs: typ -> attributes -> typ (* Resets the attributes *) - - -(** Add some attributes to a type *) -val typeAddAttributes: attribute list -> typ -> typ - -(** Remove all attributes with the given names from a type. Note that this - does not remove attributes from typedef and tag definitions, just from - their uses *) -val typeRemoveAttributes: string list -> typ -> typ - - -(****************** - ****************** VISITOR - ******************) -(** {b The visitor} *) - -(** Different visiting actions. 'a will be instantiated with [exp], [instr], - etc. *) -type 'a visitAction = - SkipChildren (** Do not visit the children. Return - the node as it is. *) - | DoChildren (** Continue with the children of this - node. Rebuild the node on return - if any of the children changes - (use == test) *) - | ChangeTo of 'a (** Replace the expression with the - given one *) - | ChangeDoChildrenPost of 'a * ('a -> 'a) (** 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 *) - - - -(** A visitor interface for traversing CIL trees. Create instantiations of - * this type by specializing the class {!Cil.nopCilVisitor}. Each of the - * specialized visiting functions can also call the [queueInstr] to specify - * that some instructions should be inserted before the current instruction - * or statement. Use syntax like [self#queueInstr] to call a method - * associated with the current object. *) -class type cilVisitor = object - method vvdec: varinfo -> varinfo visitAction - (** Invoked for each variable declaration. The subtrees to be traversed - * are those corresponding to the type and attributes of the variable. - * Note that variable declarations are all the [GVar], [GVarDecl], [GFun], - * all the [varinfo] in formals of function types, and the formals and - * locals for function definitions. This means that the list of formals - * in a function definition will be traversed twice, once as part of the - * function type and second as part of the formals in a function - * definition. *) - - method vvrbl: varinfo -> varinfo visitAction - (** Invoked on each variable use. Here only the [SkipChildren] and - * [ChangeTo] actions make sense since there are no subtrees. Note that - * the type and attributes of the variable are not traversed for a - * variable use *) - - method vexpr: exp -> exp visitAction - (** Invoked on each expression occurrence. The subtrees are the - * subexpressions, the types (for a [Cast] or [SizeOf] expression) or the - * variable use. *) - - method vlval: lval -> lval visitAction - (** Invoked on each lvalue occurrence *) - - method voffs: offset -> offset visitAction - (** Invoked on each offset occurrence that is *not* as part - * of an initializer list specification, i.e. in an lval or - * recursively inside an offset. *) - - method vinitoffs: offset -> offset visitAction - (** Invoked on each offset appearing in the list of a - * CompoundInit initializer. *) - - method vinst: instr -> instr list visitAction - (** Invoked on each instruction occurrence. The [ChangeTo] action can - * replace this instruction with a list of instructions *) - - method vstmt: stmt -> stmt visitAction - (** Control-flow statement. The default [DoChildren] action does not - * create a new statement when the components change. Instead it updates - * the contents of the original statement. This is done to preserve the - * sharing with [Goto] and [Case] statements that point to the original - * statement. If you use the [ChangeTo] action then you should take care - * of preserving that sharing yourself. *) - - method vblock: block -> block visitAction (** Block. *) - method vfunc: fundec -> fundec visitAction (** Function definition. - Replaced in place. *) - method vglob: global -> global list visitAction (** Global (vars, types, - etc.) *) - method vinit: init -> init visitAction (** Initializers for globals *) - method vtype: typ -> typ visitAction (** Use of some type. Note - * that for structure/union - * and enumeration types the - * definition of the - * composite type is not - * visited. Use [vglob] to - * visit it. *) - method vattr: attribute -> attribute list visitAction - (** Attribute. Each attribute can be replaced by a list *) - method vattrparam: attrparam -> attrparam visitAction - (** Attribute parameters. *) - - (** Add here instructions while visiting to queue them to preceede the - * current statement or instruction being processed. Use this method only - * when you are visiting an expression that is inside a function body, or - * a statement, because otherwise there will no place for the visitor to - * place your instructions. *) - method queueInstr: instr list -> unit - - (** Gets the queue of instructions and resets the queue. This is done - * automatically for you when you visit statments. *) - method unqueueInstr: unit -> instr list - -end - -(** Default Visitor. Traverses the CIL tree without modifying anything *) -class nopCilVisitor: cilVisitor - -(* other cil constructs *) - -(** Visit a file. This will will re-cons all globals TWICE (so that it is - * tail-recursive). Use {!Cil.visitCilFileSameGlobals} if your visitor will - * not change the list of globals. *) -val visitCilFile: cilVisitor -> file -> unit - -(** A visitor for the whole file that does not change the globals (but maybe - * changes things inside the globals). Use this function instead of - * {!Cil.visitCilFile} whenever appropriate because it is more efficient for - * long files. *) -val visitCilFileSameGlobals: cilVisitor -> file -> unit - -(** Visit a global *) -val visitCilGlobal: cilVisitor -> global -> global list - -(** Visit a function definition *) -val visitCilFunction: cilVisitor -> fundec -> fundec - -(* Visit an expression *) -val visitCilExpr: cilVisitor -> exp -> exp - -(** Visit an lvalue *) -val visitCilLval: cilVisitor -> lval -> lval - -(** Visit an lvalue or recursive offset *) -val visitCilOffset: cilVisitor -> offset -> offset - -(** Visit an initializer offset *) -val visitCilInitOffset: cilVisitor -> offset -> offset - -(** Visit an instruction *) -val visitCilInstr: cilVisitor -> instr -> instr list - -(** Visit a statement *) -val visitCilStmt: cilVisitor -> stmt -> stmt - -(** Visit a block *) -val visitCilBlock: cilVisitor -> block -> block - -(** Visit a type *) -val visitCilType: cilVisitor -> typ -> typ - -(** Visit a variable declaration *) -val visitCilVarDecl: cilVisitor -> varinfo -> varinfo - -(** Visit an initializer *) -val visitCilInit: cilVisitor -> init -> init - - -(** Visit a list of attributes *) -val visitCilAttributes: cilVisitor -> attribute list -> attribute list - -(* And some generic visitors. The above are built with these *) - - -(** {b Utility functions} *) - -(** Whether the pretty printer should print output for the MS VC compiler. - Default is GCC. After you set this function you should call {!Cil.initCIL}. *) -val msvcMode: bool ref - - -(** 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 *) -val useLogicalOperators: bool ref - - -(** A visitor that does constant folding. Pass as argument whether you want - * machine specific simplifications to be done, or not. *) -val constFoldVisitor: bool -> cilVisitor - -(** Styles of printing line directives *) -type lineDirectiveStyle = - | LineComment - | LinePreprocessorInput - | LinePreprocessorOutput - -(** How to print line directives *) -val lineDirectiveStyle: lineDirectiveStyle option ref - -(** Whether we print something that will only be used as input to our own - * parser. In that case we are a bit more liberal in what we print *) -val print_CIL_Input: bool ref - -(** Whether to print the CIL as they are, without trying to be smart and - * print nicer code. Normally this is false, in which case the pretty - * printer will turn the while(1) loops of CIL into nicer loops, will not - * print empty "else" blocks, etc. These is one case howewer in which if you - * turn this on you will get code that does not compile: if you use varargs - * the __builtin_va_arg function will be printed in its internal form. *) -val printCilAsIs: bool ref - -(** The length used when wrapping output lines. Setting this variable to - * a large integer will prevent wrapping and make #line directives more - * accurate. - *) -val lineLength: int ref - -(** Return the string 's' if we're printing output for gcc, suppres - * it if we're printing for CIL to parse back in. the purpose is to - * hide things from gcc that it complains about, but still be able - * to do lossless transformations when CIL is the consumer *) -val forgcc: string -> string - -(** {b Debugging support} *) - -(** A reference to the current location. If you are careful to set this to - * the current location then you can use some built-in logging functions that - * will print the location. *) -val currentLoc: location ref - -(** A reference to the current global being visited *) -val currentGlobal: global ref - - -(** CIL has a fairly easy to use mechanism for printing error messages. This - * mechanism is built on top of the pretty-printer mechanism (see - * {!Pretty.doc}) and the error-message modules (see {!Errormsg.error}). - - Here is a typical example for printing a log message: {v -ignore (Errormsg.log "Expression %a is not positive (at %s:%i)\n" - d_exp e loc.file loc.line) - v} - - and here is an example of how you print a fatal error message that stop the -* execution: {v -Errormsg.s (Errormsg.bug "Why am I here?") - v} - - Notice that you can use C format strings with some extension. The most -useful extension is "%a" that means to consumer the next two argument from -the argument list and to apply the first to [unit] and then to the second -and to print the resulting {!Pretty.doc}. For each major type in CIL there is -a corresponding function that pretty-prints an element of that type: -*) - - -(** Pretty-print a location *) -val d_loc: unit -> location -> Pretty.doc - -(** Pretty-print the {!Cil.currentLoc} *) -val d_thisloc: unit -> Pretty.doc - -(** Pretty-print an integer of a given kind *) -val d_ikind: unit -> ikind -> Pretty.doc - -(** Pretty-print a floating-point kind *) -val d_fkind: unit -> fkind -> Pretty.doc - -(** Pretty-print storage-class information *) -val d_storage: unit -> storage -> Pretty.doc - -(** Pretty-print a constant *) -val d_const: unit -> constant -> Pretty.doc - - -val derefStarLevel: int -val indexLevel: int -val arrowLevel: int -val addrOfLevel: int -val additiveLevel: int -val comparativeLevel: int -val bitwiseLevel: int - -(** Parentheses level. An expression "a op b" is printed parenthesized if its - * parentheses level is >= that that of its context. Identifiers have the - * lowest level and weakly binding operators (e.g. |) have the largest level. - * The correctness criterion is that a smaller level MUST correspond to a - * stronger precedence! - *) -val getParenthLevel: exp -> int - -(** A printer interface for CIL trees. Create instantiations of - * this type by specializing the class {!Cil.defaultCilPrinterClass}. *) -class type cilPrinter = object - method pVDecl: unit -> varinfo -> Pretty.doc - (** Invoked for each variable declaration. Note that variable - * declarations are all the [GVar], [GVarDecl], [GFun], all the [varinfo] - * in formals of function types, and the formals and locals for function - * definitions. *) - - method pVar: varinfo -> Pretty.doc - (** Invoked on each variable use. *) - - method pLval: unit -> lval -> Pretty.doc - (** Invoked on each lvalue occurrence *) - - method pOffset: Pretty.doc -> offset -> Pretty.doc - (** Invoked on each offset occurrence. The second argument is the base. *) - - method pInstr: unit -> instr -> Pretty.doc - (** Invoked on each instruction occurrence. *) - - method pLabel: unit -> label -> Pretty.doc - (** Print a label. *) - - method pStmt: unit -> stmt -> Pretty.doc - (** Control-flow statement. This is used by - * {!Cil.printGlobal} and by {!Cil.dumpGlobal}. *) - - method dStmt: out_channel -> int -> stmt -> unit - (** Dump a control-flow statement to a file with a given indentation. - * This is used by {!Cil.dumpGlobal}. *) - - method dBlock: out_channel -> int -> block -> unit - (** Dump a control-flow block to a file with a given indentation. - * This is used by {!Cil.dumpGlobal}. *) - - method pBlock: unit -> block -> Pretty.doc - - method pBlock: unit -> block -> Pretty.doc - (** Print a block. *) - - method pGlobal: unit -> global -> Pretty.doc - (** Global (vars, types, etc.). This can be slow and is used only by - * {!Cil.printGlobal} but not by {!Cil.dumpGlobal}. *) - - method dGlobal: out_channel -> global -> unit - (** Dump a global to a file with a given indentation. This is used by - * {!Cil.dumpGlobal} *) - - method pFieldDecl: unit -> fieldinfo -> Pretty.doc - (** A field declaration *) - - method pType: Pretty.doc option -> unit -> typ -> Pretty.doc - (* Use of some type in some declaration. The first argument is used to print - * the declared element, or is None if we are just printing a type with no - * name being declared. Note that for structure/union and enumeration types - * the definition of the composite type is not visited. Use [vglob] to - * visit it. *) - - method pAttr: attribute -> Pretty.doc * bool - (** Attribute. Also return an indication whether this attribute must be - * printed inside the __attribute__ list or not. *) - - method pAttrParam: unit -> attrparam -> Pretty.doc - (** Attribute parameter *) - - method pAttrs: unit -> attributes -> Pretty.doc - (** Attribute lists *) - - method pLineDirective: ?forcefile:bool -> location -> Pretty.doc - (** Print a line-number. This is assumed to come always on an empty line. - * If the forcefile argument is present and is true then the file name - * will be printed always. Otherwise the file name is printed only if it - * is different from the last time time this function is called. The last - * file name is stored in a private field inside the cilPrinter object. *) - - method pStmtKind: stmt -> unit -> stmtkind -> Pretty.doc - (** Print a statement kind. The code to be printed is given in the - * {!Cil.stmtkind} argument. The initial {!Cil.stmt} argument - * records the statement which follows the one being printed; - * {!Cil.defaultCilPrinterClass} uses this information to prettify - * statement printing in certain special cases. *) - - method pExp: unit -> exp -> Pretty.doc - (** Print expressions *) - - method pInit: unit -> init -> Pretty.doc - (** Print initializers. This can be slow and is used by - * {!Cil.printGlobal} but not by {!Cil.dumpGlobal}. *) - - method dInit: out_channel -> int -> init -> unit - (** Dump a global to a file with a given indentation. This is used by - * {!Cil.dumpGlobal} *) -end - -class defaultCilPrinterClass: cilPrinter -val defaultCilPrinter: cilPrinter - -(** These are pretty-printers that will show you more details on the internal - * CIL representation, without trying hard to make it look like C *) -class plainCilPrinterClass: cilPrinter -val plainCilPrinter: cilPrinter - -(* zra: This is the pretty printer that Maincil will use. - by default it is set to defaultCilPrinter *) -val printerForMaincil: cilPrinter ref - -(* Top-level printing functions *) -(** Print a type given a pretty printer *) -val printType: cilPrinter -> unit -> typ -> Pretty.doc - -(** Print an expression given a pretty printer *) -val printExp: cilPrinter -> unit -> exp -> Pretty.doc - -(** Print an lvalue given a pretty printer *) -val printLval: cilPrinter -> unit -> lval -> Pretty.doc - -(** Print a global given a pretty printer *) -val printGlobal: cilPrinter -> unit -> global -> Pretty.doc - -(** Print an attribute given a pretty printer *) -val printAttr: cilPrinter -> unit -> attribute -> Pretty.doc - -(** Print a set of attributes given a pretty printer *) -val printAttrs: cilPrinter -> unit -> attributes -> Pretty.doc - -(** Print an instruction given a pretty printer *) -val printInstr: cilPrinter -> unit -> instr -> Pretty.doc - -(** Print a statement given a pretty printer. This can take very long - * (or even overflow the stack) for huge statements. Use {!Cil.dumpStmt} - * instead. *) -val printStmt: cilPrinter -> unit -> stmt -> Pretty.doc - -(** Print a block given a pretty printer. This can take very long - * (or even overflow the stack) for huge block. Use {!Cil.dumpBlock} - * instead. *) -val printBlock: cilPrinter -> unit -> block -> Pretty.doc - -(** Dump a statement to a file using a given indentation. Use this instead of - * {!Cil.printStmt} whenever possible. *) -val dumpStmt: cilPrinter -> out_channel -> int -> stmt -> unit - -(** Dump a block to a file using a given indentation. Use this instead of - * {!Cil.printBlock} whenever possible. *) -val dumpBlock: cilPrinter -> out_channel -> int -> block -> unit - -(** Print an initializer given a pretty printer. This can take very long - * (or even overflow the stack) for huge initializers. Use {!Cil.dumpInit} - * instead. *) -val printInit: cilPrinter -> unit -> init -> Pretty.doc - -(** Dump an initializer to a file using a given indentation. Use this instead of - * {!Cil.printInit} whenever possible. *) -val dumpInit: cilPrinter -> out_channel -> int -> init -> unit - -(** Pretty-print a type using {!Cil.defaultCilPrinter} *) -val d_type: unit -> typ -> Pretty.doc - -(** Pretty-print an expression using {!Cil.defaultCilPrinter} *) -val d_exp: unit -> exp -> Pretty.doc - -(** Pretty-print an lvalue using {!Cil.defaultCilPrinter} *) -val d_lval: unit -> lval -> Pretty.doc - -(** Pretty-print an offset using {!Cil.defaultCilPrinter}, given the pretty - * printing for the base. *) -val d_offset: Pretty.doc -> unit -> offset -> Pretty.doc - -(** Pretty-print an initializer using {!Cil.defaultCilPrinter}. This can be - * extremely slow (or even overflow the stack) for huge initializers. Use - * {!Cil.dumpInit} instead. *) -val d_init: unit -> init -> Pretty.doc - -(** Pretty-print a binary operator *) -val d_binop: unit -> binop -> Pretty.doc - -(** Pretty-print a unary operator *) -val d_unop: unit -> unop -> Pretty.doc - -(** Pretty-print an attribute using {!Cil.defaultCilPrinter} *) -val d_attr: unit -> attribute -> Pretty.doc - -(** Pretty-print an argument of an attribute using {!Cil.defaultCilPrinter} *) -val d_attrparam: unit -> attrparam -> Pretty.doc - -(** Pretty-print a list of attributes using {!Cil.defaultCilPrinter} *) -val d_attrlist: unit -> attributes -> Pretty.doc - -(** Pretty-print an instruction using {!Cil.defaultCilPrinter} *) -val d_instr: unit -> instr -> Pretty.doc - -(** Pretty-print a label using {!Cil.defaultCilPrinter} *) -val d_label: unit -> label -> Pretty.doc - -(** Pretty-print a statement using {!Cil.defaultCilPrinter}. This can be - * extremely slow (or even overflow the stack) for huge statements. Use - * {!Cil.dumpStmt} instead. *) -val d_stmt: unit -> stmt -> Pretty.doc - -(** Pretty-print a block using {!Cil.defaultCilPrinter}. This can be - * extremely slow (or even overflow the stack) for huge blocks. Use - * {!Cil.dumpBlock} instead. *) -val d_block: unit -> block -> Pretty.doc - -(** Pretty-print the internal representation of a global using - * {!Cil.defaultCilPrinter}. This can be extremely slow (or even overflow the - * stack) for huge globals (such as arrays with lots of initializers). Use - * {!Cil.dumpGlobal} instead. *) -val d_global: unit -> global -> Pretty.doc - - -(** Versions of the above pretty printers, that don't print #line directives *) -val dn_exp : unit -> exp -> Pretty.doc -val dn_lval : unit -> lval -> Pretty.doc -(* dn_offset is missing because it has a different interface *) -val dn_init : unit -> init -> Pretty.doc -val dn_type : unit -> typ -> Pretty.doc -val dn_global : unit -> global -> Pretty.doc -val dn_attrlist : unit -> attributes -> Pretty.doc -val dn_attr : unit -> attribute -> Pretty.doc -val dn_attrparam : unit -> attrparam -> Pretty.doc -val dn_stmt : unit -> stmt -> Pretty.doc -val dn_instr : unit -> instr -> Pretty.doc - - -(** Pretty-print a short description of the global. This is useful for error - * messages *) -val d_shortglobal: unit -> global -> Pretty.doc - -(** Pretty-print a global. Here you give the channel where the printout - * should be sent. *) -val dumpGlobal: cilPrinter -> out_channel -> global -> unit - -(** Pretty-print an entire file. Here you give the channel where the printout - * should be sent. *) -val dumpFile: cilPrinter -> out_channel -> string -> file -> unit - - -(* the following error message producing functions also print a location in - * the code. use {!Errormsg.bug} and {!Errormsg.unimp} if you do not want - * that *) - -(** Like {!Errormsg.bug} except that {!Cil.currentLoc} is also printed *) -val bug: ('a,unit,Pretty.doc) format -> 'a - -(** Like {!Errormsg.unimp} except that {!Cil.currentLoc}is also printed *) -val unimp: ('a,unit,Pretty.doc) format -> 'a - -(** Like {!Errormsg.error} except that {!Cil.currentLoc} is also printed *) -val error: ('a,unit,Pretty.doc) format -> 'a - -(** Like {!Cil.error} except that it explicitly takes a location argument, - * instead of using the {!Cil.currentLoc} *) -val errorLoc: location -> ('a,unit,Pretty.doc) format -> 'a - -(** Like {!Errormsg.warn} except that {!Cil.currentLoc} is also printed *) -val warn: ('a,unit,Pretty.doc) format -> 'a - - -(** Like {!Errormsg.warnOpt} except that {!Cil.currentLoc} is also printed. - * This warning is printed only of {!Errormsg.warnFlag} is set. *) -val warnOpt: ('a,unit,Pretty.doc) format -> 'a - -(** Like {!Errormsg.warn} except that {!Cil.currentLoc} and context - is also printed *) -val warnContext: ('a,unit,Pretty.doc) format -> 'a - -(** Like {!Errormsg.warn} except that {!Cil.currentLoc} and context is also - * printed. This warning is printed only of {!Errormsg.warnFlag} is set. *) -val warnContextOpt: ('a,unit,Pretty.doc) format -> 'a - -(** Like {!Cil.warn} except that it explicitly takes a location argument, - * instead of using the {!Cil.currentLoc} *) -val warnLoc: location -> ('a,unit,Pretty.doc) format -> 'a - -(** Sometimes you do not want to see the syntactic sugar that the above - * pretty-printing functions add. In that case you can use the following - * pretty-printing functions. But note that the output of these functions is - * not valid C *) - -(** Pretty-print the internal representation of an expression *) -val d_plainexp: unit -> exp -> Pretty.doc - -(** Pretty-print the internal representation of an integer *) -val d_plaininit: unit -> init -> Pretty.doc - -(** Pretty-print the internal representation of an lvalue *) -val d_plainlval: unit -> lval -> Pretty.doc - -(** Pretty-print the internal representation of an lvalue offset -val d_plainoffset: unit -> offset -> Pretty.doc *) - -(** Pretty-print the internal representation of a type *) -val d_plaintype: unit -> typ -> Pretty.doc - - - -(** {b ALPHA conversion} has been moved to the Alpha module. *) - - -(** Assign unique names to local variables. This might be necessary after you - * transformed the code and added or renamed some new variables. Names are - * not used by CIL internally, but once you print the file out the compiler - * downstream might be confused. You might - * have added a new global that happens to have the same name as a local in - * some function. Rename the local to ensure that there would never be - * confusioin. Or, viceversa, you might have added a local with a name that - * conflicts with a global *) -val uniqueVarNames: file -> unit - -(** {b Optimization Passes} *) - -(** A peephole optimizer that processes two adjacent statements and possibly - replaces them both. If some replacement happens, then the new statements - are themselves subject to optimization *) -val peepHole2: (instr * instr -> instr list option) -> stmt list -> unit - -(** Similar to [peepHole2] except that the optimization window consists of - one statement, not two *) -val peepHole1: (instr -> instr list option) -> stmt list -> unit - -(** {b Machine dependency} *) - - -(** Raised when one of the bitsSizeOf functions cannot compute the size of a - * type. This can happen because the type contains array-length expressions - * that we don't know how to compute or because it is a type whose size is - * not defined (e.g. TFun or an undefined compinfo). The string is an - * explanation of the error *) -exception SizeOfError of string * typ - -(** The size of a type, in bits. Trailing padding is added for structs and - * arrays. Raises {!Cil.SizeOfError} when it cannot compute the size. This - * function is architecture dependent, so you should only call this after you - * call {!Cil.initCIL}. Remember that on GCC sizeof(void) is 1! *) -val bitsSizeOf: typ -> int - -(* The size of a type, in bytes. Returns a constant expression or a "sizeof" - * expression if it cannot compute the size. This function is architecture - * dependent, so you should only call this after you call {!Cil.initCIL}. *) -val sizeOf: typ -> exp - -(** The minimum alignment (in bytes) for a type. This function is - * architecture dependent, so you should only call this after you call - * {!Cil.initCIL}. *) -val alignOf_int: typ -> int - -(** Give a type of a base and an offset, returns the number of bits from the - * base address and the width (also expressed in bits) for the subobject - * denoted by the offset. Raises {!Cil.SizeOfError} when it cannot compute - * the size. This function is architecture dependent, so you should only call - * this after you call {!Cil.initCIL}. *) -val bitsOffset: typ -> offset -> int * int - - -(** Whether "char" is unsigned. Set after you call {!Cil.initCIL} *) -val char_is_unsigned: bool ref - -(** Whether the machine is little endian. Set after you call {!Cil.initCIL} *) -val little_endian: bool ref - -(** Whether the compiler generates assembly labels by prepending "_" to the - identifier. That is, will function foo() have the label "foo", or "_foo"? - Set after you call {!Cil.initCIL} *) -val underscore_name: bool ref - -(** Represents a location that cannot be determined *) -val locUnknown: location - -(** Return the location of an instruction *) -val get_instrLoc: instr -> location - -(** Return the location of a global, or locUnknown *) -val get_globalLoc: global -> location - -(** Return the location of a statement, or locUnknown *) -val get_stmtLoc: stmtkind -> location - - -(** Generate an {!Cil.exp} to be used in case of errors. *) -val dExp: Pretty.doc -> exp - -(** Generate an {!Cil.instr} to be used in case of errors. *) -val dInstr: Pretty.doc -> location -> instr - -(** Generate a {!Cil.global} to be used in case of errors. *) -val dGlobal: Pretty.doc -> location -> global - -(** Like map but try not to make a copy of the list *) -val mapNoCopy: ('a -> 'a) -> 'a list -> 'a list - -(** Like map but each call can return a list. Try not to make a copy of the - list *) -val mapNoCopyList: ('a -> 'a list) -> 'a list -> 'a list - -(** sm: return true if the first is a prefix of the second string *) -val startsWith: string -> string -> bool - - -(** {b An Interpreter for constructing CIL constructs} *) - -(** The type of argument for the interpreter *) -type formatArg = - Fe of exp - | Feo of exp option (** For array lengths *) - | Fu of unop - | Fb of binop - | Fk of ikind - | FE of exp list (** For arguments in a function call *) - | Ff of (string * typ * attributes) (** For a formal argument *) - | FF of (string * typ * attributes) list (** For formal argument lists *) - | Fva of bool (** For the ellipsis in a function type *) - | Fv of varinfo - | Fl of lval - | Flo of lval option - - | Fo of offset - - | Fc of compinfo - | Fi of instr - | FI of instr list - | Ft of typ - | Fd of int - | Fg of string - | Fs of stmt - | FS of stmt list - | FA of attributes - - | Fp of attrparam - | FP of attrparam list - - | FX of string - - -(** Pretty-prints a format arg *) -val d_formatarg: unit -> formatArg -> Pretty.doc - -val lowerConstants: bool ref - (** Do lower constant expressions into constants (default true) *) |