Wp.MemMemorySourceallocation tables
initialization tables
t_addr indexed array
Null address. Same as a_addr 0 0
Zero-offset base. Same as a_addr base 0
Constructor for { base ; offset }
Shift: a_shift a k adds k to a.offset
Returns the base
Returns the offset
Returns the offset in bytes from the logic offset (which is a memory cell index, actually)
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 fThe 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 ->
unitframes ~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 listval 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.predval 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