Skip to content

AccessViolationException durring verification #5853

@seebees

Description

@seebees

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

    Type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions