Module Misc

module Misc: sig .. end

Utilities for E-ACSL.


Handling \result

val result_lhost : Cil_types.kernel_function -> Cil_types.lhost
val result_vi : Cil_types.kernel_function -> Cil_types.varinfo

Other stuff

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 [CBA].

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 [CBA] e will return the expression (A)((B)((C)e)).