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:
"_"
,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"
.
val ttype_of_pointed : Cil_types.logic_type -> Cil_types.logic_type
Returns the type of pointed for a give logic_type
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
vdefined
is positionned to true
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
(ret_lval = ) vi.vname(args)
.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
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:
\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 typebytes_len
is a value in bytes that should be divided by the sizeof(ltyp)
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:
\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 typeval 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:
\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 pointerpred
must be applicable on simple types or pointersval 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:
\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 memberbytes_len
is the length of the structure in bytespred
must be applicable on simple types or pointersval 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
\valid{label}(ptr + (0 .. (len_bytes/sizeof(\*ptr))))
.Parameters:
ptr
must be a term of pointer type.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
\valid_read{label}(ptr + (0 .. (len_bytes/sizeof(\*ptr))))
.Parameters:
ptr
must be a term of pointer type.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:
\separated(p1 + (0 .. len1), p2 + (0 .. len2))
Parameters:
p1
and p2
must be of pointer typeval 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:
name
: Cil.default_behavior_name
requires
, ensures
, extension
: []
assigns
: = WritesAny
alloc
: FreeAllocAny
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.
termination
defaults to None
complete_disjoint
default to all disjoint, all complete