Module Basic_blocks

module Basic_blocks: sig .. end

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.