E_ACSL.Misc
Utilities for E-ACSL.
val result_lhost :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.lhost
val result_vi :
Frama_c_kernel.Cil_types.kernel_function ->
Frama_c_kernel.Cil_types.varinfo
val is_fc_or_compiler_builtin : Frama_c_kernel.Cil_types.varinfo -> bool
val is_fc_stdlib_generated : Frama_c_kernel.Cil_types.varinfo -> bool
Returns true if the varinfo
is a generated stdlib function. (For instance generated function by the Variadic plug-in.
Assume that the logic type is indeed a C type. Just return it.
val ptr_base :
loc:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.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:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.Cil_types.exp * Frama_c_kernel.Cil_types.exp
val term_of_li :
Frama_c_kernel.Cil_types.logic_info ->
Frama_c_kernel.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 : Frama_c_kernel.Cil_types.logic_type -> bool
Checks whether the given logic type is a set of pointers.
val is_range_free : Frama_c_kernel.Cil_types.term -> bool
val is_bitfield_pointers : Frama_c_kernel.Cil_types.logic_type -> bool
val term_has_lv_from_vi : Frama_c_kernel.Cil_types.term -> bool
val name_of_binop : Frama_c_kernel.Cil_types.binop -> string
val finite_min_and_max :
Frama_c_kernel.Ival.t ->
Frama_c_kernel.Integer.t * Frama_c_kernel.Integer.t
finite_min_and_max i
takes the finite ival i
and returns its bounds.
module Id_term :
Frama_c_kernel.Datatype.S_with_hashtbl
with type t = Frama_c_kernel.Cil_types.term
Datatype for terms that relies on physical equality. Note that of its collections only Hashtbl
can be used. Using Map
and Set
raises a fatal error as they require a comparison function, which cannot be defined in a sound way for physical equality.
val extract_uncoerced_lval :
Frama_c_kernel.Cil_types.exp ->
Frama_c_kernel.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
.