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_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 ptr_base : 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
.