|
|
|---|
|
|
|
|---|
Representation of pointer types in the shallow embedding.
Currently, the shallow embedding does not represent pointers explicitly. That is, the ACL2 functions that represent C functions always operate on values, including array values, not on pointers to them. However, these manipulations on values may represent manipulations on pointers, more precisely on the values referenced by pointers. An example is arrays, which in fact, in C, are mostly operated upon as pointers, via the array-to-pointer conversions. Other values, such as structures or integers, may be operated upon either by value or by pointer.
To distinguish the two cases, i.e. by value or by pointer, we introduce an identity wrapper star, which we can use to wrap recognizers of C values to signify that we mean pointers to those values. This wrapper can be used in guards of ACL2 functions that represent C functions, to wrap the conjuncts from which the function's parameter C types are derived.