Frama-C API - Ast_types
This file contains types related types/functions/values.
Type Attributes
val get_attributes : Cil_types.typ -> Cil_types.attributesReturns all the attributes contained in a type. This requires a traversal of the type structure, in case of composite, enumeration and named types
val add_attributes : ?push_qualifiers:bool -> Cil_types.attribute list -> Cil_types.typ -> Cil_types.typAdd some attributes to a type. push_qualifiers determines if type qualifiers are pushed to the elements type. It defaults to true and should not be set to false unless you known what you are doing. In Frama-C this is useful for formals (see C11 6.7.6.3#7), so push_qualifiers is turned off when typing array formals before they are changed into pointers.
val has_attribute : string -> Cil_types.typ -> boolDoes the type have the given attribute. Does not recurse through pointer types, nor inside function prototypes.
val has_qualifier : string -> Cil_types.typ -> boolDoes 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.
val has_attribute_memory_block : string -> Cil_types.typ -> boolhas_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.
val remove_attributes : string list -> Cil_types.typ -> Cil_types.typRemove 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, ...
val remove_all_attributes : Cil_types.typ -> Cil_types.typSame as remove_attributes, but remove any existing attribute from the type.
val remove_attributes_deep : string list -> Cil_types.typ -> Cil_types.typSame 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.
val remove_qualifiers : Cil_types.typ -> Cil_types.typRemove all attributes relative to const, volatile and restrict attributes.
val remove_qualifiers_deep : Cil_types.typ -> Cil_types.typRemove also qualifiers under Ptr and Arrays.
val remove_attributes_for_c_cast : Cil_types.typ -> Cil_types.typRemove all attributes relative to const, volatile and restrict attributes when building a C cast
val remove_attributes_for_logic_type : Cil_types.typ -> Cil_types.typRemove all attributes relative to const, volatile and restrict attributes when building a logic cast
Utils functions
val unroll : Cil_types.typ -> Cil_types.typUnroll 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.
val unroll_node : Cil_types.typ -> Cil_types.typ_nodeSame than unroll but discard the final type attributes and only return its node.
val unroll_skel : Cil_types.typ -> Cil_types.typ_nodeUnroll typedefs, discarding all intermediate attribute. To be used only when one is interested in the shape of the type
val unroll_deep : Cil_types.typ -> Cil_types.typUnroll all the TNamed in a type (even under type constructors such as TPtr, TFun or TArray. Does not unroll the types of fields in TComp types. Will collect all attributes
val unroll_deep_node : Cil_types.typ -> Cil_types.typ_nodeSame than unroll_deep but discard the final type attributes and only return its node.
val unroll_logic : ?unroll_typedef:bool -> Cil_types.logic_type -> Cil_types.logic_typeExpands 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.
Const Attribute
val is_const : Cil_types.typ -> boolCheck for "const" qualifier from the type of an l-value using has_attribute_memory_block.
Volatile Attribute
val is_volatile : Cil_types.typ -> boolCheck for "volatile" qualifier from the type of an l-value using has_attribute_memory_block.
Ghost Attribute
val add_ghost : Cil_types.typ -> Cil_types.typAdd the ghost attribute to a type (does nothing if the type is already ghost).
val is_ghost : Cil_types.typ -> boolCheck for "ghost" qualifier from the type of an l-value (do not follow pointer)
val is_wellformed_ghost : Cil_types.typ -> boolCheck if the received type is well-formed according to \ghost semantics, that is once the type is not ghost anymore, \ghost cannot appear again.
Type checkers
val is_void : Cil_types.typ -> boolis the given type "void"?
val is_void_ptr : Cil_types.typ -> boolis the given type "void *"?
val is_bool : Cil_types.typ -> boolTrue if the argument is _Bool.
val is_char : Cil_types.typ -> boolTrue if the argument is a plain character type (but neither signed char nor unsigned char).
val is_any_char : Cil_types.typ -> boolTrue if the argument is a character type (i.e. plain, signed or unsigned).
val is_char_ptr : Cil_types.typ -> boolTrue if the argument is a pointer to a plain character type (but neither signed char nor unsigned char).
val is_any_char_ptr : Cil_types.typ -> boolTrue if the argument is a pointer to a character type (i.e. plain, signed or unsigned).
val is_char_const_ptr : Cil_types.typ -> boolTrue if the argument is a pointer to a constant character type, e.g. a string literal.
val is_short : Cil_types.typ -> boolTrue if the argument is a short type (i.e. signed or unsigned).
val is_integral : Cil_types.typ -> boolTrue if the argument is an integral type (i.e. integer or enum).
val is_intptr_t : Cil_types.typ -> boolTrue if the argument is intptr_t (but _not_ its underlying integer type).
val is_uintptr_t : Cil_types.typ -> boolTrue if the argument is uintptr_t (but _not_ its underlying integer type).
val is_float : Cil_types.typ -> boolTrue if the argument is a floating point type.
val is_long_double : Cil_types.typ -> boolTrue if the argument is a long double type.
val is_arithmetic : Cil_types.typ -> boolTrue if the argument is an arithmetic type (i.e. integer, enum or floating point.
val is_ptr : Cil_types.typ -> boolTrue if the argument is a pointer type.
val is_integral_or_pointer : Cil_types.typ -> boolTrue if the argument is an integral or pointer type.
val is_array : Cil_types.typ -> boolTrue if the argument is an array type.
val is_unsized_array : Cil_types.typ -> boolTrue if the argument is an array type without size.
val is_sized_array : Cil_types.typ -> boolTrue if the argument is a sized array type.
val is_char_array : Cil_types.typ -> boolTrue if the argument is an array of a character type (i.e. plain, signed or unsigned).
val is_any_char_array : Cil_types.typ -> boolTrue if the argument is an array of a character type (i.e. plain, signed or unsigned).
val is_wchar_array : Cil_types.typ -> boolTrue if the argument is an array of wchar_t. Can only be used after Machdep has been set.
val is_fun : Cil_types.typ -> boolTrue if the argument is a function type.
val is_fun_ptr : Cil_types.typ -> boolTrue if the argument is a function pointer type.
val is_scalar : Cil_types.typ -> boolTrue if the argument is a scalar type (i.e. integral, enum, floating point or pointer.
val is_object : Cil_types.typ -> boolTrue if the argument is an object type (i.e. not a function type).
val is_struct : Cil_types.typ -> boolTrue if the argument is a struct.
val is_union : Cil_types.typ -> boolTrue if the argument is a union type.
val is_struct_or_union : Cil_types.typ -> boolTrue if the argument is a struct or union type.
val is_transparent_union : Cil_types.typ -> Cil_types.fieldinfo optionCheck if a type is a transparent union, and return the first field.
val is_variadic_list : Cil_types.typ -> boolTrue if the argument denotes the type of ... in a variadic function.
Type access
val direct_element_type : Cil_types.typ -> Cil_types.typReturns the type of the array elements of the given type.
val element_type : Cil_types.typ -> Cil_types.typReturns the elements type using direct_element_type, but if the resulting type is an array, recursively call element_type.
val direct_pointed_type : Cil_types.typ -> Cil_types.typReturns the type directly pointed by the given type.
val pointed_type : Cil_types.typ -> Cil_types.typReturns the pointed type using direct_pointed_type, but if the resulting type is an array, returns the element type instead using element_type
val array_elem_type_and_size : Cil_types.typ -> Cil_types.typ * Cil_types.exp optionReturns the type of the array elements of the given type, and the size of the array, if any.
Logic Type checkers
val is_logic_volatile : Cil_types.logic_type -> boolCheck for "volatile" qualifier from a logic type using is_volatile.
val is_logic_typetag : Cil_types.logic_type -> boolTrue if the argument is the type for reified C types.
val is_logic_boolean : Cil_types.logic_type -> boolTrue if the argument is a boolean type, either integral C type or mathematical boolean one.
val is_logic_pure_boolean : Cil_types.logic_type -> boolTrue if the argument is _Bool or boolean.
val is_logic_integral : Cil_types.logic_type -> boolTrue if the argument is an integral type (i.e. integer or enum), either C or mathematical one.
val is_logic_float : Cil_types.logic_type -> boolTrue if the argument is a floating point type.
val is_logic_real : Cil_types.logic_type -> boolTrue if the argument is the logic 'real' type.
val is_logic_real_or_float : Cil_types.logic_type -> boolTrue if the argument is a C floating point type or logic 'real' type.
val is_logic_arithmetic : Cil_types.logic_type -> boolTrue if the argument is a logic arithmetic type (i.e. integer, enum or floating point, either C or mathematical one.
val is_logic_fun : Cil_types.logic_type -> boolTrue if the argument is the logic function type. Expands the logic type definition if necessary.
val is_logic_fun_ptr : Cil_types.logic_type -> boolTrue if the argument is the logic function pointer type. Expands the logic type definition if necessary.
