From 0363faeec8c24ff2ffe5fd64b1b52308bdb30cdb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Jan 2014 15:12:34 -0800 Subject: [PATCH] fix(frontends/lean/scanner): assertion violation, and add more tests Signed-off-by: Leonardo de Moura --- src/frontends/lean/scanner.cpp | 2 +- tests/lean/scan_error1.lean | 4 ++++ tests/lean/scan_error1.lean.expected.out | 3 +++ tests/lean/scan_error2.lean | 1 + tests/lean/scan_error2.lean.expected.out | 3 +++ tests/lean/scan_error3.lean | 1 + tests/lean/scan_error3.lean.expected.out | 3 +++ tests/lean/scan_test1.lean | 1 + tests/lean/scan_test1.lean.expected.out | 3 +++ tests/lean/scan_test2.lean | 7 +++++++ tests/lean/scan_test2.lean.expected.out | 4 ++++ 11 files changed, 31 insertions(+), 1 deletion(-) create mode 100644 tests/lean/scan_error1.lean create mode 100644 tests/lean/scan_error1.lean.expected.out create mode 100644 tests/lean/scan_error2.lean create mode 100644 tests/lean/scan_error2.lean.expected.out create mode 100644 tests/lean/scan_error3.lean create mode 100644 tests/lean/scan_error3.lean.expected.out create mode 100644 tests/lean/scan_test1.lean create mode 100644 tests/lean/scan_test1.lean.expected.out create mode 100644 tests/lean/scan_test2.lean create mode 100644 tests/lean/scan_test2.lean.expected.out diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index d7424d59cf..556e1def95 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -353,9 +353,9 @@ scanner::token scanner::read_script_block() { next(); if (c1 == '*') { char c2 = curr(); - next(); if (c2 == EOF) throw_exception("unexpected end of script"); + next(); if (c2 == ')') { return token::ScriptBlock; } else { diff --git a/tests/lean/scan_error1.lean b/tests/lean/scan_error1.lean new file mode 100644 index 0000000000..ab902fc293 --- /dev/null +++ b/tests/lean/scan_error1.lean @@ -0,0 +1,4 @@ +.. +print "begin" +.. +print "done" \ No newline at end of file diff --git a/tests/lean/scan_error1.lean.expected.out b/tests/lean/scan_error1.lean.expected.out new file mode 100644 index 0000000000..2b1577cee5 --- /dev/null +++ b/tests/lean/scan_error1.lean.expected.out @@ -0,0 +1,3 @@ + Set: pp::colors + Set: pp::unicode +Error (line: 1, pos: 3) invalid character sequence, '...' ellipsis expected diff --git a/tests/lean/scan_error2.lean b/tests/lean/scan_error2.lean new file mode 100644 index 0000000000..64b76bed64 --- /dev/null +++ b/tests/lean/scan_error2.lean @@ -0,0 +1 @@ +(* print("from lua") \ No newline at end of file diff --git a/tests/lean/scan_error2.lean.expected.out b/tests/lean/scan_error2.lean.expected.out new file mode 100644 index 0000000000..c4b6a53015 --- /dev/null +++ b/tests/lean/scan_error2.lean.expected.out @@ -0,0 +1,3 @@ + Set: pp::colors + Set: pp::unicode +Error (line: 1, pos: 21) unexpected end of script diff --git a/tests/lean/scan_error3.lean b/tests/lean/scan_error3.lean new file mode 100644 index 0000000000..a45f48fe58 --- /dev/null +++ b/tests/lean/scan_error3.lean @@ -0,0 +1 @@ +(* print("from lua") * \ No newline at end of file diff --git a/tests/lean/scan_error3.lean.expected.out b/tests/lean/scan_error3.lean.expected.out new file mode 100644 index 0000000000..3adacfe196 --- /dev/null +++ b/tests/lean/scan_error3.lean.expected.out @@ -0,0 +1,3 @@ + Set: pp::colors + Set: pp::unicode +Error (line: 1, pos: 23) unexpected end of script diff --git a/tests/lean/scan_test1.lean b/tests/lean/scan_test1.lean new file mode 100644 index 0000000000..360dca6d53 --- /dev/null +++ b/tests/lean/scan_test1.lean @@ -0,0 +1 @@ +print 10.0. \ No newline at end of file diff --git a/tests/lean/scan_test1.lean.expected.out b/tests/lean/scan_test1.lean.expected.out new file mode 100644 index 0000000000..4c6d370253 --- /dev/null +++ b/tests/lean/scan_test1.lean.expected.out @@ -0,0 +1,3 @@ + Set: pp::colors + Set: pp::unicode +10 diff --git a/tests/lean/scan_test2.lean b/tests/lean/scan_test2.lean new file mode 100644 index 0000000000..ecbb75f5b0 --- /dev/null +++ b/tests/lean/scan_test2.lean @@ -0,0 +1,7 @@ +(* + a = 1 * +2 + print("a") +*) + +prnt "fail" \ No newline at end of file diff --git a/tests/lean/scan_test2.lean.expected.out b/tests/lean/scan_test2.lean.expected.out new file mode 100644 index 0000000000..70a136889d --- /dev/null +++ b/tests/lean/scan_test2.lean.expected.out @@ -0,0 +1,4 @@ + Set: pp::colors + Set: pp::unicode +a +Error (line: 7, pos: 0) Command expected