diff options
| author | Alasdair Armstrong | 2019-05-29 13:59:28 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-05-29 13:59:28 +0100 |
| commit | 21f2d6abb344b56ea26aff3169aebf69a0d99c8a (patch) | |
| tree | 130c342d6479eec9ecefd3224256f6985e939365 /src | |
| parent | fd00008838c6398bf1678372c53b4749f644a1a9 (diff) | |
Fix sail_truncate error message in SMT
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/jib_smt.ml | 2 | ||||
| -rw-r--r-- | src/reporting.ml | 2 |
2 files changed, 2 insertions, 2 deletions
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) |