From 21f2d6abb344b56ea26aff3169aebf69a0d99c8a Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 29 May 2019 13:59:28 +0100
Subject: Fix sail_truncate error message in SMT

---
 src/jib/jib_smt.ml | 2 +-
 src/reporting.ml   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 37d88053..c1a7191c 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -819,7 +819,7 @@ let builtin_sail_truncate ctx v1 v2 ret_ctyp =
      assert (Big_int.to_int c = m && m < lbits_size ctx);
      Extract (Big_int.to_int c - 1, 0, Fn ("contents", [smt_cval ctx v1]))
 
-  | _ -> builtin_type_error ctx "sail_truncate" [v2; v2] (Some ret_ctyp)
+  | _ -> builtin_type_error ctx "sail_truncate" [v1; v2] (Some ret_ctyp)
 
 let builtin_sail_truncateLSB ctx v1 v2 ret_ctyp =
   match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
diff --git a/src/reporting.ml b/src/reporting.ml
index e81fbae8..0b727836 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -145,7 +145,7 @@ let dest_err = function
   | Err_general (l, m) -> ("Error", Loc l, m)
   | Err_unreachable (l, (file, line, _, _), m) ->
      (Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line, Loc l, m ^ issues)
-  | Err_todo (l, m) -> ("Todo" ^ m, Loc l, "")
+  | Err_todo (l, m) -> ("Todo", Loc l, m)
   | Err_syntax (p, m) -> ("Syntax error", Pos p, m)
   | Err_syntax_loc (l, m) -> ("Syntax error", Loc l, m)
   | Err_lex (p, s) -> ("Lexical error", Pos p, s)
-- 
cgit v1.2.3