Wp.MemMemory
val t_addr : Lang.F.tau
val t_malloc : Lang.F.tau
allocation tables
val t_init : Lang.F.tau
initialization tables
val t_mem : Lang.F.tau -> Lang.F.tau
t_addr indexed array
val a_null : Lang.F.term
Null address. Same as a_addr 0 0
val a_global : Lang.F.term -> Lang.F.term
Zero-offset base. Same as a_addr base 0
val a_addr : Lang.F.term -> Lang.F.term -> Lang.F.term
Constructor for { base ; offset }
val a_shift : Lang.F.term -> Lang.F.term -> Lang.F.term
Shift: a_shift a k
adds k
to a.offset
val a_base : Lang.F.term -> Lang.F.term
Returns the base
val a_offset : Lang.F.term -> Lang.F.term
Returns the offset
val a_base_offset : Lang.F.term -> Lang.F.term -> Lang.F.term
Returns the offset in bytes from the logic offset (which is a memory cell index, actually)
val f_null : Lang.lfun
val f_base : Lang.lfun
val f_global : Lang.lfun
val f_shift : Lang.lfun
val f_offset : Lang.lfun
val f_havoc : Lang.lfun
val f_set_init : Lang.lfun
val f_region : Lang.lfun
val f_addr_of_int : Lang.lfun
Physical address
val f_int_of_addr : Lang.lfun
Physical address
val p_addr_lt : Lang.lfun
val p_addr_le : Lang.lfun
val p_linked : Lang.lfun
val p_framed : Lang.lfun
val p_sconst : Lang.lfun
val p_cinits : Lang.lfun
val p_is_init_r : Lang.lfun
val p_separated : Lang.lfun
val p_included : Lang.lfun
val p_valid_rd : Lang.lfun
val p_valid_rw : Lang.lfun
val p_valid_obj : Lang.lfun
val p_invalid : Lang.lfun
val p_eqmem : Lang.lfun
val p_monotonic : Lang.lfun
Register simplifiers for functions producing addr
terms:
~base es
is the simplifier for (f es).base
~offset es
is the simplifier for (f es).offset
~linear:true
register simplifier f(f(p,i),k)=f(p,i+j)
on f
~equal a b
is the set_eq_builtin
for f
The equality builtin is wrapped inside a default builtin that compares f es
by computing base
and offset
.
val register :
?base:( Lang.F.term list -> Lang.F.term ) ->
?offset:( Lang.F.term list -> Lang.F.term ) ->
?equal:( Lang.F.term -> Lang.F.term -> Lang.F.pred ) ->
?linear:bool ->
Lang.lfun ->
unit
frames ~addr
are frame conditions for reading a value at address addr
from a chunk of memory. The value read at addr
have length offset
, while individual element in memory chunk have type tau
and offset length sizeof
.
Memory variables use ~basename
or "mem"
by default.
val frames :
addr:Lang.F.term ->
offset:Lang.F.term ->
sizeof:Lang.F.term ->
?basename:string ->
Lang.F.tau ->
Sigs.frame list
val separated :
shift:( 'a -> Ctypes.c_object -> Lang.F.term -> 'a ) ->
addrof:( 'a -> Lang.F.term ) ->
sizeof:( Ctypes.c_object -> Lang.F.term ) ->
'a Sigs.rloc ->
'a Sigs.rloc ->
Lang.F.pred
val included :
shift:( 'a -> Ctypes.c_object -> Lang.F.term -> 'a ) ->
addrof:( 'a -> Lang.F.term ) ->
sizeof:( Ctypes.c_object -> Lang.F.term ) ->
'a Sigs.rloc ->
'a Sigs.rloc ->
Lang.F.pred
val unsupported_union : Frama_c_kernel.Cil_types.fieldinfo -> unit