package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.1-Nickel.tar.gz

sha256=0220bc743b7da2468ceb926f331edc7ddfaa7c603ba47962de3e33c8e1e3f593

doc/frama-c.kernel/Frama_c_kernel/Logic_const/index.html

Module `Frama_c_kernel.Logic_const`

Smart constructors for logic annotations.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in 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.

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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

since Chlorine-20180501

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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in 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

returns
true if the logic type definition can be expanded.

since 18.0-Argon

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

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

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 (i.e. we do not build set of sets that way).

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.

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.

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

val is_plain_type : Cil_types.logic_type -> bool

true if the argument is not a set type.

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.

val boolean_type : Cil_types.logic_type

since Sodium-20150201

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

On This Page

Nodes with a unique ID
Logic labels
Predicates
Logic types
Logic Terms
Logic Offsets

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c.kernel/Frama_c_kernel/Logic_const/index.html

Module Frama_c_kernel.Logic_const

Nodes with a unique ID

Logic labels

Predicates

Logic types

Logic Terms

Logic Offsets

Module `Frama_c_kernel.Logic_const`