Frama-C:
Plug-ins:
Libraries:

Frama-C API - Logic_const

Smart constructors for logic annotations.

Nodes with a unique ID

creates a code annotation with a fresh id.

val fresh_code_annotation : unit -> int
  • returns

    a fresh id for a code annotation.

val refresh_code_annotation : Cil_types.code_annotation -> Cil_types.code_annotation

set a fresh id to an existing code annotation

val refresh_spec : Cil_types.funspec -> Cil_types.funspec

set fresh id to properties of an existing funspec

  • since Sodium-20150201

creates a new toplevel predicate. predicate_kind is Assert by default. It can be set to:

  • Check for a predicate that should only be used to check a property, without adding it as hypothesis for the rest of the verification.
  • Admit for a predicate that is an hypothesis for the rest of the verification and should not be checked by Frama-C.

See Cil_types.toplevel_predicate for more information.

  • since 22.0-Titanium

creates a new identified predicate with a fresh id.

  • before 22.0-Titanium

    no only_check parameter.

  • before 23.0-Vanadium

    kind parameter was named only_check.

val new_acsl_extension : plugin:string -> string -> Cil_types.location -> bool -> Cil_types.acsl_extension_kind -> Cil_types.acsl_extension

creates a new acsl_extension with a fresh id.

  • since Chlorine-20180501
  • before the

    function took one less argument, ~plugin which is now used to set the ext_plugin field.

Gives a new id to an existing predicate.

  • since Oxygen-20120901
val fresh_predicate_id : unit -> int
  • returns

    a fresh id for predicates

extract a named predicate for an identified predicate.

val new_identified_term : Cil_types.term -> Cil_types.identified_term

creates a new identified term with a fresh id

val refresh_identified_term : Cil_types.identified_term -> Cil_types.identified_term

Gives a new id to an existing term.

  • since Oxygen-20120901
val fresh_term_id : unit -> int
  • returns

    a fresh id from an identified term

Logic labels

val pre_label : Cil_types.logic_label
val post_label : Cil_types.logic_label
val here_label : Cil_types.logic_label
val old_label : Cil_types.logic_label
val loop_current_label : Cil_types.logic_label
val loop_entry_label : Cil_types.logic_label
val init_label : Cil_types.logic_label
  • since Sodium-20150201

Predicates

makes a predicate with no name. Default location is unknown.

\true

val pfalse : Cil_types.predicate

\false

\old

application of predicate

&&

||

^^

!

Folds && over a list of predicates.

Folds || over a list of predicates.

local binding

==>

? :

<==>

Binary relation.

\forall

\exists

\fresh(pt,size)

\allocable

\freeable

\valid_read

\valid

\object_pointer

val pvalid_function : ?loc:Cil_types.location -> Cil_types.term -> Cil_types.predicate

\valid_function

\initialized

\dangling

\aligned

\at

\valid_index: requires index having integer type or set of integers

\valid_range: requires bounds having integer type

val pseparated : ?loc:Cil_types.location -> Cil_types.term list -> Cil_types.predicate

\separated

Logic types

val instantiate : (string * Cil_types.logic_type) list -> Cil_types.logic_type -> Cil_types.logic_type

instantiate type variables in a logic type.

  • since 18.0-Argon moved from Logic_utils
val is_unrollable_ltdef : Cil_types.logic_type_info -> bool
  • returns

    true if the logic type definition can be expanded.

  • since 18.0-Argon

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

  • since 18.0-Argon
val isLogicCType : (Cil_types.typ -> bool) -> Cil_types.logic_type -> bool

isLogicType test typ is false for pure logic types and the result of test for C types.

val is_list_type : Cil_types.logic_type -> bool

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

  • since Aluminium-20160501
val make_type_list_of : Cil_types.logic_type -> Cil_types.logic_type

make_type_list_of t returns the type list<t>.

  • since Aluminium-20160501
val type_of_list_elem : Cil_types.logic_type -> Cil_types.logic_type

returns the type of elements of a list type.

  • raises Failure

    if the input type is not a list type.

  • since Aluminium-20160501
val is_set_type : Cil_types.logic_type -> bool

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

  • since Neon-20140301

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

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

returns the type of elements of a set type.

  • raises Failure

    if the input type is not a set type.

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.

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

  • since Nitrogen-20111001
val is_plain_type : Cil_types.logic_type -> bool

true if the argument is not a set type.

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

  • since 25.0-Manganese
val is_boolean_type : Cil_types.logic_type -> bool
  • returns

    true if the argument is the boolean type.

Logic Terms

returns a anonymous term of the given type.

val trange : ?loc:Cil_datatype.Location.t -> (Cil_types.term option * Cil_types.term option) -> Cil_types.term

.. of integers

val tboolean : ?loc:Cil_datatype.Location.t -> bool -> Cil_types.term

boolean constant

  • since 30.0-Zinc
val tinteger : ?loc:Cil_datatype.Location.t -> int -> Cil_types.term

integer constant

val tinteger_s64 : ?loc:Cil_datatype.Location.t -> int64 -> Cil_types.term

integer constant

integer constant

  • since Oxygen-20120901
val treal : ?loc:Cil_datatype.Location.t -> float -> Cil_types.term

real constant

val treal_zero : ?loc:Cil_datatype.Location.t -> ?ltyp:Cil_types.logic_type -> unit -> Cil_types.term

real zero

val tstring : ?loc:Cil_datatype.Location.t -> string -> Cil_types.term

string constant

\at

\old

  • since Nitrogen-20111001

variable

\result

cast to the given C type

coercion to the given logic type

alignof(t)

val is_result : Cil_types.term -> bool

true if the term is \result (potentially enclosed in \at)

val is_exit_status : Cil_types.term -> bool

true if the term is \exit_status (potentially enclosed in \at)

  • since Nitrogen-20111001

Logic Offsets

Equivalent to lastOffset for terms.

  • since Oxygen-20120901

Equivalent to addOffset for terms.

  • since Oxygen-20120901

Equivalent to addOffsetLval for terms.

  • since Oxygen-20120901

Deprecated definitions

makes a predicate with no name. Default location is unknown.

  • deprecated Use unnamed instead.