Adding undefined

Also interpreter now supports reading and writing of basic registers (i.e with no subranges yet)

2 files changed, 10 insertions, 1 deletions

diff --git a/src/lem_interp/ast.lem b/src/lem_interp/ast.lem
index aebbebc6..51831898 100644
--- a/src/lem_interp/ast.lem
+++ b/src/lem_interp/ast.lem
@@ -8,7 +8,7 @@ type l =
   | Trans of string * option l
   | Range of num * num
 
- val disjoint : forall 'a . set 'a -> set 'a -> bool
+val disjoint : forall 'a . set 'a -> set 'a -> bool
 let disjoint s1 s2 = 
   let diff = s1 inter s2 in
   diff = Pervasives.empty
@@ -122,6 +122,7 @@ type lit =  (* Literal constant *)
  | L_num of num (* natural number constant *)
  | L_hex of string (* bit vector constant, C-style *)
  | L_bin of string (* bit vector constant, C-style *)
+ | L_undef (* constant representing undefined values *)
  | L_string of string (* string constant *)
 
 
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index face5e27..f7e473c1 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -396,6 +396,14 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level lexp =
     | (LEXP_id id,true) -> 
       match in_env l_env id with
       | Some (V_boxref n) -> (Value (V_lit L_unit), update_mem l_mem n value, l_env)
+      | None -> 
+	match in_reg regs id with
+	| Some regf -> (Action (Write_reg regf None value) (Frame (Id "0") (E_id (Id "0")) l_env l_mem Top),l_mem,l_env)
+	| None -> (*Should check memory here*)
+	  let (Mem c m) = l_mem in
+	  let l_mem = (Mem (c+1) m) in
+	  (Value (V_lit L_unit), update_mem l_mem c value, (id,(V_boxref c))::l_env)
+        end
       end 
    end