		Search-engine friendly clone of the ACL2 documentation.

Language

Computation-states

A model of C computation states.

We provide a model of the states of computation of an executing C program, along with operations to manipulate these computation states.

Subtopics

Write-object: Write an object in the computation state.
Objdesign-of-var: Object designator of a variable.
Create-var: Create a variable in a computation state.
Compustate-scopes-numbers: Ordered list of the numbers of scopes in the call stack frames.
Read-object: Read an object in the computation state.
Compustate: Fixtype of computation states.
Enter-scope: Enter a scope.
Frame: Fixtype of frames.
Exit-scope: Exit a scope.
Read-object-of-create-var: How read-object changes under create-var.
Compustate-scopes-numbers-aux
Compustate-option: Fixtype of optional computation states.
Push-frame: Push a frame onto a computation state's call stack.
Read-object-of-write-object: How read-object changes under write-object.
Pop-frame: Pop a frame from a computation state's non-empty call stack.
Compustate-frames-number: Number of frames in the call stack of a computation state.
Exit-scope-of-write-object: How write-object changes under exit-scope.
Compustate-option-result: Fixtype of optional computation states and errors.
Scope-list-result: Fixtype of lists of scopes and errors.
Not-errorp-of-write-object-of-exit-scope: If writing an object not in the top scope causes no error, neither does writing the object after exiting the scope.
Compustate-result: Fixtype of computation states and errors.
Scope-result: Fixtype of scopes and errors.
Pop-frame-of-write-object: How write-object changes under pop-frame.
Compustate-top-frame-scopes-number: Number of scopes in the top frame of a computation state with a non-empty call stack.
Not-errorp-of-write-object-of-pop-frame: If writing an object not in the top frame causes no error, neither does writing the object after popping the frame.
Read-object-of-exit-scope: Invariance of read-object under exit-scope, provided that the object is not in the exited scope.
Heap: Fixtype of heaps.
Top-frame: Top frame of a computation state's call stack.
Read-object-of-pop-frame: Invariance of read-object under pop-frame, provided that the object is not in the popped frame.
Scope: Fixtype of variable scopes.
Objdesign-of-var-of-create-var: How objdesign-of-var changes under create-var.
Scope-list: Fixtype of lists of variable scopes.
Push/pop/top-frame-theorems: Theorems relating push-frame, pop-frame, and top-frame.
Objdesign-of-var-of-write-object: How objdesign-of-var changes under write-object.
Frame-list: Fixtype of lists of frames.
Compustatep-of-write-object-of-objdesign-of-var: If objdesign-of-var succeeds, write-object returns a computation state (not an error).
Valuep-of-read-object-of-objdesign-of-var: If objdesign-of-var succeeds, read-object returns a value (not an error).
Read-object-of-enter-scope: Invariance of read-object under enter-scope.
Objdesign-of-var-of-enter-scope: How objdesign-of-var changes under enter-scope.
Entr/exit-scope-theorems: Theorems relating enter-scope and exit-scope.