The binary verification tools perform inlining of C specifications, to
simulate inlining that has been performed in the binary. This means that
`DONT_TRANSLATE` and `inline` are incompatible, since the binary
verification tools require C specifications for any functions that have
been inlined in the binary.
This `DONT_TRANSLATE` annotation was added with a `MODIFIES` annotation
for proofs that the C refines the abstract specification. Those proofs
have been updated such that the annotations are no longer needed.
Reverts 1fba3d9e68 and b903cb7372.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
c13f2413e9