Atc-tag-generation
Generation of C tag declarations (currently just structures).
Subtopics
- Atc-gen-tag-member-write-thms
- Generate the theorems to rewrite
the execution of certain assignment expressions to structure writes,
for a member of a structure type.
- Atc-gen-tag-member-read-thms
- Generate the theorems to rewrite
the execution of certain pure expressions to structure reads,
for a member of a structure type.
- Atc-gen-tag-member-write-all-thms
- Generate the theorems to rewrite exec-expr-asg
with a :memberp left expression
to a structure writer,
for all the members of a structure type.
- Atc-gen-tag-declon
- Generate a C structure type declaration,
with accompanying theorems.
- Atc-gen-tag-member-read-all-thms
- Generate the theorems to rewrite
the execution of certain pure expressions to structure reads,
for all the members of a structure type.
- Atc-gen-struct-declon-list
- Generate a list of C structure declarations
from a list of member types.
- Atc-tag-generation-rules
- Rules to support proofs generated for tag declarations.