This package contains various functions on pointers such as those for supporting direct memory access and those for performing pointer arithmetic.
castfn
g0ofg1_ptr (p: Ptr):<> ptr
castfn
g1ofg0_ptr (p: ptr):<> Ptr0
prfun
ptr_get_index
{l1:addr} (p: ptr l1): [l2:addr] EQADDR(l1, l2)
prval [l:addr] EQADDR () = ptr_get_index (p)
fun ptr0_is_null (p: ptr):<> bool = "mac#%"
fun
ptr1_is_null
{l:addr}(p: ptr l):<> bool (l==null) = "mac#%"
fun ptr0_isnot_null (p: ptr):<> bool = "mac#%"
fun
ptr1_isnot_null
{l:addr}(p: ptr l):<> bool (l > null) = "mac#%"
fun add_ptr0_bsz
(p: ptr, ofs: size_t):<> ptr = "mac#%"
fun
add_ptr1_bsz{l:addr}{i:int}
(p: ptr l, ofs: size_t (i)):<> ptr (l+i) = "mac#%"
fun sub_ptr0_bsz
(p: ptr, ofs: size_t):<> ptr = "mac#%"
fun
sub_ptr1_bsz{l:addr}{i:int}
(p: ptr l, ofs: size_t (i)):<> ptr (l-i) = "mac#%"
fun sub_ptr0_ptr0
(p1: ptr, p2: ptr):<> ssize_t = "mac#%"
fun
sub_ptr1_ptr1{l1,l2:addr}
(p1: ptr l1, p2: ptr l2):<> ssize_t (l1-l2) = "mac#%"
fun{a:vt0p} ptr0_succ(p: ptr):<> ptr
fun{
a:vt0p
} ptr1_succ{l:addr} (p: ptr l):<> ptr (l+sizeof(a))
fun{a:vt0p} ptr0_pred(p: ptr):<> ptr
fun{
a:vt0p
} ptr1_pred{l:addr} (p: ptr l):<> ptr (l-sizeof(a))
fun{
a:vt0p}{tk:tk
} ptr0_add_gint(p: ptr, ofs: g0int(tk)):<> ptr
fun{
a:vt0p}{tk:tk
} ptr0_add_guint(p: ptr, ofs: g0uint(tk)):<> ptr
fun{
a:vt0p}{tk:tk
} ptr1_add_gint
{l:addr}{i:int}
(p: ptr l, ofs: g1int (tk, i)):<> ptr(l+i*sizeof(a))
fun{
a:vt0p}{tk:tk
} ptr1_add_guint
{l:addr}{i:int}
(p: ptr l, ofs: g1uint (tk, i)):<> ptr(l+i*sizeof(a))
fun{
a:vt0p}{tk:tk
} ptr0_sub_gint (p: ptr, ofs: g0int (tk)):<> ptr
fun{
a:vt0p}{tk:tk
} ptr0_sub_guint (p: ptr, ofs: g0uint (tk)):<> ptr
fun{
a:vt0p}{tk:tk
} ptr1_sub_gint
{l:addr}{i:int}
(p: ptr l, ofs: g1int (tk, i)):<> ptr(l-i*sizeof(a))
fun{
a:vt0p}{tk:tk
} ptr1_sub_guint
{l:addr}{i:int}
(p: ptr l, ofs: g1uint (tk, i)):<> ptr(l-i*sizeof(a))
fun lt_ptr0_ptr0
(p1: ptr, p2: ptr):<> bool = "mac#%"
fun lt_ptr1_ptr1
{l1,l2:addr} (
p1: ptr (l1), p2: ptr (l2)
) :<> bool (l1 < l2) = "mac#%"
fun lte_ptr0_ptr0
(p1: ptr, p2: ptr):<> bool = "mac#%"
fun lte_ptr1_ptr1
{l1,l2:addr} (
p1: ptr (l1), p2: ptr (l2)
) :<> bool (l1 <= l2) = "mac#%"
fun gt_ptr0_ptr0
(p1: ptr, p2: ptr):<> bool = "mac#%"
fun gt_ptr1_ptr1
{l1,l2:addr} (
p1: ptr (l1), p2: ptr (l2)
) :<> bool (l1 > l2) = "mac#%"
fun gte_ptr0_ptr0
(p1: ptr, p2: ptr):<> bool = "mac#%"
fun gte_ptr1_ptr1
{l1,l2:addr} (
p1: ptr (l1), p2: ptr (l2)
) :<> bool (l1 >= l2) = "mac#%"
fun eq_ptr0_ptr0
(p1: ptr, p2: ptr):<> bool = "mac#%"
fun eq_ptr1_ptr1
{l1,l2:addr} (
p1: ptr (l1), p2: ptr (l2)
) :<> bool (l1 == l2) = "mac#%"
fun neq_ptr0_ptr0
(p1: ptr, p2: ptr):<> bool = "mac#%"
fun neq_ptr1_ptr1
{l1,l2:addr} (
p1: ptr (l1), p2: ptr (l2)
) :<> bool (l1 != l2) = "mac#%"
fun
compare_ptr0_ptr0
(p1: ptr, p2: ptr):<> int = "mac#%"
fun compare_ptr1_ptr1
{l1,l2:addr} (p1: ptr l1, p2: ptr l2) :<> int = "mac#%"
fun{a:vt0p}
ptr_get{l:addr}
(pf: !INV(a) @ l >> a?! @ l | p: ptr l):<> a
fun{a:vt0p}
ptr_set{l:addr}
(pf: !a? @ l >> a @ l | p: ptr l, x: INV(a)):<!wrt> void
fun{a:vt0p}
ptr_exch{l:addr}
(pf: !INV(a) @ l | p: ptr l, x: &a >> a):<!wrt> void
overload g0ofg1 with g0ofg1_ptr
overload g1ofg0 with g1ofg0_ptr
overload ptr_is_null with ptr0_is_null of 0
overload ptr_is_null with ptr1_is_null of 10
overload ptr_isnot_null with ptr0_isnot_null of 0
overload ptr_isnot_null with ptr1_isnot_null of 10
overload add_ptr_bsz with add_ptr0_bsz of 0
overload add_ptr_bsz with add_ptr1_bsz of 20
overload sub_ptr_bsz with sub_ptr0_bsz of 0
overload sub_ptr_bsz with sub_ptr1_bsz of 20
overload ptr_succ with ptr0_succ of 0
overload ptr_succ with ptr1_succ of 10
overload ptr_pred with ptr0_pred of 0
overload ptr_pred with ptr1_pred of 10
overload ptr_add with ptr0_add_gint of 0
overload ptr_add with ptr0_add_guint of 0
overload ptr_add with ptr1_add_gint of 20
overload ptr_add with ptr1_add_guint of 20
overload ptr_sub with ptr0_sub_gint of 0
overload ptr_sub with ptr0_sub_guint of 0
overload ptr_sub with ptr1_sub_gint of 20
overload ptr_sub with ptr1_sub_guint of 20
overload < with lt_ptr0_ptr0 of 0
overload < with lt_ptr1_ptr1 of 20
overload <= with lte_ptr0_ptr0 of 0
overload <= with lte_ptr1_ptr1 of 20
overload > with gt_ptr0_ptr0 of 0
overload > with gt_ptr0_intz of 0
overload > with gt_ptr1_ptr1 of 20
overload > with gt_ptr1_intz of 10
overload > with gt_cptr_intz of 0
overload >= with gte_ptr0_ptr0 of 0
overload >= with gte_ptr1_ptr1 of 20
overload = with eq_ptr0_ptr0 of 0
overload = with eq_ptr0_intz of 0
overload = with eq_ptr1_ptr1 of 20
overload = with eq_ptr1_intz of 10
overload = with eq_cptr_intz of 0
overload != with neq_ptr0_ptr0 of 0
overload != with neq_ptr0_intz of 0
overload != with neq_ptr1_ptr1 of 20
overload != with neq_ptr1_intz of 10
overload != with neq_cptr_intz of 0
overload compare with compare_ptr0_ptr0 of 0
overload compare with compare_ptr1_ptr1 of 20
overload print with print_ptr
overload prerr with prerr_ptr
overload fprint with fprint_ptr
| This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi. |
|