Frama-C API - Cil

• deprecated

  30.0-Zinc

• deprecated

  30.0-Zinc

• deprecated

  30.0-Zinc

• deprecated

  30.0-Zinc

• deprecated

  30.0-Zinc

Make an empty function from an existing global varinfo.

• since Nitrogen-20111001

Make an empty function

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.

Takes as input a function type (or a typename on it) and return its return type.

Change the return type of the function passed as 1st argument to be the type passed as 2nd argument.

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

Set the type of the function and make formal arguments for them

Update the smaxid after you have populated with locals and formals (unless you constructed those using Cil.makeLocalVar or Cil.makeTempVar.

state of the table associating formals to each prototype.

creates a new varinfo for the parameter of a prototype. By default, this formal variable is not ghost.

Update the formals of a function declaration from its identifier and its type. For a function definition, use Cil.setFormals. Do nothing if the type is not a function type or if the list of argument is empty.

remove a binding from the table.

• since Oxygen-20120901

replace formals of a function declaration with the given list of varinfo.

iterate the given function on declared prototypes.

• since Oxygen-20120901

Get the formals of a function declaration registered with Cil.setFormalsDecl.

• raises Not_found

  if the function is not registered (this is in particular the case for prototypes with an empty list of arguments. See Cil.setFormalsDecl)

A dummy file

Iterate over all globals, including the global initializer

Fold over all globals, including the global initializer

Map over all globals, including the global initializer and change things in place

Find a function or function prototype with the given name in the file. If it does not exist, create a prototype with the given type, and return the new varinfo. This is useful when you need to call a libc function whose prototype may or may not already exist in the file.

Because the new prototype is added to the start of the file, you shouldn't refer to any struct or union types in the function type.

creates an expression with a fresh id

performs a deep copy of an expression (especially, avoid eid sharing).

• since Nitrogen-20111001

creates an expression with a dummy id. Use with caution, i.e. not on expressions that may be put in the AST.

Return true on case and default labels, false otherwise.

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

An empty statement. Used in pretty printing

Returns a location that ranges over the two locations in arguments.

Make a initializer for zero-ing a data type

Fold over the list of initializers in a Compound (not also the nested ones). doinit is called on every present initializer, even if it is of compound type. The parameters of doinit are: the offset in the compound (this is Field(f,NoOffset) or Index(i,NoOffset)), the initializer value, expected type of the initializer value, accumulator. In the case of arrays there might be missing zero-initializers at the end of the list. These are scanned only if implicit is true. This is much like List.fold_left except we also pass the type of the initializer.

This is a good way to use it to scan even nested initializers :

  let rec myInit (lv: lval) (i: init) (acc: 'a) : 'a =
    match i with
      | SingleInit e -> (* ... do something with [lv] and [e] and [acc] ... *)
      | CompoundInit (ct, initl) ->
         foldLeftCompound ~implicit:false
           ~doinit:(fun off' i' _typ acc' ->
                      myInit (addOffsetLval off' lv) i' acc')
           ~ct
           ~initl
           ~acc

is the given type "void"?

is the given type "void *"?

Any signed integer type of size 16 bits. It is equivalent to the ISO C int16_t type but without using the corresponding header. Must only be called if such type exists in the current architecture.

• since 23.0-Vanadium

Any signed integer type of size 32 bits. It is equivalent to the ISO C int32_t type but without using the corresponding header. Must only be called if such type exists in the current architecture.

• since 23.0-Vanadium

Any signed integer type of size 64 bits. It is equivalent to the ISO C int64_t type but without using the corresponding header. Must only be called if such type exists in the current architecture.

• since 23.0-Vanadium

Any unsigned integer type of size 16 bits. It is equivalent to the ISO C uint16_t type but without using the corresponding header. Must only be called if such type exists in the current architecture.

• since Nitrogen-20111001

Any unsigned integer type of size 32 bits. It is equivalent to the ISO C uint32_t type but without using the corresponding header. Must only be called if such type exists in the current architecture.

• since Nitrogen-20111001

Any unsigned integer type of size 64 bits. It is equivalent to the ISO C uint64_t type but without using the corresponding header. Must only be called if such type exists in the current architecture.

• since Nitrogen-20111001

• returns

  true if and only if the given type is a signed integer type.

• returns

  true if and only if the given type is an unsigned integer type.

• since Oxygen-20120901

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.

Get the full name of a comp, including the 'struct' or 'union' prefix

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.

• parameter allowZeroSizeArrays

  indicates whether arrays of size 0 (a gcc extension) are considered as complete. Default value depends on the current machdep.

Performs lvalue-conversion on the type and returns the converted type, or Error if the type is incomplete and not an array type.

• since 27.0-Cobalt

true iff the given type is variably modified, i.e., an array with variable size (VLA), or a composite type containing such an array.

true iff the given type is a struct whose last field is a flexible array member. When in gcc mode, a zero-sized array is identified with a FAM for this purpose.

• since 18.0-Argon

true iff the given type has flexible array member, in GCC/MSVC mode, this function mode recursively searches in the type of the last field.

• before 24.0-Chromium

  this function didn't take in account the GCC/MSVC mode

Unroll a type until it exposes a non TNamed. Will collect all attributes appearing in TNamed!!!

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

Separate out the storage-modifier name attributes

returns the type of the result of an arithmetic operator applied to values of the corresponding input types.

• since Nitrogen-20111001 (moved from Cabs2cil)

performs the usual integral promotions mentioned in C reference manual.

• since Nitrogen-20111001 (moved from Cabs2cil)

True if the argument is a character type (i.e. plain, signed or unsigned)

• since Chlorine-20180501

True if the argument is a plain character type (but neither signed char nor unsigned char).

True if the argument is a short type (i.e. signed or unsigned)

True if the argument is a pointer to a character type (i.e. plain, signed or unsigned).

• since Chlorine-20180501

True if the argument is a pointer to a plain character type (but neither signed char nor unsigned char).

True if the argument is a pointer to a constant character type, e.g. a string literal.

• since Chlorine-20180501

True if the argument is an array of a character type (i.e. plain, signed or unsigned)

• since Chlorine-20180501

True if the argument is an array of a character type (i.e. plain, signed or unsigned)

True if the argument is an integral type (i.e. integer or enum)

True if the argument is _Bool

• since 19.0-Potassium

True if the argument is intptr_t (but _not_ its underlying integer type)

• since 30.0-Zinc

True if the argument is uintptr_t (but _not_ its underlying integer type)

• since 30.0-Zinc

True if the argument is _Bool or boolean.

• since 19.0-Potassium

True if the argument is an integral or pointer type.

True if the argument is an integral type (i.e. integer or enum), either C or mathematical one.

True if the argument is a boolean type, either integral C type or mathematical boolean one.

True if the argument is a floating point type.

True if the argument is a floating point type.

True if the argument is a C floating point type or logic 'real' type.

True if the argument is the logic 'real' type.

True if the argument is an arithmetic type (i.e. integer, enum or floating point

True if the argument is a scalar type (i.e. integral, enum, floating point or pointer

• since 22.0-Titanium

True if the argument is a logic arithmetic type (i.e. integer, enum or floating point, either C or mathematical one.

True if the argument is a function type

True if the argument is the logic function type. Expands the logic type definition if necessary.

• since 18.0-Argon

True if the argument is a pointer type.

True if the argument is a function pointer type.

• since 18.0-Argon

True if the argument is the logic function pointer type. Expands the logic type definition if necessary.

• since 18.0-Argon

Check if a type is a transparent union, and return the first field

• since 28.0-Nickel

True if the argument is the type for reified C types.

True if the argument denotes the type of ... in a variadic function.

• since Nitrogen-20111001 moved from cabs2cil

Obtain the argument list ( if None).

• since 20.0-Calcium Beware that it contains the ghost arguments.

Obtain the argument lists (non-ghost, ghosts) (, if None)

• since 20.0-Calcium

True if the argument is an array type

True if the argument is an array type without size

• since 28.0-Nickel

True if the argument is a sized array type

• since 28.0-Nickel

True if the argument is a struct

• since 28.0-Nickel

True if the argument is a union type

• since 28.0-Nickel

True if the argument is a struct or union type

possible causes for raising Cil.LenOfArray

Raised when Cil.lenOfArray fails either because the length is None, because it is a non-constant expression, or because it overflows an int.

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.

Return a named fieldinfo in compinfo, or raise Not_found

Return the compinfo of the typ, or raise Not_found

A datatype to be used in conjunction with existsType

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

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

Same as Cil.splitFunctionType but takes a varinfo. Prints a nicer error message if the varinfo is not for a function

Used in combineTypes and combineTypesGen to indicate what we want to combine.

• since 28.0-Nickel

combineAttributes what olda a combines the attributes in olda and a according to what:

• if what == CombineFunarg, then override old attributes; this is used to ensure that attributes from formal argument types in a function definition are not mixed with attributes from arguments in other (compatible, but with different qualifiers) declarations;
• else, perform the union of old and new attributes.

• since 28.0-Nickel

combineFunction contains information on how enum, struct/union and typedef are to be handled when combining with combineTypes and combineTypesGen. In pratice, the first argument of each field is a recursive definition.

• since 28.0-Nickel

• before 29.0-Copper

  strictReturnTypes was not named and strictInteger not present in typ_combine.

combineTypesGen ~strictInteger ~strictReturnTypes combF combW oldt newt Combine oldt and newt accordingly to combF, combW indicates what we are combinining.

Warning : this is not commutative. Indeed, excluding enum, struct/union and typedef which depend on combF, the resulting type is as close as possible to newt.

If strictInteger is true, same size/sign integers with different types will not be combined. Emits a warning if it is false and the compatibility is machine-dependent.

If strictReturnTypes is false, anything will be considered compatible with void if combW is CombineFunret (i.e. comparing function return types).

~emitwith is used to emit warnings.

• raises Cannot_combine

  with an explanation when the type cannot be combined.

• since 28.0-Nickel

• before 29.0-Copper

  strictInteger (true) and strictReturnTypes (false) were optional

Specialized version of combineTypesGen], we suppose here that if two global symbols are equal, then they are the same object. @since 28.0-Nickel @before 29.0-Copper [strictInteger (true)] was not present and left with its default value in combineTypesGen.

How type qualifiers must be checked when checking for types compatibility with areCompatibleTypes and compatibleTypes.

• since 28.0-Nickel

areCompatibleTypes returns true if two types are compatible. context indicates how check the compatibility of qualifiers. Other arguments are the same than combineTypes.

• since 28.0-Nickel

Same as areCompatibleTypes old newt but combine oldt and newt. context does not impact the qualifiers of the result.

• raises Cannot_combine

  if oldt and newt are not compatible.

• since 28.0-Nickel

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 temp argument defaults to false, and corresponds to the vtemp field in type Cil_types.varinfo. The source argument defaults to true, and corresponds to the field vsource . The referenced argument defaults to false, and corresponds to the field vreferenced . The ghost argument defaults to false, and corresponds to the field vghost . The loc argument defaults to Location.unknown, and corresponds to the field vdecl . The first unnamed argument specifies whether the varinfo is for a global and the second is for formals.

Make a formal variable for a function declaration. 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.

The ghost parameter indicates if the variable should be inserted in the list of formals or ghost formals. By default, it takes the ghost status of the function where the formal is inserted. Note that:

• specifying ghost to false if the function is ghost leads to an error
• when where is specified, its status must be the same as the formal to insert (else, it cannot be found in the list of ghost or non ghost formals)

Make a local variable and add it to a function's slocals and to the given block (only if insert = true, which is the default). Make sure you know what you are doing if you set insert=false. temp is passed to Cil.makeVarinfo. The variable is attached to the toplevel block if scope is not specified. If the name passed as argument already exists within the function, a fresh name will be generated for the varinfo.

if needed, rename the given varinfo so that its vname does not clash with the one of a local or formal variable of the given function.

• since Chlorine-20180501

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. Optionally, you can give the variable a description of its contents and its location. Temporary variables are always considered as generated variables. If insert is true (the default), the variable will be inserted among other locals of the function. The value for insert should only be changed if you are completely sure this is not useful.

Make a global variable. Your responsibility to make sure that the name is unique. source defaults to true. temp defaults to false.

Make a shallow copy of a varinfo and assign a new identifier. If the original varinfo has an associated logic var, it is copied too and associated to the copied varinfo

Changes the type of a varinfo and of its associated logic var if any.

• since Neon-20140301

Is an lvalue a bitfield?

Returns the last offset in the chain.

Add an offset at the end of an lvalue. Make sure the type of the lvalue and the offset are compatible.

addOffset o1 o2 adds o1 to the end of o2.

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.

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.

Compute the type of an lvalue

Compute the type of an lhost (with no offset)

Equivalent to typeOfLval for terms.

Compute the type of an offset from a base type

Equivalent to typeOffset for terms.

Compute the type of an initializer

indicates whether the given lval is a modifiable lvalue in the sense of the C standard 6.3.2.1§1.

0

1

-1

Construct an integer of a given kind without literal representation. Truncate the integer if kind is given, and the integer does not fit inside the type. The integer can have an optional literal representation repr.

• raises Not_representable

  if no ikind is provided and the integer is not representable.

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

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

Constructs a floating point constant.

• since Oxygen-20120901

True if the given expression is a (possibly cast'ed) character or an integer constant

True if the expression is a compile-time constant. is_varinfo_cst indicates whether a variable should be considered as having a constant content. Defaults to false.

• before 28.0-Nickel

  is_varinfo_cst does not exist

True if the expression is a compile-time integer constant

• before 28.0-Nickel

  is_varinfo_cst does not exist

True if the given offset contains only field names or constant indices.

• before 28.0-Nickel

  is_varinfo_cst does not exist

True if the given expression is a (possibly cast'ed) integer or character constant with value zero

True if the given expression is a null pointer, i.e. 0, (void * )0, which are the two null pointer constants in the standard, or the cast of a null pointer (constant or not) into a pointer type.

• since 28.0-Nickel

True if the term is the constant 0

True if the given term is \null or a constant null pointer

no_op_coerce typ term is true iff converting term to typ does not modify its value.

• since 19.0-Potassium

gives the value of a wide char literal.

gives the value of a char literal.

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-extended c, IInt, None)

Do constant folding on an expression. If the first argument is true then will also compute compiler-dependent expressions such as sizeof. See also Cil.constFoldVisitor, which will run constFold on all expressions in a given AST node.

Do constant folding on the given expression, just as constFold would. The resulting integer value, if the const-folding was complete, is returned. The machdep optional parameter, which is set to true by default, forces the simplification of architecture-dependent expressions.

Do constant folding on an term at toplevel only. This uses compiler-dependent informations and will remove all sizeof and alignof.

Do constant folding on an term.

• before 29.0-Copper

  takes a boolean machdep to decide if we actually do the fold or not.

Do constant folding on a Cil_types.offset. If the second argument is true then will also compute compiler-dependent expressions such as sizeof.

Do constant folding on a binary operation. The bulk of the work done by constFold is done here. If the second argument is true then will also compute compiler-dependent expressions such as sizeof.

true if the two constant are equal.

• since Nitrogen-20111001

true if two kinds have the same size independently of the machine.

true if the result of two expressions are two equal integers.

Increment an expression. Can be arithmetic or pointer type

Increment an expression. Can be arithmetic or pointer type

Makes an lvalue out of a given variable

Creates an expr representing the variable.

• since Nitrogen-20111001

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 "& v0"

Creates an expression corresponding to "&v".

• since Oxygen-20120901

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.

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

makes a binary operation and performs const folding. Inserts casts between arithmetic types as needed, or between pointer types, but do not attempt to cast pointer to int or vice-versa. Use appropriate binop (PlusPI & friends) for that.

same as mkBinOp, but performs a systematic cast (unless one of the arguments is 0) of pointers into uintptr_t during comparisons, making such operation defined even if the pointers do not share the same base. This was the behavior of mkBinOp prior to the introduction of this function.

• since Chlorine-20180501

Equivalent to mkMem for terms.

Make an expression that is a string constant (of pointer type)

true if both types are not equivalent. if force is true, returns true whenever both types are not equal (modulo typedefs). If force is false (the default), other equivalences are considered, in particular between an enum and its representative integer type.

typeForInsertedCast expr original_type destination_type returns the type into which expr, which has type original_type and whose type must be converted into destination_type, must be casted.

By default, returns destination_type.

This applies only to implicit casts. Casts already present in the source code are exempt from this hook.

• since 28.0-Nickel

checkCast context fromsource nullptr_cast oldt newt emits a warning or an error if the cast from oldt to newt is invalid (does nothing otherwise). nullptr_cast is true iff the expression being casted is a null pointer. Default is false. fromsource is false (default) if the cast is not present in the source code. Check areCompatibleTypes documentation for context.

Suspicious cases that only emit a warning:

• Implicit cast from a pointer to an integer.
• Cast from a pointer to a function type to another pointer to a function type when the function types are not compatible.
• Cast from an array to a pointer/array when types are not compatible.
• Cast, in both directions, between pointer to an object type and pointer to a function type.

• since 28.0-Nickel

Generic version of Cil.mkCastT. Construct a cast when having the old type of the expression. fromsource is false (default) if the cast is not present in the source code. If check is true (default), we check that the cast is valid, emitting an error or warning if the cast is invalid. If the new type is the same as the old type, then no cast is added, unless force is true (default is false). Cast from oldt to newt, returning the new type and the new expression.

• since 28.0-Nickel

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, unless force is true (default is false). Emit an error or warning if check is true and the cast is invalid.

• before 23.0-Vanadium

  different order of arguments.

• before 28.0-Nickel

  no check argument, it was always false.

Like Cil.mkCastT, but uses typeOf to get oldt.

• before 23.0-Vanadium

  different order of arguments.

• before 28.0-Nickel

  no check argument, it was always false.

Equivalent to stripCasts for terms.

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.

Compute the type of an expression.

Returns the type pointed by the given type. Asserts it is a pointer type.

Returns the type of the array elements of the given type. Asserts it is an array type.

Returns the type of the array elements of the given type, and the size of the array, if any. Asserts it is an array type.

• since 30.0-Zinc

Returns true whenever the type contains only arithmetic types

Convert a string representing a C integer literal to an Integer. Handles the prefixes 0x and 0 and the suffixes L, U, UL, LL, ULL.

Like parseInt, but returns Error message in case of failure, instead of aborting Frama-C.

• since 24.0-Chromium

Like parseInt, but converts to an expression.

Like parseIntExp, but returns Error message in case of failure, instead of aborting Frama-C.

• since 24.0-Chromium

Like parseInt, but converts to a logic term.

• returns

  true if the given variable appears in the expression.

Construct a statement, given its kind. Initialize the sid field to -1 if valid_sid is false (the default), or to a valid sid if valid_sid is true, and labels, succs and preds to the empty list

Construct a block with no attributes, given a list of statements

Construct a non-scoping block, i.e. a block that is not used to determine the end of scope of local variables. Hence, the blocals of such a block must always be empty.

• since Phosphorus-20170501-beta1

Construct a block with no attributes, given a list of statements and wrap it into the Cfg.

Construct a statement consisting of just one instruction See Cil.mkStmt for the signification of the optional args.

Returns an empty statement (of kind Instr). See mkStmt for ghost and valid_sid arguments.

A instr to serve as a placeholder

A statement consisting of just dummyInstr.

• see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

Create an instruction equivalent to a pure expression. The new instruction corresponds to the initialization of a new fresh variable, i.e. int tmp = exp. The scope of this fresh variable is determined by the block given in argument, that is the instruction must be placed directly (modulo non-scoping blocks) inside this block.

Create an instruction as above, enclosed in a block of a single (Instr) statement, which will be the scope of the fresh variable holding the value of the expression.

See Cil.mkStmt for information about ghost and valid_sid, and Cil.mkPureExprInstr for information about loc.

Make a loop. Can contain Break or Continue. The kind of loop (while, for, dowhile) is given by sattr (none by default). Use Cil.mkWhile for a While loop.

• before 23.0-Vanadium

  no unit argument, and default type was While (for while loops, there is now Cil.mkWhile).

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

• before 23.0-Vanadium

  did not have unit argument.

Make a for loop for(start; guard; next) { ... }. The body can contain Break but not Continue !!!

• before 23.0-Vanadium

  did not have unit argument.

Make a while loop.

• since 23.0-Vanadium

Make a do ... while loop.

• since 23.0-Vanadium

creates a block with empty attributes from an unspecified sequence.

treat_constructor_as_func action v f args kind loc calls action with the parameters corresponding to the call to f, of kind kind, initializing v with arguments args.

• since Phosphorus-20170501-beta1

find_def_stmt b v returns the Local_init instruction within b that initializes v. v must have its vdefined field set to true, and be among b.blocals.

• raises Fatal

  error if v is not a local variable of b with an initializer.

• since Phosphorus-20170501-beta1

returns true iff the given non-scoping block contains local init statements (thus of locals belonging to an outer block), either directly or within a non-scoping block or undefined sequence.labels

• since Phosphorus-20170501-beta1

returns true iff the given block is a ghost else block.

• since 21.0-Scandium

returns false if the given instruction is a call to a function with a "noreturn" attribute, and true otherwise.

• since 30.0-Zinc

Various classes of attributes

• before 30.0-Zinc

  AttrStmt and AttrIgnored didn't exist

Add a new attribute with a specified class

Remove an attribute previously registered.

isKnownAttribute attrname returns true if the attribute named attrname is known by Frama-C.

• since 30.0-Zinc

Return the class of an attributes. The class `default' is returned for unknown and ignored attributes.

• before 30.0-Zinc

  no default argument

Partition the attributes into classes: name attributes, function type and type attributes. Unknown and ignored attributes are returned in the `default` attribute class.

• before 30.0-Zinc

  no default argument

Add an attribute. Maintains the attributes in sorted order of the second argument. The attribute is not added if it is already there.

Add a list of attributes. Maintains the attributes in sorted order. The second argument must be sorted, but not necessarily the first

Remove all attributes with the given name. Maintains the attributes in sorted order.

Remove all attributes with names appearing in the string list. Maintains the attributes in sorted order

A block marked with this attribute is known to be a ghost else.

• since 21.0-Scandium

A varinfo marked with this attribute is known to be a ghost formal.

• since 20.0-Calcium

a formal marked with this attribute is known to be a pointer to an object being initialized by the current function, which can thus assign any sub-object regardless of const status.

• since 18.0-Argon

a field struct marked with this attribute is known to be mutable, i.e. it can be modified even on a const object.

• since 18.0-Argon

A block marked with this attribute is known to be inlined, i.e. it replaces a call to an inline function.

true if the underlying left-value of the given expression is allowed to be assigned to thanks to a frama_c_init_obj attribute.

true if the given lval is allowed to be assigned to thanks to a frama_c_init_obj or a frama_c_mutable attribute.

true if the given varinfo is a ghost formal variable.

• since 20.0-Calcium

true if the given formal declaration corresponds to a ghost formal variable.

• since 20.0-Calcium

true iff the given variable is a const global variable with non extern storage.

• since 25.0-Manganese

Remove any attribute appearing somewhere in the fully expanded version of the type.

• since Oxygen-20120901

Retains attributes with the given name

True if the named attribute appears in the attribute list. The list of attributes must be sorted.

Returns the name of an attribute.

Returns the list of parameters associated to an attribute. The list is empty if there is no such attribute or it has no parameters at all.

Returns all the attributes contained in a type. This requires a traversal of the type structure, in case of composite, enumeration and named types

Returns the attributes of a type.

Sets the attributes of the type to the given list. Previous attributes are discarded.

Add some attributes to a type. combine explains how to combine attributes. Default is addAttributes.

• before 28.0-Nickel

  combine does not exist

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 (unfolding the type definition when needed). It only removes attributes of topmost type, i.e. does not recurse under pointers, arrays, ...

same as above, but remove any existing attribute from the type.

• since Magnesium-20151001

Same as typeRemoveAttributes, but recursively removes the given attributes from inner types as well. Mainly useful to check whether two types are equal modulo some attributes. See also typeDeepDropAllAttributes, which will strip every single attribute from a type.

Does the type have the given attribute. Does not recurse through pointer types, nor inside function prototypes.

• since Sodium-20150201

Does the type have the given qualifier. Handles the case of arrays, for which the qualifiers are actually carried by the type of the elements. It is always correct to call this function instead of typeHasAttribute. For l-values, both functions return the same results, as l-values cannot have array type.

• since Sodium-20150201

typeHasAttributeMemoryBlock attr t is true iff at least one component of an object of type t has attribute attr. In other words, it searches for attr under aggregates, but not under pointers.

• since Chlorine-20180501 replaces typeHasAttributeDeep (name too ambiguous)

Remove all attributes relative to const, volatile and restrict attributes

• since Nitrogen-20111001

remove also qualifiers under Ptr and Arrays

• since Sodium-20150201

Remove all attributes relative to const, volatile and restrict attributes when building a C cast

• since Oxygen-20120901

Remove all attributes relative to const, volatile and restrict attributes when building a logic cast

• since Oxygen-20120901

retains attributes corresponding to type qualifiers (6.7.3)

given some attributes on an array type, split them into those that belong to the type of the elements of the array (currently, qualifiers such as const and volatile), and those that must remain on the array, in that order

• since Oxygen-20120901

Name of the attribute that is automatically inserted (with an AINT size argument when querying the type of a field that is a bitfield

Name of the attribute that is inserted when generating a name for a varinfo representing an anonymous function parameter.

• since 24.0-Chromium

attribute identifying anonymous function parameters

• since 24.0-Chromium

Convert an expression into an attrparam, if possible. Otherwise raise NotAnAttrParam with the offending subexpression

Return the attributes of the global annotation, if any.

• since 20.0-Calcium

Return the attributes of the global, if any.

• since 20.0-Calcium

Whether the given attributes contain libc indicators.

• since 23.0-Vanadium

Whether the given global contains libc indicators.

• since 23.0-Vanadium

Check for "const" qualifier from the type of an l-value (do not follow pointer)

• returns

  true iff a part of the related l-value has "const" qualifier

• since Chlorine-20180501

Check for "volatile" qualifier from the type of an l-value (do not follow pointer)

• returns

  true iff a part of the related l-value has "volatile" qualifier

• since Sulfur-20171101

Check for "volatile" qualifier from a logic type

• since Sulfur-20171101

Check if the l-value has a volatile part

• since Sulfur-20171101

Check if the l-value has a volatile part

• since Sulfur-20171101

Check for "ghost" qualifier from the type of an l-value (do not follow pointer)

• returns

  true iff a part of the related l-value has "ghost" qualifier

• since 21.0-Scandium

Check if the received type is well-formed according to \ghost semantics, that is once the type is not ghost anymore, \ghost cannot appear again.

• returns

  true iff the type is well formed

• since 21.0-Scandium

Add the ghost attribute to a type (does nothing if the type is alreay ghost)

• returns

  the ghost qualified original type

• since 26.0-Iron

Different visiting actions. 'a will be instantiated with exp, instr, etc.

• see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

returns a dummy behavior with the default name Cil.default_behavior_name. invariant: b_assumes must always be empty for behavior named Cil.default_behavior_name

• since Carbon-20101201

• since Carbon-20101201

• since Carbon-20101201

• since Carbon-20101201

A visitor interface for traversing CIL trees. Create instantiations of this type by specializing the class nopCilVisitor. Each of the specialized visiting functions can also call the queueInstr to specify that some instructions should be inserted before the current statement. Use syntax like self#queueInstr to call a method associated with the current object.

generic visitor, parameterized by its copying behavior. Traverses the CIL tree without modifying anything

Default in place visitor doing nothing and operating on current project.

doVisit vis deepCopyVisitor copy action children node visits a node (or its copy according to the result of copy) and if needed its children. Do not use it if you don't understand Cil visitor mechanism

• parameter vis

  the visitor performing the needed transformations. The open type allows for extensions to Cil to be visited by the same mechanisms.

• parameter deepCopyVisitor

  a generator for a visitor of the same type of the current one that performs a deep copy of the AST. Needed when the visitAction is SkipChildren or ChangeTo and vis is a copy visitor (we need to finish the copy anyway)

• parameter copy

  function that may return a copy of the actual node.

• parameter action

  the visiting function for the current node

• parameter children

  what to do on the children of the current node

• parameter node

  the current node

same as above, but can return a list of nodes

Visit a file. This 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.

• see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

Same thing, but the result is ignored. The given visitor must thus be an inplace visitor. Nothing is done if the visitor is a copy visitor.

• see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

A visitor for the whole file that does not *physically* change the globals (but maybe changes things inside the globals through side-effects). Use this function instead of Cil.visitCilFile whenever appropriate because it is more efficient for long files.

• see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

Same as Cil.visitCilFileSameGlobals, but only visits function definitions (i.e. behaves as if all globals but GFun return SkipChildren).

• since 25.0-Manganese

Visit a global

Visit a function definition

Visit an lvalue

Visit an lvalue or recursive offset

Visit an initializer offset

Visit a local initializer (with the local being initialized).

Visit an instruction

Visit a statement

Visit a block

Mark the given block as candidate to be flattened into its parent block, after returning from its visit. This is not systematic, as the environment might prevent it (e.g. if the preceding statement is a statement contract or if there are labels involved). Use that whenever you're creating a block in order to hold multiple statements as a result of visiting a single statement. If the block contains local variables, it will not be marked as transient, since removing it will change the scope of those variables.

• raises Fatal

  error if the given block attempts to declare local variables and contain definitions of local variables that are not part of the block.

• since Phosphorus-20170501-beta1

tells whether the block has been marked as transient

• since Phosphorus-20170501-beta1.

flatten_transient_sub_blocks b flattens all direct sub-blocks of b that have been marked as cleanable, whenever possible

• since Phosphorus-20170501-beta1

Visit a type

Visit a variable declaration

Visit an initializer, pass also the global to which this belongs and the offset.

Visit a list of attributes

• since Oxygen-20120901

• since Oxygen-20120901

• since Oxygen-20120901

visit an extended clause of a behavior.

• since Nitrogen-20111001

visit identified_term.

• since Oxygen-20120901

visit term_lval.

• since Nitrogen-20111001

A visitor that does constant folding. Pass as argument whether you want machine specific simplifications to be done, or not.

Pretty-print (Current_loc.get ())

• returns

  a dummy specification

• returns

  true if the given spec is empty.

• returns

  true if the given behavior is empty.

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 confusion. Or, viceversa, you might have added a local with a name that conflicts with a global

A peephole optimizer that processes two adjacent statements and possibly replaces them both. If some replacement happens and aggressive is true, then the new statements are themselves subject to optimization. Each statement in the list is optimized independently.

Similar to peepHole2 except that the optimization window consists of one statement, not two

Raised when one of the SizeOf/AlignOf 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

Give the unsigned kind corresponding to any integer kind

The signed integer kind for a given size (unsigned if second argument is true). Raises Not_found if no such kind exists

The float kind for a given size. Raises Not_found if no such kind exists

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 Machine.init. Remember that on GCC sizeof(void) is 1!

The size of a type, in bytes. Raises Cil.SizeOfError when it cannot compute the size.

Returns the number of bytes (resp. bits) to represent the given integer kind depending on the current machdep.

Returns the signedness of the given integer kind depending on the current machdep.

Returns the size of the given type, in bits. If this is the type of an lvalue which is a bitfield, the size of the bitfield is returned.

Cache for sizeof

Returns a unique number representing the integer conversion rank.

intTypeIncluded i1 i2 returns true iff the range of values representable in i1 is included in the one of i2

Returns a unique number representing the floating-point conversion rank.

• since Oxygen-20120901

Represents an integer as for a given kind. Returns a flag saying whether the value was changed during truncation (because it was too large to fit in k).

Returns the maximal value representable in a signed integer type of the given size (in bits)

Returns the smallest value representable in a signed integer type of the given size (in bits)

Returns the maximal value representable in a unsigned integer type of the given size (in bits)

True if the integer fits within the kind's range

True if the float is finite for the kind's range

True if the real constant is an exact float for the given type

raised by intKindForValue.

• returns

  the smallest kind that will hold the integer's value. The kind will be unsigned if the 2nd argument is true.

• raises Not_representable

  if the bigint is not representable.

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 Machine.init.

The minimum alignment (in bytes) for a type. This function is architecture dependent, so you should only call this after you call Machine.init.

• raises {!SizeOfError}

  when it cannot compute the alignment.

intOfAttrparam a tries to const-fold a into a numeric value. Returns Some n if it succeeds, None otherwise.

• since Silicium-20161101

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 Machine.init.

Give a field, returns the number of bits from the structure or union containing the field and the width (also expressed in bits) for the subobject denoted by the field. Raises Cil.SizeOfError when it cannot compute the size. This function is architecture dependent, so you should only call this after you call Machine.init.

Like map but try not to make a copy of the list

• deprecated

  30.0-Zinc

same as mapNoCopy for options

• deprecated

  30.0-Zinc

Like map but each call can return a list. Try not to make a copy of the list

• deprecated

  30.0-Zinc

if the list has 2 elements or more, it will return a block with bscoping=false

Convert a C variable into the corresponding logic variable. The returned logic variable is unique for a given C variable.

Convert a C variable into a logic term.

• since 24.0-Chromium

Make a temporary variable to use in annotations

The constant logic term zero.

• see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

The constant logic term 1.

The constant logic term -1.

The given constant logic term

Bind all free variables with an universal quantifier

extract varinfo elements from an exp

extract varinfo elements from an lval

extract logic_var elements from a term

extract logic_var elements from a predicate

extract logic_label elements from a code_annotation

extract logic_label elements from a term

extract logic_label elements from a pred

extract stmt elements from logic_label elements

creates a visitor that will replace in place uses of var in the first list by their counterpart in the second list.

• raises Invalid_argument

  if the lists have different lengths.

Provided s is a switch, separate_switch_succs s returns the subset of s.succs that correspond to the Case labels of s, and a "default statement" that either corresponds to the Default label, or to the syntactic successor of s if there is no default label. Note that this "default statement" can thus appear in the returned list.

Provided s is a if, separate_if_succs s splits the successors of s according to the truth value of the condition. The first element of the pair is the successor statement if the condition is true, and the second if the condition is false.