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 /test | |
| 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 'test')
0 files changed, 0 insertions, 0 deletions