Module Logic_const

module Logic_const: sig .. end

Smart constructors for logic annotations.

Consult the Plugin Development Guide

Nodes with a unique ID

val new_code_annotation : Cil_types.code_annotation_node -> Cil_types.code_annotation

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

val toplevel_predicate : ?kind:Cil_types.predicate_kind ->
       Cil_types.predicate -> Cil_types.toplevel_predicate

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

val new_predicate : ?kind:Cil_types.predicate_kind ->
       Cil_types.predicate -> Cil_types.identified_predicate

creates a new identified predicate with a fresh id.

Change in 22.0-Titanium

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

Consult the Plugin Development Guide

val refresh_predicate : Cil_types.identified_predicate -> Cil_types.identified_predicate

Gives a new id to an existing predicate.

Since Oxygen-20120901

val fresh_predicate_id : unit -> int

Returns a fresh id for predicates

val pred_of_id_pred : Cil_types.identified_predicate -> Cil_types.predicate

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

val unamed : ?loc:Cil_types.location -> Cil_types.predicate_node -> Cil_types.predicate

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

val ptrue : Cil_types.predicate

\true

val pfalse : Cil_types.predicate

\false

val pold : ?loc:Cil_types.location -> Cil_types.predicate -> Cil_types.predicate

\old

val papp : ?loc:Cil_types.location ->
       Cil_types.logic_info * Cil_types.logic_label list * Cil_types.term list ->
       Cil_types.predicate

application of predicate

val pand : ?loc:Cil_types.location ->
       Cil_types.predicate * Cil_types.predicate -> Cil_types.predicate

val por : ?loc:Cil_types.location ->
       Cil_types.predicate * Cil_types.predicate -> Cil_types.predicate

val pxor : ?loc:Cil_types.location ->
       Cil_types.predicate * Cil_types.predicate -> Cil_types.predicate

val pnot : ?loc:Cil_types.location -> Cil_types.predicate -> Cil_types.predicate

val pands : Cil_types.predicate list -> Cil_types.predicate

Folds && over a list of predicates.

val pors : Cil_types.predicate list -> Cil_types.predicate

Folds || over a list of predicates.

val plet : ?loc:Cil_types.location ->
       Cil_types.logic_info -> Cil_types.predicate -> Cil_types.predicate

local binding

val pimplies : ?loc:Cil_types.location ->
       Cil_types.predicate * Cil_types.predicate -> Cil_types.predicate

==>

val pif : ?loc:Cil_types.location ->
       Cil_types.term * Cil_types.predicate * Cil_types.predicate ->
       Cil_types.predicate

? :

val piff : ?loc:Cil_types.location ->
       Cil_types.predicate * Cil_types.predicate -> Cil_types.predicate

<==>

val prel : ?loc:Cil_types.location ->
       Cil_types.relation * Cil_types.term * Cil_types.term -> Cil_types.predicate

Binary relation.

Consult the Plugin Development Guide

val pforall : ?loc:Cil_types.location ->
       Cil_types.quantifiers * Cil_types.predicate -> Cil_types.predicate

\forall

val pexists : ?loc:Cil_types.location ->
       Cil_types.quantifiers * Cil_types.predicate -> Cil_types.predicate

\exists

val pfresh : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.logic_label * Cil_types.term *
       Cil_types.term -> Cil_types.predicate

\fresh(pt,size)

val pallocable : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term -> Cil_types.predicate

\allocable

val pfreeable : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term -> Cil_types.predicate

\freeable

val pvalid_read : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term -> Cil_types.predicate

\valid_read

val pvalid : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term -> Cil_types.predicate

\valid

val pobject_pointer : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term -> Cil_types.predicate

\object_pointer

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

\valid_function

val pinitialized : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term -> Cil_types.predicate

\initialized

val pdangling : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term -> Cil_types.predicate

\dangling

val pat : ?loc:Cil_types.location ->
       Cil_types.predicate * Cil_types.logic_label -> Cil_types.predicate

\at

val pvalid_index : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term * Cil_types.term ->
       Cil_types.predicate

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

val pvalid_range : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term * Cil_types.term * Cil_types.term ->
       Cil_types.predicate

\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

Since 18.0-Argon
Returns true if the logic type definition can be expanded.

val unroll_ltdef : Cil_types.logic_type -> Cil_types.logic_type

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

Change in 18.0-Argon

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.

Since Aluminium-20160501
Raises Failure if the input type is not a list type.

Change in 18.0-Argon

val is_set_type : Cil_types.logic_type -> bool

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

Since Neon-20140301

Change in 18.0-Argon

val set_conversion : Cil_types.logic_type -> Cil_types.logic_type -> Cil_types.logic_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 ( we do not build set of sets that way).

Change in 18.0-Argon

val make_set_type : Cil_types.logic_type -> Cil_types.logic_type

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

Change in 18.0-Argon

val type_of_element : Cil_types.logic_type -> Cil_types.logic_type

returns the type of elements of a set type.

Raises Failure if the input type is not a set type.

Change in 18.0-Argon

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.

Change in 18.0-Argon

val transform_element : (Cil_types.logic_type -> Cil_types.logic_type) ->
       Cil_types.logic_type -> Cil_types.logic_type

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

Since Nitrogen-20111001

Change in 18.0-Argon

val is_plain_type : Cil_types.logic_type -> bool

true if the argument is not a set type.

Change in 18.0-Argon

val make_arrow_type : Cil_types.logic_var list -> Cil_types.logic_type -> Cil_types.logic_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.

Change in 18.0-Argon

val boolean_type : Cil_types.logic_type

Since Sodium-20150201

Change in 18.0-Argon

Logic Terms

val term : ?loc:Cil_datatype.Location.t ->
       Cil_types.term_node -> Cil_types.logic_type -> Cil_types.term

returns a anonymous term of the given type.

val taddrof : ?loc:Cil_datatype.Location.t ->
       Cil_types.term_lval -> Cil_types.logic_type -> Cil_types.term

Deprecated.Neon-20130301 Logic_utils.mk_AddrOf is easier to use.

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

val tint : ?loc:Cil_datatype.Location.t -> Integer.t -> Cil_types.term

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

val tat : ?loc:Cil_datatype.Location.t ->
       Cil_types.term * Cil_types.logic_label -> Cil_types.term

\at

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

\old

Since Nitrogen-20111001

val tvar : ?loc:Cil_datatype.Location.t -> Cil_types.logic_var -> Cil_types.term

variable

val tresult : ?loc:Cil_datatype.Location.t -> Cil_types.typ -> Cil_types.term

\result

val tcast : ?loc:Cil_datatype.Location.t ->
       Cil_types.term -> Cil_types.typ -> Cil_types.term

cast to the given C type

val tlogic_coerce : ?loc:Cil_datatype.Location.t ->
       Cil_types.term -> Cil_types.logic_type -> Cil_types.term

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

val lastTermOffset : Cil_types.term_offset -> Cil_types.term_offset

Equivalent to lastOffset for terms.

Since Oxygen-20120901

val addTermOffset : Cil_types.term_offset -> Cil_types.term_offset -> Cil_types.term_offset

Equivalent to addOffset for terms.

Since Oxygen-20120901

val addTermOffsetLval : Cil_types.term_offset -> Cil_types.term_lval -> Cil_types.term_lval

Equivalent to addOffsetLval for terms.

Since Oxygen-20120901