module Logic_const:sig
..end
val new_code_annotation : Cil_types.code_annotation_node -> Cil_types.code_annotation
val fresh_code_annotation : unit -> int
val refresh_code_annotation : Cil_types.code_annotation -> Cil_types.code_annotation
val refresh_spec : Cil_types.funspec -> Cil_types.funspec
val new_predicate : Cil_types.predicate -> Cil_types.identified_predicate
val refresh_predicate : Cil_types.identified_predicate -> Cil_types.identified_predicate
val fresh_predicate_id : unit -> int
val pred_of_id_pred : Cil_types.identified_predicate -> Cil_types.predicate
val new_identified_term : Cil_types.term -> Cil_types.identified_term
val refresh_identified_term : Cil_types.identified_term -> Cil_types.identified_term
val fresh_term_id : unit -> int
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
val unamed : ?loc:Cil_types.location -> Cil_types.predicate_node -> Cil_types.predicate
val ptrue : Cil_types.predicate
val pfalse : Cil_types.predicate
val pold : ?loc:Cil_types.location -> Cil_types.predicate -> Cil_types.predicate
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
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
val pors : Cil_types.predicate list -> Cil_types.predicate
val plet : ?loc:Cil_types.location ->
Cil_types.logic_info -> Cil_types.predicate -> Cil_types.predicate
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
val pforall : ?loc:Cil_types.location ->
Cil_types.quantifiers * Cil_types.predicate -> Cil_types.predicate
val pexists : ?loc:Cil_types.location ->
Cil_types.quantifiers * Cil_types.predicate -> Cil_types.predicate
val pfresh : ?loc:Cil_types.location ->
Cil_types.logic_label * Cil_types.logic_label * Cil_types.term *
Cil_types.term -> Cil_types.predicate
val pallocable : ?loc:Cil_types.location ->
Cil_types.logic_label * Cil_types.term -> Cil_types.predicate
val pfreeable : ?loc:Cil_types.location ->
Cil_types.logic_label * Cil_types.term -> Cil_types.predicate
val pvalid_read : ?loc:Cil_types.location ->
Cil_types.logic_label * Cil_types.term -> Cil_types.predicate
val pvalid : ?loc:Cil_types.location ->
Cil_types.logic_label * Cil_types.term -> Cil_types.predicate
val pvalid_function : ?loc:Cil_types.location -> Cil_types.term -> Cil_types.predicate
val pinitialized : ?loc:Cil_types.location ->
Cil_types.logic_label * Cil_types.term -> Cil_types.predicate
val pdangling : ?loc:Cil_types.location ->
Cil_types.logic_label * Cil_types.term -> Cil_types.predicate
val pat : ?loc:Cil_types.location ->
Cil_types.predicate * Cil_types.logic_label -> Cil_types.predicate
val pvalid_index : ?loc:Cil_types.location ->
Cil_types.logic_label * Cil_types.term * Cil_types.term ->
Cil_types.predicate
val pvalid_range : ?loc:Cil_types.location ->
Cil_types.logic_label * Cil_types.term * Cil_types.term * Cil_types.term ->
Cil_types.predicate
val psubtype : ?loc:Cil_types.location ->
Cil_types.term * Cil_types.term -> Cil_types.predicate
val pseparated : ?loc:Cil_types.location -> Cil_types.term list -> Cil_types.predicate
val is_list_type : Cil_types.logic_type -> bool
true
if the type is a set<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
Failure
if the input type is not a list type.val is_set_type : Cil_types.logic_type -> bool
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 ( we do not build set of sets that way).val make_set_type : Cil_types.logic_type -> Cil_types.logic_type
val type_of_element : Cil_types.logic_type -> Cil_types.logic_type
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 typeval 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 typeval is_boolean_type : Cil_types.logic_type -> bool
val boolean_type : Cil_types.logic_type
val term : ?loc:Cil_datatype.Location.t ->
Cil_types.term_node -> Cil_types.logic_type -> Cil_types.term
val taddrof : ?loc:Cil_datatype.Location.t ->
Cil_types.term_lval -> Cil_types.logic_type -> Cil_types.term
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 integersval tinteger : ?loc:Cil_datatype.Location.t -> int -> Cil_types.term
val tinteger_s64 : ?loc:Cil_datatype.Location.t -> int64 -> Cil_types.term
val tint : ?loc:Cil_datatype.Location.t -> Integer.t -> Cil_types.term
val treal : ?loc:Cil_datatype.Location.t -> float -> Cil_types.term
val treal_zero : ?loc:Cil_datatype.Location.t ->
?ltyp:Cil_types.logic_type -> unit -> Cil_types.term
val tstring : ?loc:Cil_datatype.Location.t -> string -> Cil_types.term
val tat : ?loc:Cil_datatype.Location.t ->
Cil_types.term * Cil_types.logic_label -> Cil_types.term
val told : ?loc:Cil_datatype.Location.t -> Cil_types.term -> Cil_types.term
val tvar : ?loc:Cil_datatype.Location.t -> Cil_types.logic_var -> Cil_types.term
val tresult : ?loc:Cil_datatype.Location.t -> Cil_types.typ -> Cil_types.term
val tlogic_coerce : ?loc:Cil_datatype.Location.t ->
Cil_types.term -> Cil_types.logic_type -> Cil_types.term
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)val lastTermOffset : Cil_types.term_offset -> Cil_types.term_offset
lastOffset
for terms.val addTermOffset : Cil_types.term_offset -> Cil_types.term_offset -> Cil_types.term_offset
addOffset
for terms.val addTermOffsetLval : Cil_types.term_offset -> Cil_types.term_lval -> Cil_types.term_lval
addOffsetLval
for terms.