From ccb27e29fed5a879cbb6b10ce9882d8800b258e6 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Tue, 8 Mar 2016 17:41:35 +0000
Subject: Return undefined value on reads of uninitialised memory

---
 src/lem_interp/interp_interface.lem | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 6fe999c9..dae1ec80 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -952,13 +952,19 @@ val register_value_ones : direction -> nat -> nat -> register_value
 let register_value_ones dir width start_index = 
   register_value Bitl_one dir width start_index
 
+val byte_lifted_undef : byte_lifted
+let byte_lifted_undef = Byte_lifted (List.replicate 8 Bitl_undef)
+
 val byte_lifted_unknown : byte_lifted
 let byte_lifted_unknown = Byte_lifted (List.replicate 8 Bitl_unknown)
-
+  
 val memory_value_unknown : nat (*the number of bytes*) -> memory_value
 let memory_value_unknown (width:nat) : memory_value = 
   List.replicate width byte_lifted_unknown 
 
+val memory_value_undef : nat (*the number of bytes*) -> memory_value
+let memory_value_undef (width:nat) : memory_value = 
+  List.replicate width byte_lifted_undef 
 
 (* lengths *)  
 
-- 
cgit v1.2.3