From 92b48e2aa6d24d1ad487c1d2a3644a57966c765e Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 3 May 2019 09:25:48 +0200
Subject: rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 mppa_k1c/TargetPrinter.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'mppa_k1c/TargetPrinter.ml')

diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 62b02f58..156b16d0 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -160,9 +160,7 @@ module Target (*: TARGET*) =
   *)
 (* Offset part of a load or store *)
 
-    let offset oc = let open Asmvliw in function
-    | Ofsimm n -> ptrofs oc n
-    | Ofslow(id, ofs) -> fprintf oc "%%lo(%a)" symbol_offset (id, ofs)
+    let offset oc n = ptrofs oc n 
 
     let addressing oc = function
     | AOff ofs -> offset oc ofs
-- 
cgit