From 1b942660e5872d659bb501ef4e486c00702b7e10 Mon Sep 17 00:00:00 2001 From: David Holland Date: Mon, 20 Jan 2025 19:39:10 -0500 Subject: [PATCH] Add some more tests pursuant to #2189 (interactions of comments and Cryptol blocks) Note: these reflect the current behavior, which as discussed in the issue is not particularly desirable. They should be updated when/if the behavior is improved. --- intTests/test_parse_errors/lexer003.log.good | 3 +++ intTests/test_parse_errors/lexer003.saw | 11 +++++++++++ intTests/test_parse_errors/lexer004.log.good | 3 +++ intTests/test_parse_errors/lexer004.saw | 11 +++++++++++ intTests/test_parse_errors/lexer005.log.good | 5 +++++ intTests/test_parse_errors/lexer005.saw | 11 +++++++++++ intTests/test_parse_errors/lexer006.log.good | 3 +++ intTests/test_parse_errors/lexer006.saw | 15 +++++++++++++++ 8 files changed, 62 insertions(+) create mode 100644 intTests/test_parse_errors/lexer003.log.good create mode 100644 intTests/test_parse_errors/lexer003.saw create mode 100644 intTests/test_parse_errors/lexer004.log.good create mode 100644 intTests/test_parse_errors/lexer004.saw create mode 100644 intTests/test_parse_errors/lexer005.log.good create mode 100644 intTests/test_parse_errors/lexer005.saw create mode 100644 intTests/test_parse_errors/lexer006.log.good create mode 100644 intTests/test_parse_errors/lexer006.saw diff --git a/intTests/test_parse_errors/lexer003.log.good b/intTests/test_parse_errors/lexer003.log.good new file mode 100644 index 000000000..bc84b49cf --- /dev/null +++ b/intTests/test_parse_errors/lexer003.log.good @@ -0,0 +1,3 @@ + Loading file "lexer003.saw" + Parse error at lexer003.saw:9:20-9:22: Unexpected `*/' +FAILED diff --git a/intTests/test_parse_errors/lexer003.saw b/intTests/test_parse_errors/lexer003.saw new file mode 100644 index 000000000..793c5dda6 --- /dev/null +++ b/intTests/test_parse_errors/lexer003.saw @@ -0,0 +1,11 @@ +// Currently comment delimiters in Cryptol blocks are not recognized +// by the saw-script lexer; they're treated as part of the block and +// handled by the Cryptol lexer downstream. This has some odd +// consequences. See issue #2189. +// +// This currently fails with an unexpected end-of-comment because the +// open-comment isn't seen. + +let x = {{ /* 3 }} */; + + diff --git a/intTests/test_parse_errors/lexer004.log.good b/intTests/test_parse_errors/lexer004.log.good new file mode 100644 index 000000000..b67019d2b --- /dev/null +++ b/intTests/test_parse_errors/lexer004.log.good @@ -0,0 +1,3 @@ + Loading file "lexer004.saw" + Parse error at lexer004.saw:9:20-9:21: Unexpected `+' +FAILED diff --git a/intTests/test_parse_errors/lexer004.saw b/intTests/test_parse_errors/lexer004.saw new file mode 100644 index 000000000..30d345b64 --- /dev/null +++ b/intTests/test_parse_errors/lexer004.saw @@ -0,0 +1,11 @@ +// Currently comment delimiters in Cryptol blocks are not recognized +// by the saw-script lexer; they're treated as part of the block and +// handled by the Cryptol lexer downstream. This has some odd +// consequences. See issue #2189. +// +// This currently fails with "unexpected +" because the // isn't +// seen. + +let x = {{ // 3 }} + 4; + + diff --git a/intTests/test_parse_errors/lexer005.log.good b/intTests/test_parse_errors/lexer005.log.good new file mode 100644 index 000000000..9390d8fdc --- /dev/null +++ b/intTests/test_parse_errors/lexer005.log.good @@ -0,0 +1,5 @@ + Loading file "lexer005.saw" + Stack trace: +lexer005.saw:9:9-9:11: Unclosed block comment + +FAILED diff --git a/intTests/test_parse_errors/lexer005.saw b/intTests/test_parse_errors/lexer005.saw new file mode 100644 index 000000000..a2c66ef8e --- /dev/null +++ b/intTests/test_parse_errors/lexer005.saw @@ -0,0 +1,11 @@ +// Currently comment delimiters in Cryptol blocks are not recognized +// by the saw-script lexer; they're treated as part of the block and +// handled by the Cryptol lexer downstream. This has some odd +// consequences. See issue #2189. +// +// This currently fails with an unclosed block comment, because the +// end-comment inside the Cryptol block isn't matched. + +let x = /* {{ */ 2 }}; + + diff --git a/intTests/test_parse_errors/lexer006.log.good b/intTests/test_parse_errors/lexer006.log.good new file mode 100644 index 000000000..82efbab57 --- /dev/null +++ b/intTests/test_parse_errors/lexer006.log.good @@ -0,0 +1,3 @@ + Loading file "lexer006.saw" + Parse error at lexer006.saw:12:1-12:2: Unexpected `+' +FAILED diff --git a/intTests/test_parse_errors/lexer006.saw b/intTests/test_parse_errors/lexer006.saw new file mode 100644 index 000000000..113e20f3c --- /dev/null +++ b/intTests/test_parse_errors/lexer006.saw @@ -0,0 +1,15 @@ +// Currently comment delimiters in Cryptol blocks are not recognized +// by the saw-script lexer; they're treated as part of the block and +// handled by the Cryptol lexer downstream. This has some odd +// consequences. See issue #2189. +// +// This currently fails with "unexpected +" because the whole {{ }} +// is commented out and the comment only ends after _then_ seeing a +// newline. + +let x = 3 // {{ +}} * ++ 5; + + +