		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Read-write-variables

Functions to read and write variables.

These used to be part of the dynamic semantics, which was since then extended and generalized to no longer use these functions. However, these functions are still used by ATC, and so for now we keep them here. We may remove them altogether in the future, after changing ATC to no longer used them.

Subtopics

Write-auto-var: Write a variable in automatic storage.
Read-auto-var: Read a variable in automatic storage.
Write-static-var: Write a varible in static storage.
Write-var: Write a variable in the computation state.
Read-var: Read a variable in a computation state.
Read-static-var: Read a variable in static storage.
Objdesign-of-var-and-read/write-var-theorems: Some theorems about objdesign-of-var and the functions to read and write variables.
Read-object-of-objdesign-of-var-to-read-var: Equivalence of read-object and read-var for object designators of variables.
Write-object-of-objdesign-of-var-to-write-var: Equivalence of write-object and write-var for object designators of variables.