package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

The Abstract Syntax of CIL.

Root of the AST

In Frama-C, the whole AST is accessible through Ast.get.

type file = {
  1. mutable fileName : Filepath.Normalized.t;
    (*

    The complete file name

    *)
  2. mutable globals : global list;
    (*

    List of globals as they will appear in the printed file

    *)
  3. 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.

    *)
  4. 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.

    *)
}

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_types.file using the following iterators: Cil.mapGlobals, Cil.iterGlobals and Cil.foldGlobals. You can also use the Cil.dummyFile when you need a Cil_types.file as a placeholder. For each global item CIL stores the source location where it appears (using the type Cil_types.location)

and global =
  1. | 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.

    *)
  2. | 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.

    *)
  3. | GCompTagDecl of compinfo * location
    (*

    Declares a struct/union tag. Use as a forward declaration. This is printed without the fields.

    *)
  4. | 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.

    *)
  5. | GEnumTagDecl of enuminfo * location
    (*

    Declares an enumeration tag. Use as a forward declaration. This is printed without the items.

    *)
  6. | GVarDecl of varinfo * location
    (*

    A variable declaration (not a definition) for a variable with object type. There can be several declarations and at most one definition for a given variable. If both forms appear then they must share the same varinfo structure. Either has storage Extern or there must be a definition in this file

    *)
  7. | GFunDecl of funspec * varinfo * location
    (*

    A variable declaration (not a definition) for a function, i.e. a prototype. There can be several declarations and at most one definition for a given function. If both forms appear then they must share the same varinfo structure. A prototype shares the varinfo with the fundec of the definition. Either has storage Extern or there must be a definition in this file.

    *)
  8. | 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.

    *)
  9. | GFun of fundec * location
    (*

    A function definition.

    *)
  10. | GAsm of string * location
    (*

    Global asm statement. These ones can contain only a template

    *)
  11. | GPragma of attribute * location
    (*

    Pragmas at top level. Use the same syntax as attributes

    *)
  12. | GText of string
    (*

    Some text (printed verbatim) at top level. E.g., this way you can put comments in the output.

    *)
  13. | GAnnot of global_annotation * location
    (*

    a global annotation. Can be

    • an axiom or a lemma
    • a predicate declaration or definition
    • a global type invariant
    • a global invariant
    • a logic function declaration or definition.
    *)

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.

Types

A C type is represented in CIL using the type Cil_types.typ. Among types we differentiate the integral types (with different kinds denoting the sign and precision), floating point types, enumeration types, array and pointer types, and function types. Every type is associated with a list of attributes, which are always kept in sorted order. Use Cil.addAttribute and Cil.addAttributes to construct list of attributes. If you want to inspect a type, you should use Cil.unrollType or Cil.unrollTypeDeep to see through the uses of named types.

CIL is configured at build-time with the sizes and alignments of the underlying compiler (GCC or MSVC). CIL contains functions that can compute the size of a type (in bits) Cil.bitsSizeOf, the alignment of a type (in bytes) Cil.alignOf_int, and can convert an offset into a start and width (both in bits) using the function Cil.bitsOffset. At the moment these functions do not take into account the packed attributes and pragmas.

and typ =
  1. | TVoid of attributes
    (*

    Void type. Also predefined as Cil.voidType

    *)
  2. | 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.

    *)
  3. | TFloat of fkind * attributes
    (*

    A floating-point type. The kind specifies the precision. You can also use the predefined constant Cil.doubleType.

    *)
  4. | 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

    *)
  5. | TArray of typ * exp option * attributes
    (*

    Array type. It indicates the base type and the array length.

    *)
  6. | 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.

    *)
  7. | TNamed of typeinfo * attributes
    (*

    The use of a named type. All uses of the same type name must share the typeinfo. Each such type name must be preceded in the file by a GType global. This is printed as just the type name. The actual referred type is not printed here and is carried only to simplify processing. To see through a sequence of named type references, use Cil.unrollType. The attributes are in addition to those given when the type name was defined.

    *)
  8. | TComp of compinfo * attributes
    (*

    A reference to a struct or a union type. All references to the same struct or union must share the same compinfo among them and with a GCompTag global that precedes all uses (except maybe those that are pointers to the composite type). The attributes given are those pertaining to this use of the type and are in addition to the attributes that were given at the definition of the type and which are stored in the compinfo.

    *)
  9. | 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

    *)
  10. | TBuiltin_va_list of attributes
    (*

    This is the same as the gcc's type with the same name

    *)
and ikind =
  1. | IBool
    (*

    _Bool

    *)
  2. | IChar
    (*

    char

    *)
  3. | ISChar
    (*

    signed char

    *)
  4. | IUChar
    (*

    unsigned char

    *)
  5. | IInt
    (*

    int

    *)
  6. | IUInt
    (*

    unsigned int

    *)
  7. | IShort
    (*

    short

    *)
  8. | IUShort
    (*

    unsigned short

    *)
  9. | ILong
    (*

    long

    *)
  10. | IULong
    (*

    unsigned long

    *)
  11. | ILongLong
    (*

    long long (or _int64 on Microsoft Visual C)

    *)
  12. | IULongLong
    (*

    unsigned long long (or unsigned _int64 on Microsoft Visual C)

    *)

Various kinds of integers

and fkind =
  1. | FFloat
    (*

    float

    *)
  2. | FDouble
    (*

    double

    *)
  3. | FLongDouble
    (*

    long double

    *)

Various kinds of floating-point numbers

Attributes

and attribute =
  1. | 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.)

    *)
  2. | AttrAnnot of string
and attributes = attribute list

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 attrparam =
  1. | AInt of Integer.t
    (*

    An integer constant

    *)
  2. | AStr of string
    (*

    A string constant

    *)
  3. | 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.

    There are some Frama-C builtins that are used to account for OSX's peculiarities:

    • __fc_assign takes two arguments and emulate a1=a2 syntax
    • __fc_float takes one string argument and indicates a floating point constant, that will be printed as such. See https://clang.llvm.org/docs/AttributeReference.html#availability for more information. Proper attributes node might be added if really needed, i.e. if some plug-in wants to interpret the availability attribute.
    *)
  4. | ASizeOf of typ
    (*

    A way to talk about types

    *)
  5. | ASizeOfE of attrparam
  6. | AAlignOf of typ
  7. | AAlignOfE of attrparam
  8. | AUnOp of unop * attrparam
  9. | ABinOp of binop * attrparam * attrparam
  10. | ADot of attrparam * string
    (*

    a.foo *

    *)
  11. | AStar of attrparam
    (*

    * a

    *)
  12. | AAddrOf of attrparam
    (*

    & a *

    *)
  13. | AIndex of attrparam * attrparam
    (*

    a1a2

    *)
  14. | AQuestion of attrparam * attrparam * attrparam
    (*

    a1 ? a2 : a3 *

    *)

The type of parameters of attributes

Structures

The Cil_types.compinfo describes the definition of a structure or union type. Each such Cil_types.compinfo must be defined at the top-level using the GCompTag constructor and must be shared by all references to this type (using either the TComp type constructor or from the definition of the fields.

If all you need is to scan the definition of each composite type once, you can do that by scanning all top-level GCompTag.

Constructing a Cil_types.compinfo can be tricky since it must contain fields that might refer to the host Cil_types.compinfo and furthermore the type of the field might need to refer to the Cil_types.compinfo for recursive types. Use the Cil.mkCompInfo function to create a Cil_types.compinfo. You can easily fetch the Cil_types.fieldinfo for a given field in a structure with Cil.getCompField.

and compinfo = {
  1. mutable cstruct : bool;
    (*

    true if struct, false if union

    *)
  2. corig_name : string;
    (*

    Original name as found in C file. Will never be changed

    *)
  3. 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)

    *)
  4. mutable ckey : int;
    (*

    A unique integer. This is assigned by Cil_const.mkCompInfo using a global variable in the Cil module. Thus two identical structs in two different files might have different keys. Use Cil_const.copyCompInfo to copy structures so that a new key is assigned.

    *)
  5. mutable cfields : fieldinfo list option;
    (*

    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.

    None value means that the type is incomplete.

    • before 23.0-Vanadium

      this field was not optional

    *)
  6. 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.

    *)
  7. mutable creferenced : bool;
    (*

    true if used. Initially set to false.

    *)
}

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.).

Structure fields

The Cil_types.fieldinfo structure is used to describe a structure or union field. Fields, just like variables, can have attributes associated with the field itself or associated with the type of the field (stored along with the type of the field).

and fieldinfo = {
  1. mutable fcomp : compinfo;
    (*

    The host structure that contains this field. There can be only one compinfo that contains the field.

    *)
  2. mutable forder : int;
    (*

    The position in the host structure.

    *)
  3. forig_name : string;
    (*

    original name as found in C file.

    *)
  4. 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

    *)
  5. mutable ftype : typ;
    (*

    The type. If the field is a bitfield, a special attribute FRAMA_C_BITFIELD_SIZE indicating the width of the bitfield is added.

    *)
  6. 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.

    *)
  7. mutable fattr : attributes;
    (*

    The attributes for this field (not for its type)

    *)
  8. mutable floc : location;
    (*

    The location where this field is defined

    *)
  9. mutable faddrof : bool;
    (*

    Adapted from CIL vaddrof field for variables. Only set for non-array fields. Variable whose field address is taken is not marked anymore as having its own address taken. True if the address of this field is taken. CIL will set these flags when it parses C, but you should make sure to set the flag whenever your transformation create AddrOf expression.

    *)
  10. mutable fsize_in_bits : int option;
    (*

    Similar to fbitfield for all types of fields. Do not read this field directly. Use Cil.fieldBitsOffset or Cil.bitsOffset instead.

    *)
  11. mutable foffset_in_bits : int option;
    (*

    Offset at which the field starts in the structure. Do not read this field directly. Use Cil.fieldBitsOffset or Cil.bitsOffset instead.

    *)
}

Information about a struct/union field.

Enumerations

Information about an enumeration. This is shared by all references to an enumeration. Make sure you have a GEnumTag for each of these.

and enuminfo = {
  1. eorig_name : string;
    (*

    original name as found in C file.

    *)
  2. mutable ename : string;
    (*

    The name. Always non-empty.

    *)
  3. mutable eitems : enumitem list;
    (*

    Items. The list must be non-empty

    *)
  4. 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.

    *)
  5. mutable ereferenced : bool;
    (*

    true if used. Initially set to false.

    *)
  6. mutable ekind : ikind;
    (*

    The integer kind used to represent this enum. MSVC always assumes IInt but this is not the case for gcc. See ISO C 6.7.2.2

    *)
}

Information about an enumeration.

and enumitem = {
  1. eiorig_name : string;
    (*

    original name as found in C file.

    *)
  2. mutable einame : string;
    (*

    the name, always non-empty.

    *)
  3. mutable eival : exp;
    (*

    value of the item. Must be a compile-time constant

    *)
  4. mutable eihost : enuminfo;
    (*

    the host enumeration in which the item is declared.

    *)
  5. eiloc : location;
}
and typeinfo = {
  1. torig_name : string;
    (*

    original name as found in C file.

    *)
  2. 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

    *)
  3. mutable ttype : typ;
    (*

    The actual type. This includes the attributes that were present in the typedef

    *)
  4. mutable treferenced : bool;
    (*

    true if used. Initially set to false.

    *)
}

Information about a defined type.

Variables

Each local or global variable is represented by a unique Cil_types.varinfo structure. A global Cil_types.varinfo can be introduced with the GVarDecl or GVar, GFunDecl or GFun globals. A local varinfo can be introduced as part of a function definition Cil_types.fundec.

All references to a given global or local variable must refer to the same copy of the varinfo. Each varinfo has a globally unique identifier that can be used to index maps and hashtables (the name can also be used for this purpose, except for locals from different functions). This identifier is constructor using a global counter.

It is very important that you construct varinfo structures using only one of the following functions:

A varinfo is also used in a function type to denote the list of formals.

and varinfo = {
  1. 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.

    *)
  2. vorig_name : string;
    (*

    the original name of the variable. Need not be unique.

    *)
  3. mutable vtype : typ;
    (*

    The declared type of the variable. For modifications of the field, Cil.update_var_type helps in synchronizing the type of the C variable and the one of the associated logic variable.

    *)
  4. mutable vattr : attributes;
    (*

    A list of attributes associated with the variable.

    *)
  5. mutable vstorage : storage;
    (*

    The storage-class

    *)
  6. mutable vglob : bool;
    (*

    True if this is a global variable

    *)
  7. mutable vdefined : bool;
    (*
    • For global variables, true iff the variable or function is defined in the file.
    • For local variables, true iff the variable is explicitly initialized at declaration time.
    • Unused for formals variables and logic variables.
    *)
  8. mutable vformal : bool;
    (*

    True if the variable is a formal parameter of a function.

    *)
  9. mutable vinline : bool;
    (*

    Whether this varinfo is for an inline function.

    *)
  10. mutable vdecl : location;
    (*

    Location of variable declaration.

    *)
  11. 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.

    *)
  12. 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.

    *)
  13. mutable vreferenced : bool;
    (*

    true if this variable is ever referenced. This is computed by removeUnusedVars. It is safe to just initialize this to false.

    *)
  14. vtemp : bool;
    (*

    true for temporary variables generated by CIL normalization. false for all the other variables.

    *)
  15. mutable vdescr : string option;
    (*

    For most temporary variables, a description of what the var holds. (e.g. for temporaries used for function call results, this string is a representation of the function call.)

    *)
  16. mutable vdescrpure : bool;
    (*

    Indicates whether the vdescr above is a pure expression or call. True for all CIL expressions and Lvals, but false for e.g. function calls. Printing a non-pure vdescr more than once may yield incorrect results.

    *)
  17. mutable vghost : bool;
    (*

    Indicates if the variable is declared in ghost code

    *)
  18. vsource : bool;
    (*

    true iff this variable appears in the source of the program, which is the case of all the variables in the initial AST. Plugins may create variables with vsource=false, for example to handle dynamic allocation. Those variables do *not* have an associated GVar or GVarDecl.

    *)
  19. mutable vlogic_var_assoc : logic_var option;
    (*

    Logic variable representing this variable in the logic world. Do not access this field directly. Instead, call Cil.cvar_to_lvar.

    *)
}

Information about a variable.

and storage =
  1. | NoStorage
    (*

    The default storage. Nothing is printed

    *)
  2. | Static
  3. | Register
  4. | Extern

Storage-class information

Expressions

The CIL expression language contains only the side-effect free expressions of C. They are represented as the type Cil_types.exp. There are several interesting aspects of CIL expressions:

Integer and floating point constants can carry their textual representation. This way the integer 15 can be printed as 0xF if that is how it occurred in the source.

CIL uses arbitrary precision integers to represent the integer constants and also stores the width of the integer type. Care must be taken to ensure that the constant is representable with the given width. Use the functions Cil.kinteger, Cil.kinteger64 and Cil.integer to construct constant expressions. CIL predefines the constants Cil.zero, Cil.one and Cil.mone (for -1).

Use the functions Cil.isConstant and Cil.isInteger to test if an expression is a constant and a constant integer respectively.

CIL keeps the type of all unary and binary expressions. You can think of that type qualifying the operator. Furthermore there are different operators for arithmetic and comparisons on arithmetic types and on pointers.

Another unusual aspect of CIL is that the implicit conversion between an expression of array type and one of pointer type is made explicit, using the StartOf expression constructor (which is not printed). If you apply the AddrOfconstructor 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.

and exp = {
  1. eid : int;
    (*

    unique identifier

    *)
  2. enode : exp_node;
    (*

    the expression itself

    *)
  3. eloc : location;
    (*

    location of the expression.

    *)
}

Expressions (Side-effect free)

and exp_node =
  1. | Const of constant
    (*

    Constant

    *)
  2. | Lval of lval
    (*

    Lvalue

    *)
  3. | 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

    *)
  4. | SizeOfE of exp
    (*

    sizeof(<expression>)

    *)
  5. | 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.

    *)
  6. | AlignOf of typ
    (*

    This corresponds to the GCC __alignof_. Has unsigned int type

    *)
  7. | AlignOfE of exp
  8. | UnOp of unop * exp * typ
    (*

    Unary operation. Includes the type of the result.

    *)
  9. | BinOp of binop * exp * exp * typ
    (*

    Binary operation. Includes the type of the result. The arithmetic conversions are made explicit for the arguments.

    *)
  10. | CastE of typ * exp
    (*

    Use Cil.mkCast to make casts.

    *)
  11. | 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)

    *)
  12. | 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.

    *)

Constants

and constant =
  1. | CInt64 of Integer.t * ikind * string option
    (*

    Integer constant. Give the ikind (see ISO9899 6.1.3.2) and the textual representation. Textual representation is always set to Some s when it comes from user code. This allows us to print a constant as it was represented in the code, for example, 0xF instead of 15. It is usually None for constant generated by Cil itself. Use Cil.integer or Cil.kinteger to create these.

    *)
  2. | 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.

    *)
  3. | CWStr of int64 list
    (*

    Wide character string constant. Note that the local interpretation of such a literal depends on Cil.theMachine.wcharType and Cil.theMachine.wcharKind. Such a constant has type pointer to Cil.theMachine.wcharType. The escape characters in the string have not been "interpreted" in the sense that L"A\xabcd" remains "A\xabcd" rather than being represented as the wide character list with two elements: 65 and 43981. That "interpretation" depends on the underlying wide character type.

    *)
  4. | CChr of char
    (*

    Character constant. This has type int, so use charConstToInt to read the value in case sign-extension is needed.

    *)
  5. | 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.

    *)
  6. | CEnum of enumitem
    (*

    An enumeration constant. Use Cillower.lowerEnumVisitor to replace these with integer constants.

    *)

Literal constants

and unop =
  1. | Neg
    (*

    Unary minus

    *)
  2. | BNot
    (*

    Bitwise complement (~)

    *)
  3. | LNot
    (*

    Logical Not (!)

    *)

Unary operators

and binop =
  1. | PlusA
    (*

    arithmetic +

    *)
  2. | PlusPI
    (*

    pointer + integer

    *)
  3. | MinusA
    (*

    arithmetic -

    *)
  4. | MinusPI
    (*

    pointer - integer

    *)
  5. | MinusPP
    (*

    pointer - pointer

    *)
  6. | Mult
    (*

    *

    *)
  7. | Div
    (*

    /

    *)
  8. | Mod
    (*

    %

    *)
  9. | Shiftlt
    (*

    shift left

    *)
  10. | Shiftrt
    (*

    shift right

    *)
  11. | Lt
    (*

    < (arithmetic comparison)

    *)
  12. | Gt
    (*

    > (arithmetic comparison)

    *)
  13. | Le
    (*

    <= (arithmetic comparison)

    *)
  14. | Ge
    (*

    >= (arithmetic comparison)

    *)
  15. | Eq
    (*

    == (arithmetic comparison)

    *)
  16. | Ne
    (*

    != (arithmetic comparison)

    *)
  17. | BAnd
    (*

    bitwise and

    *)
  18. | BXor
    (*

    exclusive-or

    *)
  19. | BOr
    (*

    inclusive-or

    *)
  20. | LAnd
    (*

    logical and. Unlike other expressions this one does not always evaluate both operands. If you want to use these, you must set Cil.theMachine.useLogicalOperators.

    *)
  21. | LOr
    (*

    logical or. Unlike other expressions this one does not always evaluate both operands. If you want to use these, you must set Cil.theMachine.useLogicalOperators.

    *)

Binary operations

Left values

Left values (aka 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 a[0][1][2] might involve 1, 2 or 3 memory reads when used in an expression context, depending on the declared type of the variable a. If a has type int [4][4][4] then we have one memory read from somewhere inside the area that stores the array a. On the other hand if a has type int *** then the expression really means * ( * ( * (a + 0) + 1) + 2), in which case it is clear that it involves three separate memory operations.

An lvalue denotes the contents of a range of memory addresses. This range is denoted as a host object along with an offset within the object. The host object can be of two kinds: a local or global variable, or an object whose address is in a pointer expression. We distinguish the two cases so that we can tell quickly whether we are accessing some component of a variable directly or we are accessing a memory location through a pointer. To make it easy to tell what an lvalue means CIL represents lvalues as a host object and an offset (see Cil_types.lval). The host object (represented as Cil_types.lhost) can be a local or global variable or can be the object pointed-to by a pointer expression. The offset (represented as Cil_types.offset) is a sequence of field or array index designators.

Both the typing rules and the meaning of an lvalue is very precisely specified in CIL.

The following are a few useful function for operating on lvalues:

The following equivalences hold

    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
and lval = lhost * offset
and lhost =
  1. | Var of varinfo
    (*

    The host is a variable.

    *)
  2. | Mem of exp
    (*

    The host is an object of type T when the expression has pointer TPtr(T).

    *)

The host part of an Cil_types.lval.

and offset =
  1. | 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.

    *)
  2. | 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.

    *)
  3. | 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

    *)

The offset part of an Cil_types.lval. Each offset can be applied to certain kinds of lvalues and its effect is that it advances the starting address of the lvalue and changes the denoted type, essentially focussing to some smaller lvalue that is contained in the original one.

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_types.init. You can create initializers with Cil.makeZeroInit and you can conveniently scan compound initializers them with Cil.foldLeftCompound.

and init =
  1. | SingleInit of exp
    (*

    A single initializer

    *)
  2. | 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 arrays the list must contain a prefix of the initializers; the rest are 0-initialized. For unions there must be exactly one initializer. If the initializer is not for the first field then a field designator is printed, so you better be on GCC since MSVC does not understand this. You can scan an initializer list with Cil.foldLeftCompound.

    *)

Initializers for global variables.

and initinfo = {
  1. mutable init : init option;
}

We want to be able to update an initializer in a global variable, so we define it as a mutable field

kind of constructor for initializing a local variable through a function call.

  • since Phosphorus-20170501-beta1.
and constructor_kind =
  1. | Plain_func
    (*

    plain function call, whose result is used for initializing the variable.

    *)
  2. | Constructor
    (*

    C++-like constructor: the function takes as first argument the address of the variable to be initialized, and returns void.

    *)
and local_init =
  1. | AssignInit of init
    (*

    normal initialization

    *)
  2. | ConsInit of varinfo * exp list * constructor_kind
    (*

    ConsInit(f,args,kind) indicates that the corresponding local is initialized via a call to f, of kind kind with the given args.

    *)

Initializers for local variables.

  • since Phosphorus-20170501-beta1

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_types.fundec. Some of the information (e.g. its name, type, storage, attributes) is stored as a Cil_types.varinfo that is a field of the fundec. To refer to the function from the expression language you must use the varinfo.

The function definition contains, in addition to the body, a list of all the local variables and separately a list of the formals. Both kind of variables can be referred to in the body of the function. The formals must also be shared with the formals that appear in the function type. For that reason, to manipulate formals you should use the provided functions Cil.makeFormalVar and Cil.setFormals.

and fundec = {
  1. 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.

    *)
  2. 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 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.

    *)
  3. mutable slocals : varinfo list;
    (*

    Locals. Does NOT include the sformals. Do not make copies of these because the body refers to them.

    *)
  4. 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.

    *)
  5. mutable sbody : block;
    (*

    The function body.

    *)
  6. 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 Cfg.computeCFGInfo.

    *)
  7. mutable sallstmts : stmt list;
    (*

    After you call Cfg.computeCFGInfo this field is set to contain all statements in the function.

    *)
  8. mutable sspec : funspec;
}

Function definitions.

and block = {
  1. mutable battrs : attributes;
    (*

    Attributes for the block

    *)
  2. mutable bscoping : bool;
    (*

    Whether the block is used to determine the scope of local variables.

    *)
  3. mutable blocals : varinfo list;
    (*

    variables that are local to the block. It is a subset of the slocals of the enclosing function.

    *)
  4. mutable bstatics : varinfo list;
    (*

    static variables whose syntactic scope is restricted to the block. They are normalized as globals, since their lifetime is the whole program execution, but we maintain a syntactic scope information here for better traceability from the original source code.

    *)
  5. mutable bstmts : stmt list;
    (*

    The statements comprising the block.

    *)
}

A block is a sequence of statements with the control falling through from one element to the next. In addition, blocks are used to determine the scope of variables, through the blocals field. Variables in blocals that have their vdefined field set to true must appear as the target of a Local_init instruction directly in the bstmts, with two exceptions: the Local_init instruction can be part of an UnspecifiedSequence, or of a block that has bscoping set to false. Such block _must not_ itself have local variables: it denotes a simple list of statements grouped together (e.g. to stay in scope of an annotation extending to the whole list).

Statements

CIL statements are the structural elements that make the CFG. They are represented using the type Cil_types.stmt. Every statement has a (possibly empty) list of labels. The Cil_types.stmtkind field of a statement indicates what kind of statement it is.

Use Cil.mkStmt to make a statement and the fill-in the fields.

CIL also comes with support for control-flow graphs. The sid field in stmt can be used to give unique numbers to statements, and the succs and preds fields can be used to maintain a list of successors and predecessors for every statement. The CFG information is not computed by default. Instead you must explicitly use the functions Cfg.prepareCFG and Cfg.computeCFGInfo to do it.

and stmt = {
  1. mutable labels : label list;
    (*

    Whether the statement starts with some labels, case statements or default statements.

    *)
  2. mutable skind : stmtkind;
    (*

    The kind of statement

    *)
  3. mutable sid : int;
    (*

    A number (>= 0) that is unique in a function. Filled in only after the CFG is computed.

    *)
  4. 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.

    *)
  5. mutable preds : stmt list;
    (*

    The inverse of the succs function.

    *)
  6. mutable ghost : bool;
  7. mutable sattr : attributes;
    (*

    Statement attributes.

    • since 19.0-Potassium
    *)
}

Statements.

and label =
  1. | 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

    *)
  2. | Case of exp * location
    (*

    A case statement. This expression is lowered into a constant if Cil.theMachine.lowerConstants is set to true.

    *)
  3. | Default of location
    (*

    A default statement

    *)

Labels

and stmtkind =
  1. | Instr of instr
    (*

    An instruction that does not contain control flow. Control implicitly falls through.

    *)
  2. | Return of exp option * location
    (*

    The return statement. This is a leaf in the CFG.

    *)
  3. | Goto of stmt Stdlib.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.

    *)
  4. | Break of location
    (*

    A break to the end of the nearest enclosing Loop or Switch.

    *)
  5. | Continue of location
    (*

    A continue to the start of the nearest enclosing Loop.

    *)
  6. | If of exp * block * block * location
    (*

    A conditional. Two successors, the "then" and the "else" branches (in this order). Both branches fall-through to the successor of the If statement.

    *)
  7. | Switch of exp * block * stmt list * location
    (*

    A switch statement. exp is the index of the switch. block is the body of the switch. stmt list contains the set of statements whose labels are cases of the switch (i.e. for each case, the corresponding statement is in stmt list, a statement cannot appear more than once in the list, and statements in stmt list can have several labels corresponding to several cases.

    *)
  8. | Loop of code_annotation list * 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 Cfg.prepareCFG has been called, the first stmt option will point to the stmt containing the continue label for this loop and the second will point to the stmt containing the break label for this loop.

    *)
  9. | Block of block
    (*

    Just a block of statements. Use it as a way to keep some block attributes local.

    *)
  10. | UnspecifiedSequence of (stmt * lval list * lval list * lval list * stmt Stdlib.ref list) list
    (*

    statements whose order of execution is not specified by ISO/C. This is important for the order of side effects during evaluation of expressions. Each statement comes together with three list of lval, in this order.

    • lvals that are written during the sequence and whose future value depends upon the statement (it is legal to read from them, but not to write to them)
    • lvals that are written during the evaluation of the statement itself
    • lval that are read.
    • Function calls in the corresponding statement Note that this include only a subset of the affectations of the statement. Namely, the temporary variables generated by cil are excluded (i.e. it is assumed that the "compilation" is correct). In addition, side effects caused by function applications are not taken into account in the list. For a single statement, the written lvals are supposed to be ordered (or their order of evaluation doesn't matter), so that an alarm should be emitted only if the lvals read by a statement overlap with the lvals written (or read) by another statement of the sequence.

    At this time this feature is experimental and may miss some unspecified sequences.

    In case you do not care about this feature just handle it like a block (see Cil.block_from_unspecified_sequence).

    *)
  11. | Throw of (exp * typ) option * location
    (*

    Throws an exception, C++ style. We keep the type of the expression, to match it against the appropriate catch clause. A Throw node has no successor, even if it is in try-catch block that will catch the exception: we keep normal and exceptional control-flow completely separate, as in Jo and Chang, ICSSA 2004.

    *)
  12. | TryCatch of block * (catch_binder * block) list * location
  13. | TryFinally of block * block * location
    (*

    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.

    *)
  14. | TryExcept of block * instr list * exp * 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. The location corresponds to the try keyword.

    *)
and catch_binder =
  1. | Catch_exn of varinfo * (varinfo * block) list
    (*

    catch exception of given type(s). If the list is empty, only exceptions with the same type as the varinfo can be caught. If the list is non-empty, only exceptions matching one of the type of a varinfo in the list are caught. The associated block contains the operations necessary to transform the matched varinfo into the principal one. Semantics is by value (i.e. the varinfo is bound to a copy of the caught object).

    This clause is a declaration point for the varinfo(s) mentioned in it. More precisely, for Catch_exn(v_0,[(v_1, b_1),..., (v_n, b_n)]), the v_i must be referenced in the slocals of the enclosing fundec, and _must not_ appear in any blocals of some block. The scope of v_0 is all the b_i and the corresponding block in the catch_binder * block list of the TryCatch node the binder belongs to. The scope of the other v_i is the corresponding b_i.

    *)
  2. | Catch_all
    (*

    default catch clause: all exceptions are caught.

    *)

Kind of exceptions that are caught by a given clause.

and instr =
  1. | Set of lval * exp * location
    (*

    An assignment. A cast is present if the exp has different type from lval

    *)
  2. | Call of lval option * exp * exp list * location
    (*

    optional: result is an lval. A cast might be necessary if the declared result type of the function is not the same as that of the destination. Actual arguments must have a type equivalent (i.e. Cil.need_cast must return false) to the one of the formals of the function. If the type of the result variable is not the same as the declared type of the function result then an implicit cast exists.

    *)
  3. | Local_init of varinfo * local_init * location
    (*

    initialization of a local variable. The corresponding varinfo must belong to the blocals list of the innermost enclosing block that does not have attribute Cil.block_no_scope_attr. Such blocks are purely here for grouping statements and do not play a role for scoping variables. See Cil_types.block definition for more information

    • since Phosphorus-20170501-beta1
    *)
  4. | Asm of attributes * string list * extended_asm option * location
    (*

    An inline assembly instruction. The arguments are (1) a list of attributes (only const and volatile can appear here and only for GCC) (2) templates (CR-separated) (3) GCC extended asm information if any (4) location information

    *)
  5. | Skip of location
  6. | Code_annot of code_annotation * location

Instructions. They may cause effects directly but may not have control flow.

and extended_asm = {
  1. asm_outputs : (string option * string * lval) list;
    (*

    outputs must be lvals with optional names and constraints. I would like these to be actually variables, but I run into some trouble with ASMs in the Linux sources

    *)
  2. asm_inputs : (string option * string * exp) list;
    (*

    inputs with optional names and constraints

    *)
  3. asm_clobbers : string list;
    (*

    register clobbers

    *)
  4. asm_gotos : stmt Stdlib.ref list;
    (*

    list of statements this asm section may jump to. Destination must have a label.

    *)
}

GNU extended-asm information:

  • a list of outputs, each of which is an lvalue with optional names and constraints.
  • a list of input expressions along with constraints
  • clobbered registers
  • Possible destinations statements

Describes a location in a source file

Abstract syntax trees for annotations

and logic_constant =
  1. | Integer of Integer.t * string option
    (*

    Integer constant with a textual representation.

    *)
  2. | LStr of string
    (*

    String constant.

    *)
  3. | LWStr of int64 list
    (*

    Wide character string constant.

    *)
  4. | LChr of char
    (*

    Character constant.

    *)
  5. | LReal of logic_real
  6. | LEnum of enumitem
    (*

    An enumeration constant.

    *)
and logic_real = {
  1. r_literal : string;
    (*

    Initial string representation s.

    *)
  2. r_nearest : float;
    (*

    Nearest approximation of s in double precision.

    *)
  3. r_upper : float;
    (*

    Smallest double u such that s <= u.

    *)
  4. r_lower : float;
    (*

    Greatest double l such that l <= s.

    *)
}

Real constants.

and logic_type =
  1. | Ctype of typ
    (*

    a C type

    *)
  2. | Ltype of logic_type_info * logic_type list
    (*

    an user-defined logic type with its parameters

    *)
  3. | Lvar of string
    (*

    a type variable.

    *)
  4. | Linteger
    (*

    mathematical integers, i.e. Z

    *)
  5. | Lreal
    (*

    mathematical reals, i.e. R

    *)
  6. | Larrow of logic_type list * logic_type
    (*

    (n-ary) function type

    *)

Types of logic terms.

and identified_term = {
  1. it_id : int;
    (*

    the identifier.

    *)
  2. it_content : term;
    (*

    the term

    *)
}

tsets with an unique identifier. Use Logic_const.new_identified_term to generate a new id.

and logic_label =
  1. | StmtLabel of stmt Stdlib.ref
    (*

    label of a C statement.

    *)
  2. | FormalLabel of string
    (*

    label of global annotation.

    *)
  3. | BuiltinLabel of logic_builtin_label

logic label referring to a particular program point.

and logic_builtin_label =
  1. | Here
  2. | Old
  3. | Pre
  4. | Post
  5. | LoopEntry
  6. | LoopCurrent
  7. | Init

builtin logic labels defined in ACSL.

Terms

C Expressions as logic terms follow C constructs (with prefix T)

and term = {
  1. term_node : term_node;
    (*

    kind of term.

    *)
  2. term_loc : Filepath.position * Filepath.position;
    (*

    position in the source file.

    *)
  3. term_type : logic_type;
    (*

    type of the term.

    *)
  4. term_name : string list;
    (*

    names of the term if any. A name can be an arbitrary string, where '"' and '\'' are escaped by a \, and which does not end with a \. Hence, "name" and 'name' should be recognized as a unique label by most tools.

    *)
}

Logic terms.

and term_node =
  1. | TConst of logic_constant
    (*

    a constant.

    *)
  2. | TLval of term_lval
    (*

    an L-value

    *)
  3. | TSizeOf of typ
    (*

    size of a given C type.

    *)
  4. | TSizeOfE of term
    (*

    size of the type of an expression.

    *)
  5. | TSizeOfStr of string
    (*

    size of a string constant.

    *)
  6. | TAlignOf of typ
    (*

    alignment of a type.

    *)
  7. | TAlignOfE of term
    (*

    alignment of the type of an expression.

    *)
  8. | TUnOp of unop * term
    (*

    unary operator.

    *)
  9. | TBinOp of binop * term * term
    (*

    binary operators.

    *)
  10. | TCastE of typ * term
    (*

    cast to a C type.

    *)
  11. | TAddrOf of term_lval
    (*

    address of a term.

    *)
  12. | TStartOf of term_lval
    (*

    beginning of an array.

    *)
  13. | Tapp of logic_info * logic_label list * term list
    (*

    application of a logic function.

    *)
  14. | Tlambda of quantifiers * term
    (*

    lambda abstraction.

    *)
  15. | TDataCons of logic_ctor_info * term list
    (*

    constructor of logic sum-type.

    *)
  16. | Tif of term * term * term
    (*

    conditional operator

    *)
  17. | Tat of term * logic_label
    (*

    term refers to a particular program point.

    *)
  18. | Tbase_addr of logic_label * term
    (*

    base address of a pointer.

    *)
  19. | Toffset of logic_label * term
    (*

    offset from the base address of a pointer.

    *)
  20. | Tblock_length of logic_label * term
    (*

    length of the block pointed to by the term.

    *)
  21. | Tnull
    (*

    the null pointer.

    *)
  22. | TLogic_coerce of logic_type * term
    (*

    implicit conversion from a C type to a logic type. The logic type must not be a Ctype. In particular, used to denote lifting to Linteger and Lreal.

    *)
  23. | TUpdate of term * term_offset * term
    (*

    functional update of a field.

    *)
  24. | Ttypeof of term
    (*

    type tag for a term.

    *)
  25. | Ttype of typ
    (*

    type tag for a C type.

    *)
  26. | Tempty_set
    (*

    the empty set.

    *)
  27. | Tunion of term list
    (*

    union of terms.

    *)
  28. | Tinter of term list
    (*

    intersection of terms.

    *)
  29. | Tcomprehension of term * quantifiers * predicate option
    (*

    set defined in comprehension ({ t[i] | integer i; 0 <= i < 5})

    *)
  30. | Trange of term option * term option
    (*

    range of integers.

    *)
  31. | Tlet of logic_info * term
    (*

    local binding

    *)

the various kind of terms.

and term_lval = term_lhost * term_offset

lvalue: base address and offset.

and term_lhost =
  1. | TVar of logic_var
    (*

    a variable.

    *)
  2. | TResult of typ
    (*

    value returned by a C function. Only used in post-conditions or assigns

    *)
  3. | TMem of term
    (*

    memory access.

    *)

base address of an lvalue.

and model_info = {
  1. mi_name : string;
    (*

    name

    *)
  2. mi_field_type : logic_type;
    (*

    type of the field

    *)
  3. mi_base_type : typ;
    (*

    type to which the field is associated.

    *)
  4. mi_decl : location;
    (*

    where the field has been declared.

    *)
  5. mutable mi_attr : attributes;
    (*

    attributes tied to the field.

    • since Phosphorus-20170501-beta1
    *)
}

model field.

and term_offset =
  1. | TNoOffset
    (*

    no further offset.

    *)
  2. | TField of fieldinfo * term_offset
    (*

    access to the field of a compound type.

    *)
  3. | TModel of model_info * term_offset
    (*

    access to a model field.

    *)
  4. | TIndex of term * term_offset
    (*

    index. Note that a range is denoted by TIndex(Trange(i1,i2),ofs)

    *)

offset of an lvalue.

and logic_info = {
  1. mutable l_var_info : logic_var;
    (*

    we use only fields lv_name and lv_id of l_var_info we should factorize lv_type and l_type+l_profile below

    *)
  2. mutable l_labels : logic_label list;
    (*

    label arguments of the function.

    *)
  3. mutable l_tparams : string list;
    (*

    type parameters

    *)
  4. mutable l_type : logic_type option;
    (*

    return type. None for predicates

    *)
  5. mutable l_profile : logic_var list;
    (*

    type of the arguments.

    *)
  6. mutable l_body : logic_body;
    (*

    body of the function.

    *)
}

description of a logic function or predicate.

and builtin_logic_info = {
  1. mutable bl_name : string;
  2. mutable bl_labels : logic_label list;
  3. mutable bl_params : string list;
  4. mutable bl_type : logic_type option;
  5. mutable bl_profile : (string * logic_type) list;
}
and logic_body =
  1. | LBnone
    (*

    no definition and no reads clause

    *)
  2. | LBreads of identified_term list
    (*

    read accesses performed by a function.

    *)
  3. | LBterm of term
    (*

    direct definition of a function.

    *)
  4. | LBpred of predicate
    (*

    direct definition of a predicate.

    *)
  5. | LBinductive of (string * logic_label list * string list * predicate) list
    (*

    inductive definition

    *)
and logic_type_info = {
  1. mutable lt_name : string;
  2. lt_params : string list;
    (*

    type parameters

    *)
  3. mutable lt_def : logic_type_def option;
    (*

    definition of the type. None for abstract types.

    *)
  4. mutable lt_attr : attributes;
    (*

    attributes associated to the logic type.

    • since Phosphorus-20170501-beta1
    *)
}

Description of a logic type.

and logic_type_def =
  1. | LTsum of logic_ctor_info list
    (*

    sum type with its constructors.

    *)
  2. | LTsyn of logic_type
    (*

    Synonym of another type.

    *)
and logic_var_kind =
  1. | LVGlobal
    (*

    global logic function or predicate.

    *)
  2. | LVC
    (*

    Logic counterpart of a C variable.

    *)
  3. | LVFormal
    (*

    formal parameter of a logic function / predicate or \lambda abstraction

    *)
  4. | LVQuant
    (*

    Bound by a quantifier (\exists or \forall)

    *)
  5. | LVLocal
    (*

    local \let

    *)

origin of a logic variable.

and logic_var = {
  1. mutable lv_name : string;
    (*

    name of the variable.

    *)
  2. mutable lv_id : int;
    (*

    unique identifier

    *)
  3. mutable lv_type : logic_type;
    (*

    type of the variable.

    *)
  4. mutable lv_kind : logic_var_kind;
    (*

    kind of the variable

    *)
  5. mutable lv_origin : varinfo option;
    (*

    when the logic variable stems from a C variable, set to the original C variable.

    *)
  6. mutable lv_attr : attributes;
    (*

    attributes tied to the logic variable

    • since Phosphorus-20170501-beta1
    *)
}

description of a logic variable

and logic_ctor_info = {
  1. mutable ctor_name : string;
    (*

    name of the constructor.

    *)
  2. ctor_type : logic_type_info;
    (*

    type to which the constructor belongs.

    *)
  3. ctor_params : logic_type list;
    (*

    types of the parameters of the constructor.

    *)
}

Description of a constructor of a logic sum-type.

Predicates

and quantifiers = logic_var list

variables bound by a quantifier.

and relation =
  1. | Rlt
  2. | Rgt
  3. | Rle
  4. | Rge
  5. | Req
  6. | Rneq
    (*

    Different

    *)

comparison relations

and predicate_node =
  1. | Pfalse
    (*

    always-false predicate.

    *)
  2. | Ptrue
    (*

    always-true predicate.

    *)
  3. | Papp of logic_info * logic_label list * term list
    (*

    application of a predicate.

    *)
  4. | Pseparated of term list
  5. | Prel of relation * term * term
    (*

    comparison of two terms.

    *)
  6. | Pand of predicate * predicate
    (*

    conjunction

    *)
  7. | Por of predicate * predicate
    (*

    disjunction.

    *)
  8. | Pxor of predicate * predicate
    (*

    logical xor.

    *)
  9. | Pimplies of predicate * predicate
    (*

    implication.

    *)
  10. | Piff of predicate * predicate
    (*

    equivalence.

    *)
  11. | Pnot of predicate
    (*

    negation.

    *)
  12. | Pif of term * predicate * predicate
    (*

    conditional

    *)
  13. | Plet of logic_info * predicate
    (*

    definition of a local variable

    *)
  14. | Pforall of quantifiers * predicate
    (*

    universal quantification.

    *)
  15. | Pexists of quantifiers * predicate
    (*

    existential quantification.

    *)
  16. | Pat of predicate * logic_label
    (*

    predicate refers to a particular program point.

    *)
  17. | Pobject_pointer of logic_label * term
    (*

    the given locations can be pointed to.

    *)
  18. | Pvalid_read of logic_label * term
    (*

    the given locations are valid for reading.

    *)
  19. | Pvalid of logic_label * term
    (*

    the given locations are valid.

    *)
  20. | Pvalid_function of term
    (*

    the pointed function has a type compatible with the one of pointer.

    *)
  21. | Pinitialized of logic_label * term
    (*

    the given locations are initialized.

    *)
  22. | Pdangling of logic_label * term
    (*

    the given locations contain dangling addresses.

    *)
  23. | Pallocable of logic_label * term
    (*

    the given locations can be allocated.

    *)
  24. | Pfreeable of logic_label * term
    (*

    the given locations can be free.

    *)
  25. | Pfresh of logic_label * logic_label * term * term
    (*

    \fresh(pointer, n) A memory block of n bytes is newly allocated to the pointer.

    *)

predicates

and identified_predicate = {
  1. ip_id : int;
    (*

    identifier

    *)
  2. ip_content : toplevel_predicate;
    (*

    the predicate itself

    *)
}

predicate with an unique identifier. Use Logic_const.new_predicate to create fresh predicates

and predicate_kind =
  1. | Assert
  2. | Check
  3. | Admit
and toplevel_predicate = {
  1. tp_kind : predicate_kind;
    (*

    whether the annotation is only used to check that ip_content holds, but stays invisible for other verification tasks (see description of ACSL's check keyword).

    *)
  2. tp_statement : predicate;
}

main statement of an annotation.

and predicate = {
  1. pred_name : string list;
    (*

    list of given names

    *)
  2. pred_loc : location;
    (*

    position in the source code.

    *)
  3. pred_content : predicate_node;
    (*

    content

    *)
}

predicates with a location and an optional list of names

and variant = term * logic_info option

variant of a loop or a recursive function.

and allocation =
  1. | FreeAlloc of identified_term list * identified_term list
    (*

    tsets. Empty list means \nothing.

    *)
  2. | FreeAllocAny
    (*

    Nothing specified. Semantics depends on where it is written.

    *)

allocates and frees.

  • since Oxygen-20120901
and deps =
  1. | From of identified_term list
    (*

    tsets. Empty list means \nothing.

    *)
  2. | FromAny
    (*

    Nothing specified. Any location can be involved.

    *)

dependencies of an assigned location.

and from = identified_term * deps
and assigns =
  1. | WritesAny
    (*

    Nothing specified. Anything can be written.

    *)
  2. | Writes of from list
    (*

    list of locations that can be written. Empty list means \nothing.

    *)

zone assigned with its dependencies.

and spec = {
  1. mutable spec_behavior : behavior list;
    (*

    behaviors

    *)
  2. mutable spec_variant : variant option;
    (*

    variant for recursive functions.

    *)
  3. mutable spec_terminates : identified_predicate option;
    (*

    termination condition.

    *)
  4. mutable spec_complete_behaviors : string list list;
    (*

    list of complete behaviors. It is possible to have more than one set of complete behaviors

    *)
  5. mutable spec_disjoint_behaviors : string list list;
    (*

    list of disjoint behaviors. It is possible to have more than one set of disjoint behaviors

    *)
}

Function or statement contract. This type shares the name of its constructors with Logic_ptree.spec.

and acsl_extension = {
  1. ext_id : int;
  2. ext_name : string;
  3. ext_loc : location;
  4. ext_has_status : bool;
  5. ext_kind : acsl_extension_kind;
}

Extension to standard ACSL clause with an unique identifier.

The integer is a (unique) identifier. The boolean flag is true if the annotation can be assigned a property status.

Use Logic_const.new_acsl_extension to create new acsl extension with a fresh id. Each extension is associated with a keyword, and can be either a global annotation, the clause of a function contract, a code annotation, or a loop annotation. An extension can be registered through the function Acsl_extension.register_xxx.

It is _not_ possible to register the same keyword for annotations at two different levels (e.g. global and behavior), as this would make the grammar ambiguous.

and acsl_extension_kind =
  1. | Ext_id of int
    (*

    id used internally by the extension itself.

    *)
  2. | Ext_terms of term list
  3. | Ext_preds of predicate list
    (*

    a list of predicates, the most common case of for extensions

    *)
  4. | Ext_annot of string * acsl_extension list
and ext_category =
  1. | Ext_contract
  2. | Ext_global
  3. | Ext_code_annot of ext_code_annot_context

Where are we expected to find corresponding extension keyword.

  • since 18.0-Argon
and ext_code_annot_context =
  1. | Ext_here
    (*

    at current program point.

    *)
  2. | Ext_next_stmt
    (*

    covers next statement.

    *)
  3. | Ext_next_loop
    (*

    covers next loop.

    *)
  4. | Ext_next_both
    (*

    can be found both as normal code annot or loop annot.

    *)
and behavior = {
  1. mutable b_name : string;
    (*

    name of the behavior.

    *)
  2. mutable b_requires : identified_predicate list;
    (*

    require clauses.

    *)
  3. mutable b_assumes : identified_predicate list;
    (*

    assume clauses.

    *)
  4. mutable b_post_cond : (termination_kind * identified_predicate) list;
    (*

    post-condition.

    *)
  5. mutable b_assigns : assigns;
    (*

    assignments.

    *)
  6. mutable b_allocation : allocation;
    (*

    frees, allocates.

    *)
  7. mutable b_extended : acsl_extension list;
    (*

    extensions

    *)
}

Behavior of a function or statement. This type shares the name of its constructors with Logic_ptree.behavior.

and termination_kind =
  1. | Normal
  2. | Exits
  3. | Breaks
  4. | Continues
  5. | Returns

kind of termination a post-condition applies to. See ACSL manual.

and loop_pragma =
  1. | Unroll_specs of term list
  2. | Widen_hints of term list
  3. | Widen_variables of term list

Pragmas for the value analysis plugin of Frama-C.

and slice_pragma =
  1. | SPexpr of term
  2. | SPctrl
  3. | SPstmt

Pragmas for the slicing plugin of Frama-C.

and impact_pragma =
  1. | IPexpr of term
  2. | IPstmt

Pragmas for the impact plugin of Frama-C.

and pragma =
  1. | Loop_pragma of loop_pragma
  2. | Slice_pragma of slice_pragma
  3. | Impact_pragma of impact_pragma

The various kinds of pragmas.

and code_annotation_node =
  1. | AAssert of string list * toplevel_predicate
    (*

    assertion to be checked. The list of strings is the list of behaviors to which this assertion applies.

    *)
  2. | AStmtSpec of string list * spec
    (*

    statement contract (potentially restricted to some enclosing behaviors).

    *)
  3. | AInvariant of string list * bool * toplevel_predicate
    (*

    loop/code invariant. The list of strings is the list of behaviors to which this invariant applies. The boolean flag is true for normal loop invariants and false for invariant-as-assertions.

    *)
  4. | AVariant of variant
    (*

    loop variant. Note that there can be at most one variant associated to a given statement

    *)
  5. | AAssigns of string list * assigns
    (*

    loop assigns. (see b_assigns in the behaviors for other assigns). At most one clause associated to a given (statement, behavior) couple.

    *)
  6. | AAllocation of string list * allocation
    (*

    loop allocation clause. (see b_allocation in the behaviors for other allocation clauses). At most one clause associated to a given (statement, behavior) couple.

    • since Oxygen-20120901 when [b_allocation] has been added.
    *)
  7. | APragma of pragma
    (*

    pragma.

    *)
  8. | AExtended of string list * bool * acsl_extension
    (*

    extension in a code or loop annotation. Boolean flag is true for loop extensions and false for code extensions

    • since Silicon-20161101
    *)

all annotations that can be found in the code. This type shares the name of its constructors with Logic_ptree.code_annot.

function contract.

and funspec = spec
and code_annotation = {
  1. annot_id : int;
    (*

    identifier.

    *)
  2. annot_content : code_annotation_node;
    (*

    content of the annotation.

    *)
}

code annotation with an unique identifier. Use Logic_const.new_code_annotation to create new code annotations with a fresh id.

and funbehavior = behavior

behavior of a function.

and global_annotation =
  1. | Dfun_or_pred of logic_info * location
  2. | Dvolatile of identified_term list * varinfo option * varinfo option * attributes * location
    (*

    associated terms, reading function, writing function

    *)
  3. | Daxiomatic of string * global_annotation list * attributes * location
  4. | Dtype of logic_type_info * location
    (*

    declaration of a logic type.

    *)
  5. | Dlemma of string * logic_label list * string list * toplevel_predicate * attributes * location
    (*

    definition of all kinds of lemmas (axioms are admit lemmas).

    *)
  6. | Dinvariant of logic_info * location
    (*

    global invariant. The predicate does not have any argument.

    *)
  7. | Dtype_annot of logic_info * location
    (*

    type invariant. The predicate has exactly one argument.

    *)
  8. | Dmodel_annot of model_info * location
    (*

    Model field for a type t, seen as a logic function with one argument of type t

    *)
  9. | Dextended of acsl_extension * attributes * location
    (*

    Extended global clause.

    *)

global annotations, not attached to a statement or a function.

type kinstr =
  1. | Kstmt of stmt
  2. | Kglobal
type cil_function =
  1. | Definition of fundec * location
    (*

    defined function

    *)
  2. | Declaration of funspec * varinfo * varinfo list option * location
    (*

    Declaration(spec,f,args,loc) represents a leaf function f with specification spec and arguments args, at location loc. As with the TFun constructor of Cil_types.typ, the arg list is optional, to distinguish void f() (None) from void f(void) (Some []).

    *)

Internal representation of decorated C functions

type kernel_function = {
  1. mutable fundec : cil_function;
  2. mutable spec : funspec;
}

Only field fundec can be used directly. Use Annotations.funspec, Annotations.add_* and Annotations.remove_* to query or modify field spec.

type syntactic_scope =
  1. | Global
    (*

    Any global symbol, whether static or not.

    • since 27.0-Cobalt
    *)
  2. | Program
    (*

    Only non-static global symbols.

    *)
  3. | Translation_unit of Filepath.Normalized.t
    (*

    Any global visible within the given C source file.

    *)
  4. | Formal of kernel_function
    (*

    formal parameter of the given function.

    • since 27.0-Cobalt
    *)
  5. | Block_scope of stmt
    (*

    locals (including static locals) of the block to which the given statement belongs.

    *)
  6. | Whole_function of kernel_function
    (*

    same as above, but any local variable of the given function, regardless of the block to which it is tied, will be considered.

    • since 27.0-Cobalt
    *)

Various syntactic scopes through which an identifier might be searched. Note that for this purpose static variables are still tied to the block where they were declared in the original source (see Cil_types.block).

  • since Chlorine-20180501
type mach = {
  1. sizeof_short : int;
  2. sizeof_int : int;
  3. sizeof_long : int;
  4. sizeof_longlong : int;
  5. sizeof_ptr : int;
  6. sizeof_float : int;
  7. sizeof_double : int;
  8. sizeof_longdouble : int;
  9. sizeof_void : int;
  10. sizeof_fun : int;
  11. size_t : string;
  12. ssize_t : string;
  13. wchar_t : string;
  14. ptrdiff_t : string;
  15. intptr_t : string;
  16. uintptr_t : string;
  17. int_fast8_t : string;
  18. int_fast16_t : string;
  19. int_fast32_t : string;
  20. int_fast64_t : string;
  21. uint_fast8_t : string;
  22. uint_fast16_t : string;
  23. uint_fast32_t : string;
  24. uint_fast64_t : string;
  25. wint_t : string;
  26. sig_atomic_t : string;
  27. time_t : string;
  28. alignof_short : int;
  29. alignof_int : int;
  30. alignof_long : int;
  31. alignof_longlong : int;
  32. alignof_ptr : int;
  33. alignof_float : int;
  34. alignof_double : int;
  35. alignof_longdouble : int;
  36. alignof_str : int;
  37. alignof_fun : int;
  38. char_is_unsigned : bool;
  39. little_endian : bool;
  40. alignof_aligned : int;
  41. has__builtin_va_list : bool;
  42. compiler : string;
  43. cpp_arch_flags : string list;
  44. version : string;
  45. weof : string;
  46. wordsize : string;
  47. posix_version : string;
  48. bufsiz : string;
  49. eof : string;
  50. fopen_max : string;
  51. filename_max : string;
  52. host_name_max : string;
  53. tty_name_max : string;
  54. l_tmpnam : string;
  55. path_max : string;
  56. tmp_max : string;
  57. rand_max : string;
  58. mb_cur_max : string;
  59. nsig : string;
  60. errno : (string * string) list;
  61. machdep_name : string;
  62. custom_defs : string;
}

Definition of a machine model (architecture + compiler).

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct