internal error on static constants in newtypes based on bitvectors #5371
Labels
during 2: compilation of correct program
Dafny rejects a valid program during compilation
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: resolver
Resolution and typechecking
Dafny version
4.6
Code to produce this issue
Command to run and resulting output
What happened?
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Dafny.DetectUnderspecificationVisitor.VisitOneExpr(Expression expr)
at Microsoft.Boogie.CollectionExtensions.ForEach[T](IEnumerable
1 coll, Action
1 action)at Microsoft.Dafny.BottomUpVisitor.Visit(Expression expr)
at Microsoft.Boogie.CollectionExtensions.ForEach[T](IEnumerable
1 coll, Action
1 action)at Microsoft.Dafny.BottomUpVisitor.Visit(Expression expr)
at Microsoft.Dafny.UnderspecificationDetector.CheckExpression(Expression expr, UnderspecificationDetectorContext context)
at Microsoft.Dafny.UnderspecificationDetector.CheckMember(MemberDecl member)
at Microsoft.Dafny.UnderspecificationDetector.CheckMembers(TopLevelDeclWithMembers cl)
at Microsoft.Dafny.UnderspecificationDetector.Check(List
1 declarations) at Microsoft.Dafny.ModuleResolver.ResolveTopLevelDecls_Core(List
1 declarations, Graph1 datatypeDependencies, Graph
1 codatatypeDependencies, String moduleDescription, Boolean isAnExport)at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, String exportSetName)
at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation)
at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
at Microsoft.Dafny.LanguageServer.Language.CachingResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.CachingResolver.<>n__0(CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.CachingResolver.<>c__DisplayClass5_0.b__0()
at Microsoft.Dafny.LanguageServer.Language.CacheExtensions.ProfileAndPruneCache[T,Key,Value](PruneIfNotUsedSinceLastPruneCache
2 cache, Func
1 useCache, TelemetryPublisherBase telemetryPublisher, String programName, String activity)at Microsoft.Dafny.LanguageServer.Language.CachingResolver.Resolve(CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(Compilation compilation, Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.TextDocumentLoader.ResolveInternal(Compilation compilation, Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.TextDocumentLoader.<>c__DisplayClass5_0.<b__0>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.TextDocumentLoader.ResolveAsync(Compilation compilation, Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.ResolveAsync()
What type of operating system are you experiencing the problem on?
Mac
The text was updated successfully, but these errors were encountered: