diff options
Diffstat (limited to 'common/Values.v')
-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. |