sig
val string_of_typ : Cil_types.typ -> string
val ttype_of_pointed : Cil_types.logic_type -> Cil_types.logic_type
val ptr_of : Cil_types.typ -> Cil_types.typ
val const_of : Cil_types.typ -> Cil_types.typ
val size_t : unit -> Cil_types.typ
val prepare_definition : string -> Cil_types.typ -> Cil_types.fundec
val call_function :
Cil_types.lval option ->
Cil_types.varinfo -> Cil_types.exp list -> Cil_types.instr
val cvar_to_tvar : Cil_types.varinfo -> Cil_types.term
val tunref_range :
?loc:Cil_types.location ->
Cil_types.term -> Cil_types.term -> Cil_types.term
val tunref_range_bytes_len :
?loc:Cil_types.location ->
Cil_types.term -> Cil_types.term -> Cil_types.term
val tplus :
?loc:Cil_types.location ->
Cil_types.term -> Cil_types.term -> Cil_types.term
val tminus :
?loc:Cil_types.location ->
Cil_types.term -> Cil_types.term -> Cil_types.term
val tdivide :
?loc:Cil_types.location ->
Cil_types.term -> Cil_types.term -> Cil_types.term
val pbounds_incl_excl :
?loc:Cil_types.location ->
Cil_types.term -> Cil_types.term -> Cil_types.term -> Cil_types.predicate
val plet_len_div_size :
?loc:Cil_types.location ->
?name_ext:string ->
Cil_types.logic_type ->
Cil_types.term ->
(Cil_types.term -> Cil_types.predicate) -> Cil_types.predicate
val punfold_all_elems_eq :
?loc:Cil_types.location ->
Cil_types.term -> Cil_types.term -> Cil_types.term -> Cil_types.predicate
val punfold_all_elems_pred :
?loc:Cil_types.location ->
Cil_types.term ->
Cil_types.term ->
(?loc:Cil_types.location -> Cil_types.term -> Cil_types.predicate) ->
Cil_types.predicate
val punfold_flexible_struct_pred :
?loc:Cil_types.location ->
Cil_types.term ->
Cil_types.term ->
(?loc:Cil_types.location -> Cil_types.term -> Cil_types.predicate) ->
Cil_types.predicate
val pvalid_len_bytes :
?loc:Cil_types.location ->
Cil_types.logic_label ->
Cil_types.term -> Cil_types.term -> Cil_types.predicate
val pvalid_read_len_bytes :
?loc:Cil_types.location ->
Cil_types.logic_label ->
Cil_types.term -> Cil_types.term -> Cil_types.predicate
val pcorrect_len_bytes :
?loc:Cil_types.location ->
Cil_types.logic_type -> Cil_types.term -> Cil_types.predicate
val pseparated_memories :
?loc:Cil_types.location ->
Cil_types.term ->
Cil_types.term -> Cil_types.term -> Cil_types.term -> Cil_types.predicate
val make_behavior :
?name:string ->
?assumes:Cil_types.identified_predicate list ->
?requires:Cil_types.identified_predicate list ->
?ensures:(Cil_types.termination_kind * Cil_types.identified_predicate)
list ->
?assigns:Cil_types.assigns ->
?alloc:Cil_types.allocation ->
?extension:Cil_types.acsl_extension list -> unit -> Cil_types.behavior
val make_funspec :
Cil_types.behavior list ->
?termination:Cil_types.identified_predicate option ->
?complete_disjoint:string list list * string list list ->
unit -> Cil_types.funspec
end