Frama-C API - Ast_types

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

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

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

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 has_attribute. For l-values, both functions return the same results, as l-values cannot have array type.

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

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 remove_attributes, but remove any existing attribute from the type.

Same as remove_attributes, 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 Cil.typeDeepDropAllAttributes, which will strip every single attribute from a type.

Remove all attributes relative to const, volatile and restrict attributes.

Remove also qualifiers under Ptr and Arrays.

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

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

Unroll a type until it exposes a non TNamed. Will collect all attributes appearing in TNamed and add them to the final type using add_attributes.

Same than unroll but discard the final type attributes and only return its node.

Unroll typedefs, discarding all intermediate attribute. To be used only when one is interested in the shape of the type

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

Same than unroll_deep but discard the final type attributes and only return its node.

Expands logic type definitions. If the unroll_typedef flag is set to true (this is the default), C typedef will be expanded as well using Logic_const.unroll_ltdef.

Check for "const" qualifier from the type of an l-value using has_attribute_memory_block.

Check for "volatile" qualifier from the type of an l-value using has_attribute_memory_block.

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

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

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.

is the given type "void"?

is the given type "void *"?

True if the argument is _Bool.

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

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

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 character type (i.e. plain, signed or unsigned).

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

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

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

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

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

True if the argument is a floating point type.

True if the argument is a long double type.

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

True if the argument is a pointer type.

True if the argument is an integral or pointer type.

True if the argument is an array type.

True if the argument is an array type without size.

True if the argument is a sized array type.

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

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

True if the argument is a function type.

True if the argument is a function pointer type.

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

True if the argument is an object type (i.e. not a function type).

True if the argument is a struct.

True if the argument is a union type.

True if the argument is a struct or union type.

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

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

Returns the type of the array elements of the given type.

• raises AbortFatal

  it is not an array type.

Returns the elements type using direct_element_type, but if the resulting type is an array, recursively call element_type.

Returns the type directly pointed by the given type.

• raises AbortFatal

  it is not a pointer type.

Returns the pointed type using direct_pointed_type, but if the resulting type is an array, returns the element type instead using element_type

Returns the type of the array elements of the given type, and the size of the array, if any.

• raises AbortFatal

  it is not an array type.

• before Frama-C+dev

  In Cil this function applied Cil.constFoldToInt on array's size and returned a Z.t option.

Check for "volatile" qualifier from a logic type using is_volatile.

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

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

True if the argument is _Bool or boolean.

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

True if the argument is a floating point type.

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

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

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 the logic function type. Expands the logic type definition if necessary.

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