summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorOri Bernstein <ori@eigenstate.org>2017-01-29 23:54:46 -0800
committerOri Bernstein <ori@eigenstate.org>2017-01-29 23:54:46 -0800
commit5c12b2816f7feeafb5e3e52ee287bf33927a1c74 (patch)
tree61ffa45b48d7f7683d3e590ecc33883391fa9d1d /doc
parentedd0699416df633c8199ecfecb48f5f18917a32d (diff)
downloadmc-5c12b2816f7feeafb5e3e52ee287bf33927a1c74.tar.gz
Add specification of accessing pointers via casts.
Diffstat (limited to 'doc')
-rw-r--r--doc/lang.txt12
1 files changed, 12 insertions, 0 deletions
diff --git a/doc/lang.txt b/doc/lang.txt
index d20490e..76ea677 100644
--- a/doc/lang.txt
+++ b/doc/lang.txt
@@ -1328,6 +1328,18 @@ TABLE OF CONTENTS:
The `#` operator refers to the value at the pointer `expr`. This
is an lvalue, and may be stored to.
+ The pointer being dereferenced may have at some point come from a
+ cast expression. It may also be constructed by arbitrary code via
+ integer manipulations and system specific memory allocation.
+
+ If this happens, there are two cases. If the pointed-to type of
+ the accessing pointer is larger than the declaration type of the
+ object, the behavior is undefined. Similarly, if the pointer
+ value has an incompatible alignment at runtime, the behavior is
+ undefined. Otherwise, the value read back through the pointer is
+ implementation specific. These system specific values may include
+ trap representations.
+
Type:
(expr : @a#)# : @a