|author||Ori Bernstein <firstname.lastname@example.org>||2017-01-29 23:54:46 -0800|
|committer||Ori Bernstein <email@example.com>||2017-01-29 23:54:46 -0800|
Add specification of accessing pointers via casts.
1 files changed, 12 insertions, 0 deletions
diff --git a/doc/lang.txt b/doc/lang.txt
index d20490e..76ea677 100644
@@ -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.
(expr : @a#)# : @a