From 01df2ff845f85f1b90d2f5dcc2b3efc5cf470904 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9on=20Frenot?= <leon.frenot@ens-lyon.fr>
Date: Mon, 9 Dec 2024 15:50:22 +0000
Subject: [PATCH] updated test

---
 test/lean/bitfield.lean.expected | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/test/lean/bitfield.lean.expected b/test/lean/bitfield.lean.expected
index a92fe23f3..4a27a3c18 100644
--- a/test/lean/bitfield.lean.expected
+++ b/test/lean/bitfield.lean.expected
@@ -5,7 +5,7 @@ structure cr_type  where
 
 
 def undefined_cr_type (lit : Unit) : cr_type :=
-  sorry
+  sorry /- internal_plet -/
 
 def Mk_cr_type (v : BitVec 8) : cr_type :=
   {bits := v}
@@ -16,8 +16,8 @@ def _get_cr_type_bits (v : cr_type) : BitVec 8 :=
 def _update_cr_type_bits (v : cr_type) (x : BitVec 8) : cr_type :=
   {v with bits := (Sail.BitVec.update_subrange v.bits (HSub.hSub 8 1) 0 x)}
 
-def _set_cr_type_bits (r_ref : Register cr_type) (v : BitVec 8) : Unit :=
-  sorry
+def _set_cr_type_bits (r_ref : register_ref Unit Unit cr_type) (v : BitVec 8) : Unit :=
+  sorry /- internal_plet -/
 
 def _get_cr_type_CR0 (v : cr_type) : BitVec 4 :=
   (Sail.BitVec.extractLsb v.bits 7 4)
@@ -25,8 +25,8 @@ def _get_cr_type_CR0 (v : cr_type) : BitVec 4 :=
 def _update_cr_type_CR0 (v : cr_type) (x : BitVec 4) : cr_type :=
   {v with bits := (Sail.BitVec.update_subrange v.bits 7 4 x)}
 
-def _set_cr_type_CR0 (r_ref : Register cr_type) (v : BitVec 4) : Unit :=
-  sorry
+def _set_cr_type_CR0 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 4) : Unit :=
+  sorry /- internal_plet -/
 
 def _get_cr_type_CR1 (v : cr_type) : BitVec 2 :=
   (Sail.BitVec.extractLsb v.bits 3 2)
@@ -34,8 +34,8 @@ def _get_cr_type_CR1 (v : cr_type) : BitVec 2 :=
 def _update_cr_type_CR1 (v : cr_type) (x : BitVec 2) : cr_type :=
   {v with bits := (Sail.BitVec.update_subrange v.bits 3 2 x)}
 
-def _set_cr_type_CR1 (r_ref : Register cr_type) (v : BitVec 2) : Unit :=
-  sorry
+def _set_cr_type_CR1 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit :=
+  sorry /- internal_plet -/
 
 def _get_cr_type_CR3 (v : cr_type) : BitVec 2 :=
   (Sail.BitVec.extractLsb v.bits 1 0)
@@ -43,8 +43,8 @@ def _get_cr_type_CR3 (v : cr_type) : BitVec 2 :=
 def _update_cr_type_CR3 (v : cr_type) (x : BitVec 2) : cr_type :=
   {v with bits := (Sail.BitVec.update_subrange v.bits 1 0 x)}
 
-def _set_cr_type_CR3 (r_ref : Register cr_type) (v : BitVec 2) : Unit :=
-  sorry
+def _set_cr_type_CR3 (r_ref : register_ref Unit Unit cr_type) (v : BitVec 2) : Unit :=
+  sorry /- internal_plet -/
 
 def _get_cr_type_GT (v : cr_type) : BitVec 1 :=
   (Sail.BitVec.extractLsb v.bits 6 6)
@@ -52,8 +52,8 @@ def _get_cr_type_GT (v : cr_type) : BitVec 1 :=
 def _update_cr_type_GT (v : cr_type) (x : BitVec 1) : cr_type :=
   {v with bits := (Sail.BitVec.update_subrange v.bits 6 6 x)}
 
-def _set_cr_type_GT (r_ref : Register cr_type) (v : BitVec 1) : Unit :=
-  sorry
+def _set_cr_type_GT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit :=
+  sorry /- internal_plet -/
 
 def _get_cr_type_LT (v : cr_type) : BitVec 1 :=
   (Sail.BitVec.extractLsb v.bits 7 7)
@@ -61,8 +61,8 @@ def _get_cr_type_LT (v : cr_type) : BitVec 1 :=
 def _update_cr_type_LT (v : cr_type) (x : BitVec 1) : cr_type :=
   {v with bits := (Sail.BitVec.update_subrange v.bits 7 7 x)}
 
-def _set_cr_type_LT (r_ref : Register cr_type) (v : BitVec 1) : Unit :=
-  sorry
+def _set_cr_type_LT (r_ref : register_ref Unit Unit cr_type) (v : BitVec 1) : Unit :=
+  sorry /- internal_plet -/
 
 def initialize_registers : Unit :=
   ()