LARA This is an old revision of the document! Semantics of Field Reads and Writes What is x = y.f; x.f = y; Function associated with list, function update. Null pointer checks.