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