From 659c06eb4fabce59751476ddeb2e065759f19765 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 12 May 2019 19:17:14 +0200 Subject: Values: add functions for zero- and sign-extension of 64-bit integers --- common/Values.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'common/Values.v') 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. -- cgit