module Misc:sig
..end
Utilities for E-ACSL.
exception Unregistered_library_function of string
val get_lib_fun_vi : string -> Cil_types.varinfo
Return varinfo corresponding to a name of a given library function
val mk_call : loc:Cil_datatype.Location.t ->
?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
Call an E-ACSL library function or an E-ACSL built-in.
Unregistered_library_function
if the given string does not represent
such a function or if these functions were never registered (only possible
when using E-ACSL through its API.val mk_deref : loc:Cil_datatype.Location.t -> Cil_types.exp -> Cil_types.exp
Make a dereference of an expression
type
annotation_kind =
| |
Assertion |
| |
Precondition |
| |
Postcondition |
| |
Invariant |
| |
RTE |
val mk_e_acsl_guard : ?reverse:bool ->
annotation_kind ->
Cil_types.kernel_function ->
Cil_types.exp -> Cil_types.predicate -> Cil_types.stmt
val mk_block : Project.t -> Cil_types.stmt -> Cil_types.block -> Cil_types.stmt
val result_lhost : Cil_types.kernel_function -> Cil_types.lhost
val result_vi : Cil_types.kernel_function -> Cil_types.varinfo
val library_files : unit -> string list
val is_library_loc : Cil_types.location -> bool
val register_library_function : Cil_types.varinfo -> unit
val reset : unit -> unit
val mk_store_stmt : ?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
val mk_duplicate_store_stmt : ?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
val mk_delete_stmt : Cil_types.varinfo -> Cil_types.stmt
val mk_full_init_stmt : ?addr:bool -> Cil_types.varinfo -> Cil_types.stmt
val mk_initialize : loc:Cil_types.location -> Cil_types.lval -> Cil_types.stmt
val mk_mark_readonly : Cil_types.varinfo -> Cil_types.stmt
val term_addr_of : loc:Cil_types.location ->
Cil_types.term_lval -> Cil_types.typ -> Cil_types.term
val reorder_ast : unit -> unit
val cty : Cil_types.logic_type -> Cil_types.typ
Assume that the logic type is indeed a C type. Just return it.
val ptr_index : ?loc:Cil_types.location ->
?index:Cil_types.exp -> Cil_types.exp -> Cil_types.exp * Cil_types.exp
Split pointer-arithmetic expression of the type `p + i` into its pointer and integer parts.
val term_of_li : Cil_types.logic_info -> Cil_types.term
term_of_li li
assumes that li.l_body
matches LBterm t
and returns t
.
val is_set_of_ptr_or_array : Cil_types.logic_type -> bool
Checks whether the given logic type is a set of pointers.
val is_range_free : Cil_types.term -> bool
Returns true
iff the given term does not contain any range.
val is_bitfield_pointers : Cil_types.logic_type -> bool
Returns true
iff the given logic type is a bitfield pointer or a
set of bitfield pointers.
val term_has_lv_from_vi : Cil_types.term -> bool
Return true
iff the given term contains a variables that originates from
a C varinfo, that is a non-purely logic variable.
type
pred_or_term =
| |
PoT_pred of |
| |
PoT_term of |
val mk_ptr_sizeof : Cil_types.typ -> Cil_types.location -> Cil_types.exp
mk_ptr_sizeof ptr_typ loc
takes the pointer typ ptr_typ
that points
to a typ
typ and returns sizeof(typ)
.
val finite_min_and_max : Ival.t -> Integer.t * Integer.t
finite_min_and_max i
takes the finite ival i
and returns its bounds