|
|
|---|
|
|
|
|---|
Error values used in the formalization of C.
In our formal static and dynamic semantics of C, our ACL2 functions return error values in certain circumstances. An example is when a run-time check in our defensive dynamic semantics fails, e.g. due to a value having the wrong type for an operator. Another example is when some static constraint fail, e.g. a variable is referenced in some code without being in scope.
These ACL2 functions return different kinds of values when they do not fail. Thus, the return types of these functions include both those values and error values.
We introduce a fixtype for error values, which is used in all those ACL2 functions.
We also introduce a macro to generate a fixtype that consists of
a specified fixtype for the non-error values
and the error fixtype.
This is somewhat analogous to Rust's
We actually plan to use fty::defresult and to eventually remove this code here.