Open erniecohen opened 5 months ago
I can't reproduce this on 4.6, neither in the IDE nor the CLI:
rwillems@bcd0745419f2 Sync % dafny --version
4.6.0
rwillems@bcd0745419f2 Sync % dafny verify ./temp.dfy
Temp/temp.dfy(4,6): Error: the type of this const is underspecified
|
4 | const c := T.c
| ^
1 resolution/type errors detected in temp.dfy
rwillems@bcd0745419f2 Sync % dafny verify --type-system-refresh ./temp.dfy
Dafny program verifier finished with 0 verified, 0 errors
Closing this issue as I can't reproduce it either. Feel free to push again if needed.
I should have mentioned that this is with --type-system-refresh --general-newtypes.
With the above I can reproduce it. Note that just --type-system-refresh
is not enough
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](IEnumerableb0()
at Microsoft.Dafny.LanguageServer.Language.CacheExtensions.ProfileAndPruneCache[T,Key,Value](PruneIfNotUsedSinceLastPruneCacheb__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()
1 coll, Action
1 action) at Microsoft.Dafny.BottomUpVisitor.Visit(Expression expr) at Microsoft.Boogie.CollectionExtensions.ForEach[T](IEnumerable1 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(List1 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.<>n0(CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Language.CachingResolver.<>cDisplayClass5_0.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.<>cDisplayClass5_0.<What type of operating system are you experiencing the problem on?
Mac