Skip to content

Commit

Permalink
Add some more tests pursuant to #2189
Browse files Browse the repository at this point in the history
(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.
  • Loading branch information
sauclovian-g committed Jan 21, 2025
1 parent 6e26035 commit 1b94266
Show file tree
Hide file tree
Showing 8 changed files with 62 additions and 0 deletions.
3 changes: 3 additions & 0 deletions intTests/test_parse_errors/lexer003.log.good
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Loading file "lexer003.saw"
Parse error at lexer003.saw:9:20-9:22: Unexpected `*/'
FAILED
11 changes: 11 additions & 0 deletions intTests/test_parse_errors/lexer003.saw
Original file line number Diff line number Diff line change
@@ -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 }} */;


3 changes: 3 additions & 0 deletions intTests/test_parse_errors/lexer004.log.good
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Loading file "lexer004.saw"
Parse error at lexer004.saw:9:20-9:21: Unexpected `+'
FAILED
11 changes: 11 additions & 0 deletions intTests/test_parse_errors/lexer004.saw
Original file line number Diff line number Diff line change
@@ -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;


5 changes: 5 additions & 0 deletions intTests/test_parse_errors/lexer005.log.good
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
Loading file "lexer005.saw"
Stack trace:
lexer005.saw:9:9-9:11: Unclosed block comment

FAILED
11 changes: 11 additions & 0 deletions intTests/test_parse_errors/lexer005.saw
Original file line number Diff line number Diff line change
@@ -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 }};


3 changes: 3 additions & 0 deletions intTests/test_parse_errors/lexer006.log.good
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Loading file "lexer006.saw"
Parse error at lexer006.saw:12:1-12:2: Unexpected `+'
FAILED
15 changes: 15 additions & 0 deletions intTests/test_parse_errors/lexer006.saw
Original file line number Diff line number Diff line change
@@ -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;



0 comments on commit 1b94266

Please sign in to comment.