ref: 5c12b2816f7feeafb5e3e52ee287bf33927a1c74
parent: edd0699416df633c8199ecfecb48f5f18917a32d
author: Ori Bernstein <ori@eigenstate.org>
date: Sun Jan 29 18:54:46 EST 2017
Add specification of accessing pointers via casts.
--- a/doc/lang.txt
+++ b/doc/lang.txt
@@ -1328,6 +1328,18 @@
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