This is an old revision of the document!
Semantics of Field Reads and Writes
How to model field assignment ?
What about null pointer checks?
Examples:
y = x.next.next x.next.next.prev = y (x = null | x.next == y)
Statement simplification.
Short-circuit evaluation.
Compiler intermediate representation is sometimes more convenient than source code
- or verification system can repeat the compilation process from source to relations (guarded commands)