Module Basic_blocks

module Basic_blocks: sig .. end
string_of_typ t returns a name generated from the given t. This is basically the C name of the type except that: For example for: struct X ( * ) [10], the name is "ptr_arr10_st_X".

Features related to terms


val string_of_typ : Cil_types.typ -> string
string_of_typ t returns a name generated from the given t. This is basically the C name of the type except that: For example for: struct X ( * ) [10], the name is "ptr_arr10_st_X".
val ttype_of_pointed : Cil_types.logic_type -> Cil_types.logic_type
Returns the type of pointed for a give logic_type

C


val ptr_of : Cil_types.typ -> Cil_types.typ
For a type T, returns T*
val const_of : Cil_types.typ -> Cil_types.typ
For a type T, returns T const
val size_t : unit -> Cil_types.typ
Finds and returns size_t
val prepare_definition : string -> Cil_types.typ -> Cil_types.fundec
Create a function definition from a name and a type
val call_function : Cil_types.lval option ->
Cil_types.varinfo -> Cil_types.exp list -> Cil_types.instr
call_function ret_lval vi args creates an instruction

Terms


val cvar_to_tvar : Cil_types.varinfo -> Cil_types.term
Builds a term from a varinfo
val tunref_range : ?loc:Cil_types.location -> Cil_types.term -> Cil_types.term -> Cil_types.term
tunref_range ~loc ptr len builds *(ptr + (0 .. len-1))
val tunref_range_bytes_len : ?loc:Cil_types.location -> Cil_types.term -> Cil_types.term -> Cil_types.term
tunref_range ~loc ptr bytes_len same as tunref_range except that length is provided in bytes.
val tplus : ?loc:Cil_types.location -> Cil_types.term -> Cil_types.term -> Cil_types.term
tplus ~loc t1 t2 builds t1+t2
val tminus : ?loc:Cil_types.location -> Cil_types.term -> Cil_types.term -> Cil_types.term
tminus ~loc t1 t2 builds t1-t2
val tdivide : ?loc:Cil_types.location -> Cil_types.term -> Cil_types.term -> Cil_types.term
tdivide ~loc t1 t2 builds t1/t2

Predicates


val pbounds_incl_excl : ?loc:Cil_types.location ->
Cil_types.term -> Cil_types.term -> Cil_types.term -> Cil_types.predicate
pbounds_incl_excl ~loc low v up builds low <= v < up.
val plet_len_div_size : ?loc:Cil_types.location ->
?name_ext:string ->
Cil_types.logic_type ->
Cil_types.term ->
(Cil_types.term -> Cil_types.predicate) -> Cil_types.predicate
plet_len_div_size ~loc ~name_ext ltyp bytes_len pred buils a predicate: with name = "__fc_<name_ext>len". For example, if pred len generates an ACSL predicate: ltyp is int, and bytes_len is 16, it generates: Parameters:
val punfold_all_elems_eq : ?loc:Cil_types.location ->
Cil_types.term -> Cil_types.term -> Cil_types.term -> Cil_types.predicate
punfold_all_elems_eq ~loc p1 p2 len builds a predicate: If p1[j1] is itself an array, it recursively builds a predicate: Parameters:
val punfold_all_elems_pred : ?loc:Cil_types.location ->
Cil_types.term ->
Cil_types.term ->
(?loc:Cil_types.location -> Cil_types.term -> Cil_types.predicate) ->
Cil_types.predicate
punfold_all_elems_pred ~loc ptr len pred builds a predicate: If ptr[j1] is a compound type (array or structure), it recursively builds a predicate on each element (either by introducing a new \forall for arrays or a conjunction for structure fields).


val punfold_flexible_struct_pred : ?loc:Cil_types.location ->
Cil_types.term ->
Cil_types.term ->
(?loc:Cil_types.location -> Cil_types.term -> Cil_types.predicate) ->
Cil_types.predicate
punfold_flexible_struct_pred ~loc struct bytes_len pred.

For a struct term of C type struct X { ... ; Type a[]; };, it generates a predicate:

If met components are compound, it behaves like punfold_all_elems_pred.

Parameters:


val pvalid_len_bytes : ?loc:Cil_types.location ->
Cil_types.logic_label ->
Cil_types.term -> Cil_types.term -> Cil_types.predicate
pvalid_len_bytes ~loc label ptr bytes_len generates a predicate Parameters:
val pvalid_read_len_bytes : ?loc:Cil_types.location ->
Cil_types.logic_label ->
Cil_types.term -> Cil_types.term -> Cil_types.predicate
pvalid_read_len_bytes ~loc label ptr bytes_len generates a predicate Parameters:
val pcorrect_len_bytes : ?loc:Cil_types.location ->
Cil_types.logic_type -> Cil_types.term -> Cil_types.predicate
pcorrect_len_bytes ~loc ltyp bytes_len returns a predicate bytes_len % sizeof(ltyp) == 0.
val pseparated_memories : ?loc:Cil_types.location ->
Cil_types.term ->
Cil_types.term -> Cil_types.term -> Cil_types.term -> Cil_types.predicate
pseparated_memories ~loc p1 len1 p2 len2 returns a predicate: Parameters:

Specification


val make_behavior : ?name:string ->
?assumes:Cil_types.identified_predicate list ->
?requires:Cil_types.identified_predicate list ->
?ensures:(Cil_types.termination_kind * Cil_types.identified_predicate) list ->
?assigns:Cil_types.assigns ->
?alloc:Cil_types.allocation ->
?extension:Cil_types.acsl_extension list -> unit -> Cil_types.behavior
Builds a behavior from its components. If a component is missing, it defaults to:
val make_funspec : Cil_types.behavior list ->
?termination:Cil_types.identified_predicate option ->
?complete_disjoint:string list list * string list list ->
unit -> Cil_types.funspec
Builds a funspec from a list of behaviors.