Module Misc

module Misc: sig .. end
Utilities for E-ACSL.

Handling the E-ACSL's C-libraries, part I




Builders


exception Unregistered_library_function of string
val get_lib_fun_vi : string -> Cil_types.varinfo
Returns varinfo corresponding to a name of a given library function

Handling \result


val result_lhost : Cil_types.kernel_function -> Cil_types.lhost
Returns the lhost corresponding to \result in the given function
val result_vi : Cil_types.kernel_function -> Cil_types.varinfo
Returns the varinfo corresponding to \result in the given function

Handling the E-ACSL's C-libraries


val library_files : unit -> Datatype.Filepath.t list
val is_library_loc : Cil_types.location -> bool
val register_library_function : Cil_types.varinfo -> unit
val reset : unit -> unit
val is_fc_or_compiler_builtin : Cil_types.varinfo -> bool

Other stuff


val term_addr_of : loc:Cil_types.location ->
Cil_types.term_lval -> Cil_types.typ -> Cil_types.term
val reorder_ast : unit -> unit
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 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
Returns true iff the given term does not contain any range.
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.
type pred_or_term = 
| PoT_pred of Cil_types.predicate
| PoT_term of Cil_types.term
val mk_ptr_sizeof : Cil_types.typ -> Cil_types.location -> Cil_types.exp
mk_ptr_sizeof ptr_typ loc takes the pointer typ ptr_typ that points to a typ typ and returns sizeof(typ).
val name_of_binop : Cil_types.binop -> string
Returns the name of the given binop as a 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.