module Misc:sig
..end
Utilities for E-ACSL.
val result_lhost : Cil_types.kernel_function -> Cil_types.lhost
val result_vi : Cil_types.kernel_function -> Cil_types.varinfo
val is_fc_or_compiler_builtin : Cil_types.varinfo -> bool
val is_fc_stdlib_generated : Cil_types.varinfo -> bool
Returns true if the varinfo
is a generated stdlib function. (For instance
generated function by the Variadic plug-in.
val term_addr_of : loc:Cil_types.location ->
Cil_types.term_lval -> Cil_types.typ -> Cil_types.term
val cty : Cil_types.logic_type -> Cil_types.typ
Assume that the logic type is indeed a C type. Just return it.
val ptr_base : loc:Cil_types.location -> Cil_types.exp -> Cil_types.exp
Takes an expression e
and return base
where base
is the address p
if e
is of the form p + i
and e
otherwise.
val ptr_base_and_base_addr : loc:Cil_types.location -> Cil_types.exp -> Cil_types.exp * Cil_types.exp
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
val is_bitfield_pointers : Cil_types.logic_type -> bool
val term_has_lv_from_vi : Cil_types.term -> bool
val name_of_binop : Cil_types.binop -> string
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.
module Id_term:Datatype.S_with_collections
with type t = term
Datatype for terms that relies on physical equality.
val extract_uncoerced_lval : Cil_types.exp -> Cil_types.exp option
Unroll the CastE
part of the expression until an Lval
is found, and
return it.
If at some point the expression is neither a CastE
nor an Lval
, then
return None
.
val strip_casts : Cil_types.exp -> Cil_types.exp * Cil_types.typ list
strip casts e
strips the casts from the expression e
and returns the
uncasted expression and the list of casts that were removed in order of
application. For example calling strip_casts ((A)((B)((C)e)))
will return
the expression e
and the list [C; B; A]
.
val add_casts : Cil_types.typ list -> Cil_types.exp -> Cil_types.exp
add_casts typs e
successively adds the casts in typs
to the expression
e
. For example calling add_casts [C; B; A] e
will return the expression
(A)((B)((C)e))
.