Module E_ACSL.Misc

Utilities for E-ACSL.

Handling \result

  • returns

    the lhost corresponding to \result in the given function

  • returns

    the varinfo corresponding to \result in the given function

Other stuff

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.

Takes an expression e and return base where base is the address p if e is of the form p + i and e otherwise.

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

    true iff the given term does not contain any range.

val is_bitfield_pointers : Frama_c_kernel.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 : Frama_c_kernel.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 : Frama_c_kernel.Cil_types.binop -> string
  • returns

    the name of the given binop as a string.

finite_min_and_max i takes the finite ival i and returns its bounds.

Datatype for terms that relies on 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.