ForeignType Pointer -- dereference a pointer

• Operator: SPACE

• Usage:

  T ptr

• Inputs:
  • T, a foreign type,
  • ptr, a pointer,
• Outputs:
  • a foreign object, of type T;

i1 : x = int 5

o1 = 5

o1 : ForeignObject of type int32

i2 : ptr = address x

o2 = 0x7728fbefcdd0

o2 : Pointer

i3 : int ptr

o3 = 5

o3 : ForeignObject of type int32