|
|
|---|
|
|
|
|---|
An ACL2 representation of C integers manipulated by pointers.
The representation of C integers in the shallow embedding
is for C integers manipulated as values.
In C, integers may also be manipulated by pointers:
that is, given a pointer to an integer,
it is possible to read and write that integer,
via the indirection operator
Pointed-to-integers are represented in the same way as by-value integers, in our shallow embedding of C in ACL2. However, we introduce specific ACL2 operations to read and write pointed-to integers, which represent C code that accesses those integers by pointer.
We define a family of functions to read pointed-to integers.
These are identities in ACL2,
but they represent applications of indirection
We also define a family of functions to write pointed-to integers. They are also identity functions, but, as explained in the ATC user documentation, they are actually applied to the term that represents the expression whose value is being assigned to the pointed-to integer.
To support some level of type checking in the ACL2 representation of C code that uses pointed-to integers, we use the star wrapper (see pointer-types) in the guards of the readers and in the return theorems of the writers: each reader takes a pointed-to integer and returns an integer, and each writer takes an integer and returns a pointed-to integer. The star wrappers are all identities, but by keeping them disabled, one can enforce some type checking at the ACL2 level. (ATC makes all the necessary type checking anyhow, but these additional checks may be useful before calling ATC, when manipulating ACL2 representations of C code.)