The following numerical operators are inherited from native C:
-and the binary arithmetic operators
~and binary operators
/) to fixed-point arguments.
Assignment statements may use the basic assignment operator
= or any of the assignment operators
corresponding to the binary arithmetic and logical operators listed above:
*=, etc. An application of either of the unary arithmetic operators
-- of C (which are not recognized as operators, i.e., may not occur within an expression), is also admitted as an
All arithmetic operations on registers is unbounded and performed with absolute precision. When the result of a computation is assigned to an integer or fixed-point register, the least significant fractional bits and most significant integer bits are discarded as necessary for the result to fit into the target format. This is consistent with the semantics of ACL2, which is based on unbounded rational arithmetic. However, special care must be taken with arithmetic performed on native C integer data, the inherent limitations of which are not addressed by the ACL2 translator. It is the responsibility of the programmer to avoid arithmetic overflow and match the simpler semantics of ACL2, i.e., to ensure that the results of all such computations and the values of all assigments lie within the bounds of the relevant data formats.
David Russinoff 2017-08-01