diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-05-08 16:05:56 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-07 10:37:28 +0200 |
commit | 62c92241a69cd4597650d8408744ff922ca34245 (patch) | |
tree | 6803efd97b35d877da505f82f6a549f7c3c4051a /runtime/include | |
parent | 1f73810ca4f9754f3da8bd02f85a6e294129813a (diff) | |
download | compcert-62c92241a69cd4597650d8408744ff922ca34245.tar.gz compcert-62c92241a69cd4597650d8408744ff922ca34245.zip |
Define integer sign extension for zero bits
Just ensure sign_ext 0 x = zero. This simplifies some statements and proofs.
Diffstat (limited to 'runtime/include')
0 files changed, 0 insertions, 0 deletions