Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

dafny translate -t:cs tmp2.dfy crashes #3259

Closed
davidcok opened this issue Dec 23, 2022 · 0 comments
Closed

dafny translate -t:cs tmp2.dfy crashes #3259

davidcok opened this issue Dec 23, 2022 · 0 comments
Assignees
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@davidcok
Copy link
Collaborator

Dafny version

3.10.0+dev

Code to produce this issue

method Main() {
  print "Hi\n";
}

Command to run and resulting output

dafny translate -t:cs test.dfy

What happened?

Crashed.

Dafny program verifier finished with 0 verified, 0 errors
Unhandled exception. System.AggregateException: One or more errors occurred. (Specified method is not supported.)
---> System.NotSupportedException: Specified method is not supported.
at Microsoft.Dafny.NoCompiler.Compile(Program dafnyProgram, ConcreteSyntaxTree output) in /Users/davidcok/projects/dafny/dafny/Source/DafnyDriver/DafnyDriver.cs:line 761
at Microsoft.Dafny.DafnyDriver.CompileDafnyProgram(Program dafnyProgram, String dafnyProgramName, ReadOnlyCollection1 otherFileNames, Boolean invokeCompiler, TextWriter outputWriter) in /Users/davidcok/projects/dafny/dafny/Source/DafnyDriver/DafnyDriver.cs:line 681 at Microsoft.Dafny.DafnyDriver.Compile(String fileName, ReadOnlyCollection1 otherFileNames, Program dafnyProgram, PipelineOutcome oc, IDictionary2 moduleStats, Boolean verified) in /Users/davidcok/projects/dafny/dafny/Source/DafnyDriver/DafnyDriver.cs:line 548 at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IList1 dafnyFiles, ReadOnlyCollection1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in /Users/davidcok/projects/dafny/dafny/Source/DafnyDriver/DafnyDriver.cs:line 358 --- End of inner exception stack trace --- at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions) at System.Threading.Tasks.Task1.GetResultCore(Boolean waitCompletionNotification)
at System.Threading.Tasks.Task`1.get_Result()
at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in /Users/davidcok/projects/dafny/dafny/Source/DafnyDriver/DafnyDriver.cs:line 123
at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass10_0.

b__0() in /Users/davidcok/projects/dafny/dafny/Source/DafnyDriver/DafnyDriver.cs:line 100
at System.Threading.Thread.StartCallback()
/Users/davidcok/mybin/dafny: line 3: 40798 Abort trap: 6 /usr/local/bin/dotnet /Users/davidcok/projects/dafny/dafny/Binaries/Dafny.dll "$@"

What type of operating system are you experiencing the problem on?

Mac

@davidcok davidcok added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Dec 23, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Development

No branches or pull requests

2 participants