diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-05-12 19:17:14 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-07 10:38:34 +0200 |
| commit | 659c06eb4fabce59751476ddeb2e065759f19765 (patch) | |
| tree | 651e01cae97493e517b23b1c27ffec98f2463721 | |
| parent | 8be12dfcd60d40cc5ba90657bc6a2f5528b45e55 (diff) | |
| download | compcert-659c06eb4fabce59751476ddeb2e065759f19765.tar.gz compcert-659c06eb4fabce59751476ddeb2e065759f19765.zip | |
Values: add functions for zero- and sign-extension of 64-bit integers
| -rw-r--r-- | common/Values.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/common/Values.v b/common/Values.v index 2eb778a5..52474f99 100644 --- a/common/Values.v +++ b/common/Values.v @@ -783,6 +783,18 @@ Definition rolml (v: val) (amount: int) (mask: int64): val := | _ => Vundef end. +Definition zero_ext_l (nbits: Z) (v: val) : val := + match v with + | Vlong n => Vlong(Int64.zero_ext nbits n) + | _ => Vundef + end. + +Definition sign_ext_l (nbits: Z) (v: val) : val := + match v with + | Vlong n => Vlong(Int64.sign_ext nbits n) + | _ => Vundef + end. + (** Comparisons *) Section COMPARISONS. |