diff options
Diffstat (limited to 'backend/PPCgen.v')
| -rw-r--r-- | backend/PPCgen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/PPCgen.v b/backend/PPCgen.v index 1484a1e6..faedcb1c 100644 --- a/backend/PPCgen.v +++ b/backend/PPCgen.v @@ -80,7 +80,7 @@ Definition freg_of (r: mreg) : freg := Definition low_u (n: int) := Int.and n (Int.repr 65535). Definition high_u (n: int) := Int.shru n (Int.repr 16). -Definition low_s (n: int) := Int.cast16signed n. +Definition low_s (n: int) := Int.sign_ext 16 n. Definition high_s (n: int) := Int.shru (Int.sub n (low_s n)) (Int.repr 16). (** Smart constructors for arithmetic operations involving |