From f9282ab5dec29d7ec99d473d013d32b41a0b8dbc Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 7 Aug 2018 11:02:09 +0100
Subject: Improve cast introduction for Lem Handles mutable variables and
 conditionals (there are still some corner cases that don't appear in Aarch64
 to do). The pretty printer is now back to preferring to use concrete types,
 but has a special case for casts to print more general types.

---
 lib/mono_rewrites.sail | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index aa8d05cd..9e837e10 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -29,7 +29,8 @@ function extsv(v) = exts_vec(sizeof('m),v)
 
 /* This is generated internally to deal with case splits which reveal the size
    of a bitvector */
-val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
 
 /* Definitions for the rewrites */
 
-- 
cgit v1.2.3