path: root/cil/src/cil.mli

(* 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) *)