Frama-C API - Logic_const
Smart constructors for logic annotations.
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 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
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.
val new_predicate : ?kind:Cil_types.predicate_kind -> Cil_types.predicate -> Cil_types.identified_predicate
creates a new identified predicate with a fresh id.
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.
val refresh_predicate : Cil_types.identified_predicate -> Cil_types.identified_predicate
Gives a new id to an existing predicate.
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.
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
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.
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.
val is_unrollable_ltdef : Cil_types.logic_type_info -> bool
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
.
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>.
val make_type_list_of : Cil_types.logic_type -> Cil_types.logic_type
make_type_list_of t
returns the type list<t
>.
val type_of_list_elem : Cil_types.logic_type -> Cil_types.logic_type
returns the type of elements of a list type.
val is_set_type : Cil_types.logic_type -> bool
returns true
if the type is a set<t>.
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.
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
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.
val is_boolean_type : Cil_types.logic_type -> bool
val boolean_type : Cil_types.logic_type
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
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
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)
Logic Offsets
val lastTermOffset : Cil_types.term_offset -> Cil_types.term_offset
Equivalent to lastOffset
for terms.
val addTermOffset : Cil_types.term_offset -> Cil_types.term_offset -> Cil_types.term_offset
Equivalent to addOffset
for terms.
val addTermOffsetLval : Cil_types.term_offset -> Cil_types.term_lval -> Cil_types.term_lval
Equivalent to addOffsetLval
for terms.