From 192bd462233d0284fa3d5f8e8994a514b549713e Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bschommer@users.noreply.github.com>
Date: Tue, 13 Aug 2019 17:13:46 +0200
Subject: Allow Long as const result for ppc64 variant.

Since the ppc64 has 64 bit registers it is okay to have a 64 bit
constant result.
---
 powerpc/ConstpropOpproof.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'powerpc/ConstpropOpproof.v')

diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 38daefe4..8687b056 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -101,6 +101,8 @@ Proof.
   destruct a; inv H; SimplVM.
 - (* integer *)
   exists (Vint n); auto.
+- (* long *)
+  destruct (Archi.ppc64); inv H2. exists (Vlong n); auto.
 - (* float *)
   destruct (generate_float_constants tt); inv H2. exists (Vfloat f); auto.
 - (* single *)
-- 
cgit