Previous  Up  Next

Module Logic_const

module Logic_const: sig .. end
Smart contructors for logic annotations.
Consult the Plugin Development Guide for additional details.

Nodes with a unique ID


val new_code_annotation : (Cil_types.term, Cil_types.predicate Cil_types.named,
        Cil_types.identified_predicate, Cil_types.identified_term)
       Cil_types.code_annot -> 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 new_predicate : Cil_types.predicate Cil_types.named -> Cil_types.identified_predicate
creates a new identified predicate with a fresh id.
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 Cil_types.named
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 predicate
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 -> 'a -> 'a Cil_types.named
makes a predicate with no name. Default location is unknown.
val ptrue : Cil_types.predicate Cil_types.named
\true
val pfalse : Cil_types.predicate Cil_types.named
\false
val pold : ?loc:Cil_types.location ->
       Cil_types.predicate Cil_types.named -> Cil_types.predicate Cil_types.named
\old
val papp : ?loc:Cil_types.location ->
       Cil_types.logic_info * (Cil_types.logic_label * Cil_types.logic_label) list *
       Cil_types.term list -> Cil_types.predicate Cil_types.named
application of predicate
val pand : ?loc:Cil_types.location ->
       Cil_types.predicate Cil_types.named * Cil_types.predicate Cil_types.named ->
       Cil_types.predicate Cil_types.named
&&
val por : ?loc:Cil_types.location ->
       Cil_types.predicate Cil_types.named * Cil_types.predicate Cil_types.named ->
       Cil_types.predicate Cil_types.named
||
val pxor : ?loc:Cil_types.location ->
       Cil_types.predicate Cil_types.named * Cil_types.predicate Cil_types.named ->
       Cil_types.predicate Cil_types.named
^^

!

val pnot : ?loc:Cil_types.location ->
       Cil_types.predicate Cil_types.named -> Cil_types.predicate Cil_types.named
val pands : Cil_types.predicate Cil_types.named list ->
       Cil_types.predicate Cil_types.named
Folds && over a list of predicates.
val pors : Cil_types.predicate Cil_types.named list ->
       Cil_types.predicate Cil_types.named
Folds || over a list of predicates.
val plet : ?loc:Cil_types.location ->
       (Cil_types.logic_info * Cil_types.predicate Cil_types.named) Cil_types.named ->
       Cil_types.predicate Cil_types.named
local binding
val pimplies : ?loc:Cil_types.location ->
       Cil_types.predicate Cil_types.named * Cil_types.predicate Cil_types.named ->
       Cil_types.predicate Cil_types.named
==>
val pif : ?loc:Cil_types.location ->
       Cil_types.term * Cil_types.predicate Cil_types.named *
       Cil_types.predicate Cil_types.named -> Cil_types.predicate Cil_types.named
? :
val piff : ?loc:Cil_types.location ->
       Cil_types.predicate Cil_types.named * Cil_types.predicate Cil_types.named ->
       Cil_types.predicate Cil_types.named
<==>
val prel : ?loc:Cil_types.location ->
       Cil_types.relation * Cil_types.term * Cil_types.term ->
       Cil_types.predicate Cil_types.named
Binary relation.
Consult the Plugin Development Guide for additional details.
val pforall : ?loc:Cil_types.location ->
       Cil_types.quantifiers * Cil_types.predicate Cil_types.named ->
       Cil_types.predicate Cil_types.named
\forall
val pexists : ?loc:Cil_types.location ->
       Cil_types.quantifiers * Cil_types.predicate Cil_types.named ->
       Cil_types.predicate Cil_types.named
\exists
val pfresh : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.logic_label * Cil_types.term *
       Cil_types.term -> Cil_types.predicate Cil_types.named
\fresh(pt,size)
val pallocable : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term -> Cil_types.predicate Cil_types.named
\allocable
val pfreeable : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term -> Cil_types.predicate Cil_types.named
\freeable
val pvalid_read : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term -> Cil_types.predicate Cil_types.named
\valid_read
val pvalid : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term -> Cil_types.predicate Cil_types.named
\valid
val pvalid_function : ?loc:Cil_types.location ->
       Cil_types.term -> Cil_types.predicate Cil_types.named
\valid_function
val pinitialized : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term -> Cil_types.predicate Cil_types.named
\initialized
val pdangling : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term -> Cil_types.predicate Cil_types.named
\dangling
val pat : ?loc:Cil_types.location ->
       Cil_types.predicate Cil_types.named * Cil_types.logic_label ->
       Cil_types.predicate Cil_types.named
\at
val pvalid_index : ?loc:Cil_types.location ->
       Cil_types.logic_label * Cil_types.term * Cil_types.term ->
       Cil_types.predicate Cil_types.named
\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 Cil_types.named
\valid_range: requires bounds having integer type
val psubtype : ?loc:Cil_types.location ->
       Cil_types.term * Cil_types.term -> Cil_types.predicate Cil_types.named
subtype relation
val pseparated : ?loc:Cil_types.location ->
       Cil_types.term list -> Cil_types.predicate Cil_types.named
\separated

Logic types


val is_list_type : Cil_types.logic_type -> bool
returns true if the type is a set<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.
Since Aluminium-20160501
Raises Failure if the input type is not a list type.
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 ( 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 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 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 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