package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 : 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

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

\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 Logic_utils.unroll_type.

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

val boolean_type : Cil_types.logic_type
  • since Sodium-20150201

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

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct