-
Notifications
You must be signed in to change notification settings - Fork 254
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Check for mistyped options when using
dafny run
(#5120)
Fixes #5097 ### Description - Add a warning to dafny run when users are likely to accidentally have mistyped an option name - Enable using `&>` and `&>>` in littish tests ### How has this been tested? - Added a littish test `runArgument.dfy` <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
- Loading branch information
1 parent
ba2c2b2
commit 99ad60a
Showing
6 changed files
with
85 additions
and
7 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
20 changes: 20 additions & 0 deletions
20
Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/runArgument.dfy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
// NONUNIFORM: This tests front-end behavior, and is back-end independent. | ||
// RUN: %run %s blie 2 &> %t | ||
// RUN: %run %s --blie --2 &>> %t | ||
// RUN: %run %s -- --bla --2 &>> %t | ||
// RUN: %diff "%s.expect" "%t" | ||
|
||
method Main(args: seq<string>) { | ||
if |args| != 3 { | ||
print "Expected 3 arguments, got ", |args|; | ||
} else { | ||
print args[1], " says "; | ||
if args[2] == "1" { | ||
print "hello\n"; | ||
} else if args[2] == "2" { | ||
print "howdy\n"; | ||
} else { | ||
print args[2],"\n"; | ||
} | ||
} | ||
} |
11 changes: 11 additions & 0 deletions
11
Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/runArgument.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
|
||
Dafny program verifier finished with 1 verified, 0 errors | ||
blie says howdy | ||
Argument --blie is not a Dafny option so it was interpreted as an argument to the user program, even though it starts with '--'. Move this argument to after a `--` token to silence this message. | ||
Argument --2 is not a Dafny option so it was interpreted as an argument to the user program, even though it starts with '--'. Move this argument to after a `--` token to silence this message. | ||
|
||
Dafny program verifier finished with 1 verified, 0 errors | ||
--blie says --2 | ||
|
||
Dafny program verifier finished with 1 verified, 0 errors | ||
--bla says --2 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
Add a check to `dafny run` that notifies the user when a value that was parsed as a user program argument, and which occurs before a `--` token, starts with `--`, since this indicates they probably mistyped a Dafny option name. |