Module Basic_blocks

string_of_typ t returns a name generated from the given t. This is basically the C name of the type except that:

• separator is "_",
• unsigned is "u"
• [SIZE] is "arrSIZE",
• * is "ptr",
• enum is "e_",
• struct is "st_",
• union is "un_"

For example for: struct X ( * ) [10], the name is "ptr_arr10_st_X".

Returns the type of pointed for a give logic_type

For a type T, returns T*

For a type T, returns T const

Finds and returns size_t

Create a function definition from a name and a type

• vdefined is positionned to true
• formals are registered to FormalsDecl

call_function ret_lval vi args creates an instruction

• (ret_lval = ) vi.vname(args).

Builds a term from a varinfo

tunref_range ~loc ptr len builds *(ptr + (0 .. len-1))

tunref_range ~loc ptr bytes_len same as tunref_range except that length is provided in bytes.

tplus ~loc t1 t2 builds t1+t2

tminus ~loc t1 t2 builds t1-t2

tdivide ~loc t1 t2 builds t1/t2

pbounds_incl_excl ~loc low v up builds low <= v < up.

plet_len_div_size ~loc ~name_ext ltyp bytes_len pred buils a predicate:

• \let name = bytes_len / sizeof(ltyp) ; < pred name >

with name = "__fc_<name_ext>len". For example, if pred len generates an ACSL predicate:

• \forall int x ; 0 <= x < len ==> p[x] == 0,

ltyp is int, and bytes_len is 16, it generates:

• \let __fc_len = bytes_len / sizeof(ltyp) ; \forall int x ; 0 <= x < __fc_len ==> p[x] == 0.

Parameters:

• loc defaults to Cil_datatype.Location.unknown
• name_ext defaults to ""
• ltyp must be a logic C type
• bytes_len is a value in bytes that should be divided by the sizeof(ltyp)
• if the elements contains structures they cannot have flexible array member

punfold_all_elems_eq ~loc p1 p2 len builds a predicate:

• \forall integer j1 ; 0 <= j1 < len ==> p1[j1] == p2[j1].

If p1[j1] is itself an array, it recursively builds a predicate:

• \forall integer j2 ; 0 <= j2 < len_of_array ==> ....

Parameters:

• p1 and p2 must be pointers to the same type

punfold_all_elems_pred ~loc ptr len pred builds a predicate:

• \forall integer j ; 0 <= j1 < len ==> < pred (\*(ptr + j1)) >.

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

• ptr must be a pointer
• pred must be applicable on simple types or pointers
• if the elements contains structures they cannot have flexible array member

punfold_flexible_struct_pred ~loc struct bytes_len pred.

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

• \let __fc_len = (bytes_len - sizeof(struct X)) / sizeof(Type) ; < pred on struct fields > && \forall integer j ; 0 <= j <= __fc_len ==> < pred on struct.a[j] >

If met components are compound, it behaves like punfold_all_elems_pred.

Parameters:

• struct must be a (term) structure with a flexible array member
• bytes_len is the length of the structure in bytes
• pred must be applicable on simple types or pointers

pvalid_len_bytes ~loc label ptr bytes_len generates a predicate

• \valid{label}(ptr + (0 .. (len_bytes/sizeof(\*ptr)))).

Parameters:

• ptr must be a term of pointer type.

pvalid_read_len_bytes ~loc label ptr bytes_len generates a predicate

• \valid_read{label}(ptr + (0 .. (len_bytes/sizeof(\*ptr)))).

Parameters:

• ptr must be a term of pointer type.

pcorrect_len_bytes ~loc ltyp bytes_len returns a predicate bytes_len % sizeof(ltyp) == 0.

pseparated_memories ~loc p1 len1 p2 len2 returns a predicate:

• \separated(p1 + (0 .. len1), p2 + (0 .. len2))

Parameters:

• p1 and p2 must be of pointer type

Builds a behavior from its components. If a component is missing, it defaults to:

• name: Cil.default_behavior_name
• requires, ensures, extension: []
• assigns: = WritesAny
• alloc: FreeAllocAny

Builds a funspec from a list of behaviors.

• termination defaults to None
• complete_disjoint default to all disjoint, all complete