Module Misc

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 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

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

Returns true iff the given term contains a variables that originates from a C varinfo, that is a non-purely logic variable.

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.