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 mk_call : loc:Cil_datatype.Location.t ->
?result:Cil_types.lval -> string -> Cil_types.exp list -> Cil_types.stmt
Call an E-ACSL library function or an E-ACSL built-in.
Raises Unregistered_library_function if the given string does not represent such a function or if these functions were never registered (only possible when using E-ACSL through its API.
val mk_deref : loc:Cil_datatype.Location.t -> Cil_types.exp -> Cil_types.exp
Make a dereference of an expression
type annotation_kind = 
| Assertion
| Precondition
| Postcondition
| Invariant
| RTE
val mk_e_acsl_guard : ?reverse:bool ->
annotation_kind ->
Cil_types.kernel_function ->
Cil_types.exp -> Cil_types.predicate -> Cil_types.stmt
val mk_block : Project.t -> Cil_types.stmt -> Cil_types.block -> Cil_types.stmt

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 -> string list
val is_library_loc : Cil_types.location -> bool
val register_library_function : Cil_types.varinfo -> unit
val reset : unit -> unit
val mk_store_stmt : ?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
val mk_duplicate_store_stmt : ?str_size:Cil_types.exp -> Cil_types.varinfo -> Cil_types.stmt
val mk_delete_stmt : Cil_types.varinfo -> Cil_types.stmt
val mk_full_init_stmt : ?addr:bool -> Cil_types.varinfo -> Cil_types.stmt
val mk_initialize : loc:Cil_types.location -> Cil_types.lval -> Cil_types.stmt
val mk_mark_readonly : Cil_types.varinfo -> Cil_types.stmt

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

Handling prefixes of generated library functions and variables


val mk_api_name : string -> string
Returns given some base name append it with a prefix used by functions and variables in the public API of E-ACSL runtime library. (__e_acsl_)
val mk_gen_name : string -> string
Returns given some base name append it with a prefix used by functions and variables generated by E-ACSL (__gen_e_acsl_).
val is_generated_varinfo : Cil_types.varinfo -> bool
Returns true if the name of the given varinfo indicates that it has been generated by E-ACSL. This is done by checking whether the name of the varinfo has been generated using mk_gen_name function.
val is_generated_literal_string_varinfo : Cil_types.varinfo -> bool
Same as is_generated_varinfo but indicates that varinfo is a local variable which replaced a literal string.
val is_generated_kf : Cil_types.kernel_function -> bool
Same as is_generated_varinfo but for kernel functions