# Representation

A representation of C in ACL2.

We define ACL2 representations of C constructs,
which is a shallow embedding of (a subset of) C in ACL2.

This is related to, but different from,
the deep embedding of C in ACL2,
i.e. the formalization of (a subset of) C in ACL2.

This shallow embedding is used by ATC to generate C from ACL2.
It could be also used by a future lifter from C code to ACL2;
it is more general than code generation,
as it is also usable for code lifting.
For this reason, we are in the process of moving this shallow embedding
from the atc subdirectory to this representation subdirectory.

### Subtopics

- Representation-of-integer-operations
- A representation of C integer operations in ACL2.
- Atc-arrays
- A model of shallowly embedded C arrays for ATC.
- Representation-of-integers
- A representation of C integers in ACL2.
- Representation-of-integer-conversions
- A representation of C integer conversions in ACL2.
- Pointed-integers
- An ACL2 representation of C integers manipulated by pointers.