sig
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
val make_type_list_of : Cil_types.logic_type -> Cil_types.logic_type
val type_of_list_elem : Cil_types.logic_type -> Cil_types.logic_type
val is_set_type : Cil_types.logic_type -> bool
val set_conversion :
Cil_types.logic_type -> Cil_types.logic_type -> Cil_types.logic_type
val make_set_type : Cil_types.logic_type -> Cil_types.logic_type
val type_of_element : Cil_types.logic_type -> Cil_types.logic_type
val plain_or_set :
(Cil_types.logic_type -> 'a) -> Cil_types.logic_type -> 'a
val transform_element :
(Cil_types.logic_type -> Cil_types.logic_type) ->
Cil_types.logic_type -> Cil_types.logic_type
val is_plain_type : Cil_types.logic_type -> bool
val 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
val trange :
?loc:Cil_datatype.Location.t ->
Cil_types.term option * Cil_types.term option -> Cil_types.term
val 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
val is_exit_status : Cil_types.term -> bool
val lastTermOffset : Cil_types.term_offset -> Cil_types.term_offset
val addTermOffset :
Cil_types.term_offset -> Cil_types.term_offset -> Cil_types.term_offset
val addTermOffsetLval :
Cil_types.term_offset -> Cil_types.term_lval -> Cil_types.term_lval
end