Improve Verilog error messages

2 files changed, 11 insertions, 2 deletions

diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index 41e7359..426a7e6 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -167,7 +167,13 @@ Definition transf_instr (n : node) (i : instruction) (s : state) : mon node :=
     | Some instr => add_instr n n' s instr
     | _ => Error (Errors.msg "Instruction is not implemented.")
     end
-  | _ => Error (Errors.msg "The other things were also not implemented")
+  | Hload _ _ _ _ _ => Error (Errors.msg "Load not implemented.")
+  | Hstore _ _ _ _ _ => Error (Errors.msg "Store not implemented.")
+  | Hinst _ _ _ _ => Error (Errors.msg "Call not implemented.")
+  | Htailcall _ _ _ => Error (Errors.msg "Tailcall not implemented.")
+  | Hcond _ _ _ _ => Error (Errors.msg "Cond not implemented.")
+  | Hjumptable _ _ => Error (Errors.msg "Jumptable not implemented.")
+  | Hfinish _ => OK n s
   end.
 
 Definition make_stm_cases (s : positive * stmnt) : expr * stmnt :=
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 225d35d..09eb914 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -43,7 +43,10 @@ Definition posToValue (p : positive) : value :=
   mkvalue size (Word.posToWord size p).
 
 Definition intToValue (i : Integers.int) : value :=
-  mkvalue 32%nat (Word.natToWord 32%nat (Z.to_nat (Integers.Int.unsigned i))).
+  mkvalue 32%nat (Word.ZToWord 32%nat (Integers.Int.unsigned i)).
+
+Definition valueToZ (v : value) : Z :=
+  Word.uwordToZ v.(vword).
 
 Definition state : Type := PositiveMap.t value * PositiveMap.t value.