LARA

This is an old revision of the document!


Semantics of Field Reads and Writes

How to model $x.f$ ?

How to model field assignment $x.f=y$ ?

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)