ATSLIB/prelude/pointer

This package contains various functions on pointers such as those for supporting direct memory access and those for performing pointer arithmetic.


  • g0ofg1_ptr
  • g1ofg0_ptr
  • ptr_get_index
  • ptr0_is_null
  • ptr1_is_null
  • ptr0_isnot_null
  • ptr1_isnot_null
  • add_ptr0_bsz
  • add_ptr1_bsz
  • sub_ptr0_bsz
  • sub_ptr1_bsz
  • sub_ptr0_ptr0
  • sub_ptr1_ptr1
  • ptr0_succ
  • ptr1_succ
  • ptr0_pred
  • ptr1_pred
  • ptr0_add_gint
  • ptr0_add_guint
  • ptr1_add_gint
  • ptr1_add_guint
  • ptr0_sub_gint
  • ptr0_sub_guint
  • ptr1_sub_gint
  • ptr1_sub_guint
  • lt_ptr0_ptr0
  • lt_ptr1_ptr1
  • lte_ptr0_ptr0
  • lte_ptr1_ptr1
  • gt_ptr0_ptr0
  • gt_ptr1_ptr1
  • gte_ptr0_ptr0
  • gte_ptr1_ptr1
  • eq_ptr0_ptr0
  • eq_ptr1_ptr1
  • neq_ptr0_ptr0
  • neq_ptr1_ptr1
  • compare_ptr0_ptr0
  • compare_ptr1_ptr1
  • ptr_get
  • ptr_set
  • ptr_exch
  • Overloaded Symbols
  • g0ofg1
  • g1ofg0
  • ptr_is_null
  • ptr_isnot_null
  • add_ptr_bsz
  • sub_ptr_bsz
  • ptr_succ
  • ptr_pred
  • ptr_add
  • ptr_sub
  • <
  • <=
  • >
  • >=
  • =
  • !=
  • compare
  • print
  • prerr
  • fprint

  • g0ofg1_ptr

    Synopsis

    castfn
    g0ofg1_ptr (p: Ptr):<> ptr

    g1ofg0_ptr

    Synopsis

    castfn
    g1ofg0_ptr (p: ptr):<> Ptr0

    ptr_get_index

    Synopsis

    prfun
    ptr_get_index
      {l1:addr} (p: ptr l1): [l2:addr] EQADDR(l1, l2)

    Description

    The purpose of calling this proof function is to introduce a static variable that binds to the index of the type assigned to the argument of the function.

    Example

    Let p be a value of the type ptr(L) for some L. Then the following line of code initiates a binding between l and L:
    prval [l:addr] EQADDR () = ptr_get_index (p)

    ptr0_is_null

    Synopsis

    fun ptr0_is_null (p: ptr):<> bool = "mac#%"

    Description

    This function returns true if and only if its argument is the null pointer.

    ptr1_is_null

    Synopsis

    fun
    ptr1_is_null
      {l:addr}(p: ptr l):<> bool (l==null) = "mac#%"

    Description

    This function does the same as ptr0_is_null but is given a more informative type.

    ptr0_isnot_null

    Synopsis

    fun ptr0_isnot_null (p: ptr):<> bool = "mac#%"

    Description

    This function returns true if and only if its argument is not the null pointer.

    ptr1_isnot_null

    Synopsis

    fun
    ptr1_isnot_null
      {l:addr}(p: ptr l):<> bool (l > null) = "mac#%"

    Description

    This function does the same as ptr0_isnot_null but is given a more informative type.

    add_ptr0_bsz

    Synopsis

    fun add_ptr0_bsz
      (p: ptr, ofs: size_t):<> ptr = "mac#%"

    add_ptr1_bsz

    Synopsis

    fun
    add_ptr1_bsz{l:addr}{i:int}
      (p: ptr l, ofs: size_t (i)):<> ptr (l+i) = "mac#%"

    sub_ptr0_bsz

    Synopsis

    fun sub_ptr0_bsz
      (p: ptr, ofs: size_t):<> ptr = "mac#%"

    sub_ptr1_bsz

    Synopsis

    fun
    sub_ptr1_bsz{l:addr}{i:int}
      (p: ptr l, ofs: size_t (i)):<> ptr (l-i) = "mac#%"

    sub_ptr0_ptr0

    Synopsis

    fun sub_ptr0_ptr0
      (p1: ptr, p2: ptr):<> ssize_t = "mac#%"

    sub_ptr1_ptr1

    Synopsis

    fun
    sub_ptr1_ptr1{l1,l2:addr}
      (p1: ptr l1, p2: ptr l2):<> ssize_t (l1-l2) = "mac#%"

    ptr0_succ

    Synopsis

    fun{a:vt0p} ptr0_succ (p: ptr):<> ptr

    ptr1_succ

    Synopsis

    fun{
    a:vt0p
    } ptr1_succ{l:addr} (p: ptr l):<> ptr (l+sizeof(a))

    ptr0_pred

    Synopsis

    fun{a:vt0p} ptr0_pred (p: ptr):<> ptr

    ptr1_pred

    Synopsis

    fun{
    a:vt0p
    } ptr1_pred{l:addr} (p: ptr l):<> ptr (l-sizeof(a))

    ptr0_add_gint

    Synopsis

    fun{
    a:vt0p}{tk:tk
    } ptr0_add_gint (p: ptr, ofs: g0int (tk)):<> ptr

    ptr0_add_guint

    Synopsis

    fun{
    a:vt0p}{tk:tk
    } ptr0_add_guint (p: ptr, ofs: g0uint (tk)):<> ptr

    ptr1_add_gint

    Synopsis

    fun{
    a:vt0p}{tk:tk
    } ptr1_add_gint
      {l:addr}{i:int}
      (p: ptr l, ofs: g1int (tk, i)):<> ptr(l+i*sizeof(a))

    ptr1_add_guint

    Synopsis

    fun{
    a:vt0p}{tk:tk
    } ptr1_add_guint
      {l:addr}{i:int}
      (p: ptr l, ofs: g1uint (tk, i)):<> ptr(l+i*sizeof(a))

    ptr0_sub_gint

    Synopsis

    fun{
    a:vt0p}{tk:tk
    } ptr0_sub_gint (p: ptr, ofs: g0int (tk)):<> ptr

    ptr0_sub_guint

    Synopsis

    fun{
    a:vt0p}{tk:tk
    } ptr0_sub_guint (p: ptr, ofs: g0uint (tk)):<> ptr

    ptr1_sub_gint

    Synopsis

    fun{
    a:vt0p}{tk:tk
    } ptr1_sub_gint
      {l:addr}{i:int}
      (p: ptr l, ofs: g1int (tk, i)):<> ptr(l-i*sizeof(a))

    ptr1_sub_guint

    Synopsis

    fun{
    a:vt0p}{tk:tk
    } ptr1_sub_guint
      {l:addr}{i:int}
      (p: ptr l, ofs: g1uint (tk, i)):<> ptr(l-i*sizeof(a))

    lt_ptr0_ptr0

    Synopsis

    fun lt_ptr0_ptr0
      (p1: ptr, p2: ptr):<> bool = "mac#%"

    lt_ptr1_ptr1

    Synopsis

    fun lt_ptr1_ptr1
      {l1,l2:addr} (
      p1: ptr (l1), p2: ptr (l2)
    ) :<> bool (l1 < l2) = "mac#%"

    lte_ptr0_ptr0

    Synopsis

    fun lte_ptr0_ptr0
      (p1: ptr, p2: ptr):<> bool = "mac#%"

    lte_ptr1_ptr1

    Synopsis

    fun lte_ptr1_ptr1
      {l1,l2:addr} (
      p1: ptr (l1), p2: ptr (l2)
    ) :<> bool (l1 <= l2) = "mac#%"

    gt_ptr0_ptr0

    Synopsis

    fun gt_ptr0_ptr0
      (p1: ptr, p2: ptr):<> bool = "mac#%"

    gt_ptr1_ptr1

    Synopsis

    fun gt_ptr1_ptr1
      {l1,l2:addr} (
      p1: ptr (l1), p2: ptr (l2)
    ) :<> bool (l1 > l2) = "mac#%"

    gte_ptr0_ptr0

    Synopsis

    fun gte_ptr0_ptr0
      (p1: ptr, p2: ptr):<> bool = "mac#%"

    gte_ptr1_ptr1

    Synopsis

    fun gte_ptr1_ptr1
      {l1,l2:addr} (
      p1: ptr (l1), p2: ptr (l2)
    ) :<> bool (l1 >= l2) = "mac#%"

    eq_ptr0_ptr0

    Synopsis

    fun eq_ptr0_ptr0
      (p1: ptr, p2: ptr):<> bool = "mac#%"

    eq_ptr1_ptr1

    Synopsis

    fun eq_ptr1_ptr1
      {l1,l2:addr} (
      p1: ptr (l1), p2: ptr (l2)
    ) :<> bool (l1 == l2) = "mac#%"

    neq_ptr0_ptr0

    Synopsis

    fun neq_ptr0_ptr0
      (p1: ptr, p2: ptr):<> bool = "mac#%"

    neq_ptr1_ptr1

    Synopsis

    fun neq_ptr1_ptr1
      {l1,l2:addr} (
      p1: ptr (l1), p2: ptr (l2)
    ) :<> bool (l1 != l2) = "mac#%"

    compare_ptr0_ptr0

    Synopsis

    fun compare_ptr0_ptr0
      (p1: ptr, p2: ptr):<> int = "mac#%"

    compare_ptr1_ptr1

    Synopsis

    fun compare_ptr1_ptr1
      {l1,l2:addr} (p1: ptr l1, p2: ptr l2) :<> int = "mac#%"

    ptr_get

    Synopsis

    fun{a:vt0p}
    ptr_get{l:addr}
      (pf: !INV(a) @ l >> a?! @ l | p: ptr l):<> a

    ptr_set

    Synopsis

    fun{a:vt0p}
    ptr_set{l:addr}
      (pf: !a? @ l >> a @ l | p: ptr l, x: INV(a)):<!wrt> void

    ptr_exch

    Synopsis

    fun{a:vt0p}
    ptr_exch{l:addr}
      (pf: !INV(a) @ l | p: ptr l, x: &a >> a):<!wrt> void

    Overloaded Symbols


    g0ofg1

    Synopsis

    overload g0ofg1 with g0ofg1_ptr

    g1ofg0

    Synopsis

    overload g1ofg0 with g1ofg0_ptr

    ptr_is_null

    Synopsis

    overload ptr_is_null with ptr0_is_null of 0
    overload ptr_is_null with ptr1_is_null of 10

    ptr_isnot_null

    Synopsis

    overload ptr_isnot_null with ptr0_isnot_null of 0
    overload ptr_isnot_null with ptr1_isnot_null of 10

    add_ptr_bsz

    Synopsis

    overload add_ptr_bsz with add_ptr0_bsz of 0
    overload add_ptr_bsz with add_ptr1_bsz of 20

    sub_ptr_bsz

    Synopsis

    overload sub_ptr_bsz with sub_ptr0_bsz of 0
    overload sub_ptr_bsz with sub_ptr1_bsz of 20

    ptr_succ

    Synopsis

    overload ptr_succ with ptr0_succ of 0
    overload ptr_succ with ptr1_succ of 10

    ptr_pred

    Synopsis

    overload ptr_pred with ptr0_pred of 0
    overload ptr_pred with ptr1_pred of 10

    ptr_add

    Synopsis

    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

    ptr_sub

    Synopsis

    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

    <

    Synopsis

    overload < with lt_ptr0_ptr0 of 0
    overload < with lt_ptr1_ptr1 of 20

    <=

    Synopsis

    overload <= with lte_ptr0_ptr0 of 0
    overload <= with lte_ptr1_ptr1 of 20

    >

    Synopsis

    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

    >=

    Synopsis

    overload >= with gte_ptr0_ptr0 of 0
    overload >= with gte_ptr1_ptr1 of 20

    =

    Synopsis

    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

    !=

    Synopsis

    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

    compare

    Synopsis

    overload compare with compare_ptr0_ptr0 of 0
    overload compare with compare_ptr1_ptr1 of 20

    print

    Synopsis

    overload print with print_ptr

    prerr

    Synopsis

    overload prerr with prerr_ptr

    fprint

    Synopsis

    overload fprint with fprint_ptr

    This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi. SourceForge.net Logo