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

Crash when Boogie receives SIGINT #716

Open
keyboardDrummer opened this issue Apr 13, 2023 · 0 comments
Open

Crash when Boogie receives SIGINT #716

keyboardDrummer opened this issue Apr 13, 2023 · 0 comments
Labels

Comments

@keyboardDrummer
Copy link
Collaborator

When verifying a closed-source Dafny program and pressing ctrl+C in the shell, the following exception occurs.

Unhandled exception. System.AggregateException: One or more errors occurred. (Object reference not set to an instance of an object.)
 ---> System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Boogie.SMTLib.SMTLibProcess.Send(String cmd)
   at Microsoft.Boogie.SMTLib.SMTLibProcess.PingPong()
   at Microsoft.Boogie.Checker.GoBackToIdle()
   at VC.SplitAndVerifyWorker.DoWork(Int32 iteration, Split split, CancellationToken cancellationToken)
   at VC.SplitAndVerifyWorker.DoWorkForMultipleIterations(Split split, CancellationToken cancellationToken)
   at VC.SplitAndVerifyWorker.WorkUntilDone(CancellationToken cancellationToken)
   at VC.VCGen.VerifyImplementation(ImplementationRun run, VerifierCallback callback, CancellationToken cancellationToken)
   at VC.ConditionGeneration.VerifyImplementation(ImplementationRun run, CancellationToken cancellationToken)
   at Microsoft.Boogie.ExecutionEngine.VerifyImplementationWithoutCaching(ProcessedProgram processedProgram, PipelineStatistics stats, ErrorReporterDelegate er, CancellationToken cancellationToken, String programId, Implementation impl, TextWriter traceWriter)
   at Microsoft.Boogie.ExecutionEngine.VerifyImplementation(ProcessedProgram processedProgram, PipelineStatistics stats, ErrorReporterDelegate er, CancellationToken cancellationToken, Implementation implementation, String programId, TextWriter traceWriter)
   at Microsoft.Boogie.ExecutionEngine.<>c__DisplayClass38_0.<<VerifyEachImplementation>b__1>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Boogie.ExecutionEngine.<>c__DisplayClass38_0.<<VerifyEachImplementation>b__1>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Boogie.ExecutionEngine.VerifyEachImplementation(TextWriter output, ProcessedProgram processedProgram, PipelineStatistics stats, String programId, ErrorReporterDelegate er, String requestId, Implementation[] stablePrioritizedImpls)
   at Microsoft.Boogie.ExecutionEngine.InferAndVerify(TextWriter output, Program program, PipelineStatistics stats, String programId, ErrorReporterDelegate er, String requestId)
   at Microsoft.Dafny.Main.BoogiePipelineWithRerun(TextWriter output, ExecutionEngine engine, Program program, String bplFileName, String programId)
   at Microsoft.Dafny.Main.BoogieOnce(TextWriter output, ExecutionEngine engine, String baseFile, String moduleName, Program boogieProgram, String programId)
   at Microsoft.Dafny.DafnyDriver.BoogieOnceWithTimerAsync(TextWriter output, String baseName, String programId, String moduleName, Program program)
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass20_0.<<BoogieAsync>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass20_0.<<BoogieAsync>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.DafnyDriver.BoogieAsync(String baseName, IEnumerable`1 boogiePrograms, String programId)
   at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId)
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args)
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass10_0.<Main>b__0()
   at System.Threading.Thread.StartCallback()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant