From 295058286407ec6c4182f2b12b27608fc7d28f95 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 10 May 2019 23:53:02 +0200
Subject: use shift 1-4 in backend

---
 mppa_k1c/ExtValues.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'mppa_k1c/ExtValues.v')

diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index 5d16b79c..1aa17458 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -2,6 +2,20 @@ Require Import Coqlib.
 Require Import Integers.
 Require Import Values.
 
+Inductive shift1_4 : Type :=
+| SHIFT1 | SHIFT2 | SHIFT3 | SHIFT4.
+
+Definition z_of_shift1_4 (x : shift1_4) :=
+  match x with
+  | SHIFT1 => 1
+  | SHIFT2 => 2
+  | SHIFT3 => 3
+  | SHIFT4 => 4
+  end.
+
+Definition int_of_shift1_4 (x : shift1_4) :=
+  Int.repr (z_of_shift1_4 x).
+
 Definition is_bitfield stop start :=
   (Z.leb start stop)
     && (Z.geb start Z.zero)
-- 
cgit