|
|
|---|
|
|
|
|---|
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