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

AccessViolationException durring verification #5853

Open
seebees opened this issue Oct 23, 2024 · 0 comments
Open

AccessViolationException durring verification #5853

seebees opened this issue Oct 23, 2024 · 0 comments
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@seebees
Copy link

seebees commented Oct 23, 2024

Dafny version

4.8.0

Code to produce this issue

No response

Command to run and resulting output

No response

What happened?

Added a by method to a predicate.
I now get the following error:

https://github.com/aws/aws-database-encryption-sdk-dynamodb/actions/runs/11467529623/job/31910628384?pr=1457#step:8:5242

Fatal error. System.AccessViolationException: Attempted to read or write protected memory. This is often an indication that other memory is corrupt.
   at Microsoft.Boogie.ReadOnlyVisitor.Visit(Microsoft.Boogie.Absy)
   at Microsoft.Boogie.ReadOnlyVisitor.VisitDeclarationList(System.Collections.Generic.List`1<Microsoft.Boogie.Declaration>)
   at Microsoft.Boogie.ReadOnlyVisitor.VisitProgram(Microsoft.Boogie.Program)
   at Microsoft.Boogie.BasicTypeVisitor..ctor(Microsoft.Boogie.Absy)
   at Microsoft.Boogie.Checker.Target(Microsoft.Boogie.Program, Microsoft.Boogie.ProverContext, VC.Split)
   at VC.CheckerPool.PrepareChecker(Microsoft.Boogie.Program, VC.Split, Microsoft.Boogie.Checker)
   at VC.CheckerPool+<FindCheckerFor>d__7.MoveNext()
   at System.Threading.ExecutionContext.RunFromThreadPoolDispatchLoop(System.Threading.Thread, System.Threading.ExecutionContext, System.Threading.ContextCallback, System.Object)
   at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1+AsyncStateMachineBox`1[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[VC.CheckerPool+<FindCheckerFor>d__7, Boogie.VCGeneration, Version=3.2.3.0, Culture=neutral, PublicKeyToken=null]].MoveNext(System.Threading.Thread)
   at System.Threading.ThreadPoolWorkQueue.Dispatch()
   at System.Threading.PortableThreadPool+WorkerThread.WorkerThreadStart()
   at System.Threading.Thread.StartCallback()

Here is the PR: aws/aws-database-encryption-sdk-dynamodb#1457

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

Linux

@seebees seebees added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Oct 23, 2024
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

1 participant