Frama-C:
Plug-ins:
Libraries:

Frama-C API - Acsl

This module contains all functions related to logic types. Most of these functions where moved from Logic_const or Logic_utils and renamed for better consistency.

  • since Frama-C+dev
val instantiate : (string * Cil_types.logic_type) list -> Cil_types.logic_type -> Cil_types.logic_type

instantiate type variables in a logic type.

val is_unrollable_ltdef : Cil_types.logic_type_info -> bool
  • returns

    true if the logic type definition can be expanded.

expands logic type definitions only. To expands both logic part and C part, uses Ast_types.Acsl.unroll.

val unroll : ?unroll_typedef:bool -> Cil_types.logic_type -> Cil_types.logic_type

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 Ast_types.Acsl.unroll_ltdef.

tests and extraction of element type

val fold_plain_ctype : default:'a -> (Cil_types.typ -> 'a) -> Cil_types.logic_type -> 'a

fold_plain_ctype ~default f t is ~default for pure logic types and the result of f for C types.

val is_plain : Cil_types.logic_type -> bool

true if the argument is not a set type.

val is_plain_set : Cil_types.logic_type -> bool

returns true if the type is a set<t>.

val plain_or_set : (Cil_types.logic_type -> 'a) -> Cil_types.logic_type -> 'a

plain_or_set f t applies f to t or to the type of elements of t if it is a set type.

val plain_or_set_ctype : (Cil_types.typ -> bool) -> Cil_types.logic_type -> bool

plain_or_set_ctype test typ is false for pure logic types and the result of test for C types. In case of a set type, the function tests the element type.

val is_logic_boolean : Cil_types.logic_type -> bool
tests for direct type

is_plain_xxx t returns true iff t is a xxx (and not a set<xxx>. Uses Ast_types.Acsl.unroll_ltdef if needed.

val is_plain_volatile : Cil_types.logic_type -> bool

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

val is_plain_typetag : Cil_types.logic_type -> bool

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

val is_plain_boolean : Cil_types.logic_type -> bool

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

val is_plain_pure_boolean : Cil_types.logic_type -> bool

True if the argument is _Bool or Lboolean.

val is_plain_integral : Cil_types.logic_type -> bool

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

val is_plain_float : Cil_types.logic_type -> bool

True if the argument is a floating point type.

val is_plain_real : Cil_types.logic_type -> bool

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

val is_plain_real_or_float : Cil_types.logic_type -> bool

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

val is_plain_arithmetic : Cil_types.logic_type -> bool

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

val is_plain_ptr : Cil_types.logic_type -> bool

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

val is_plain_array : Cil_types.logic_type -> bool

True if the argument is an array type. Expands the logic type definition if necessary.

val is_plain_fun : Cil_types.logic_type -> bool

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

val is_plain_fun_ptr : Cil_types.logic_type -> bool

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

val is_plain_fun_or_ptr : Cil_types.logic_type -> bool

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

val is_plain_list : Cil_types.logic_type -> bool

Returns true if the type is a list<t>.

tests for potential sets

is_xxx t returns true iff t is a xxx _or_ a set of xxx

val is_arithmetic : Cil_types.logic_type -> bool
val is_integral : Cil_types.logic_type -> bool
val is_fun_ptr : Cil_types.logic_type -> bool
val is_array : Cil_types.logic_type -> bool
val is_ptr : Cil_types.logic_type -> bool
val is_char : Cil_types.logic_type -> bool
val is_any_char : Cil_types.logic_type -> bool
val is_void : Cil_types.logic_type -> bool
val is_void_ptr : Cil_types.logic_type -> bool
constructors

make_list t returns the type list<t>.

converts a type into the corresponding set type if needed. Does nothing if the argument is already a set type.

make_arrow args rt returns a rt if args is empty or the corresponding Larrow type.

set_conversion ty1 ty2 returns a set type as soon as ty1 and/or ty2 is a set. Elements have type ty1, or the type of the elements of ty1 if it is itself a set-type (i.e. we do not build set of sets that way).

transform_element f t is the same as set_conversion (plain_or_set f t) t

extract elements

returns the type of elements of a list type.

  • raises Failure

    if the input type is not a list type.

returns the type of elements of a set type.

  • raises Failure

    if the input type is not a set type.

returns the type of the element pointed to by the type. If the source type is a set of pointers, returns a set of elements.

val direct_array_element : Cil_types.logic_type -> Cil_types.logic_type

same as Ast_types.Acsl.direct_pointed but for arrays (or set of arrays).

Type conversions
  • returns

    the equivalent C type.

  • raises Failure

    if the type is purely logical

val remove_qualifiers : Cil_types.logic_type -> Cil_types.logic_type

removes qualifiers if logic_type is a C type, identity otherwise.

val direct_pointed_ctype : Cil_types.logic_type -> Cil_types.typ
val direct_array_element_ctype : Cil_types.logic_type -> Cil_types.typ