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

internal error on match with static const of newtype #5405

Open
erniecohen opened this issue May 3, 2024 · 2 comments
Open

internal error on match with static const of newtype #5405

erniecohen opened this issue May 3, 2024 · 2 comments
Assignees
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

Comments

@erniecohen
Copy link

Failing code

newtype T = nat {
    static const C := 0 as T
    const V:bool := match this case C => true
}

Steps to reproduce the issue

  • Dafny version: 4.6.0.0
  • Dafny VSCode extension version: 3.3.0
  • type-system-refresh, general-traits = full

Expected behavior

not crashing

Actual behavior

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.MatchFlattener.LetBind(IdPattern var, Expression genExpr, PatternPath bodyPath)
at Microsoft.Dafny.MatchFlattener.LetBindNonWildCard(IdPattern idPattern, Expression expr, PatternPath bodyPath)
at Microsoft.Dafny.MatchFlattener.<>c__DisplayClass14_0.b__4(PatternPath path)
at System.Linq.Enumerable.SelectListIterator2.ToList() at Microsoft.Dafny.MatchFlattener.CompilePatternPathsForMatchee(MatchCompilationState state, MatchingContext context, List1 paths, Cons1 consMatchees) at Microsoft.Dafny.MatchFlattener.CompilePatternPaths(MatchCompilationState state, MatchingContext context, SinglyLinkedList1 matchees, List1 paths) at Microsoft.Dafny.MatchFlattener.CompileNestedMatchExpr(NestedMatchExpr nestedMatchExpr) at Microsoft.Dafny.MatchFlattener.<>c__DisplayClass5_0.<FlattenNode>b__0(INode node) at Microsoft.Dafny.Node.Visit(Func2 beforeChildren, Action1 afterChildren, Action1 reportError)
at Microsoft.Dafny.MatchFlattener.FlattenNode(Node root)
at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation)
at Microsoft.Dafny.ModuleResolver.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.<>c__DisplayClass5_0.b__0()
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()

@erniecohen
Copy link
Author

no crash when match is replaced with conditionals

@keyboardDrummer keyboardDrummer self-assigned this May 6, 2024
@keyboardDrummer keyboardDrummer transferred this issue from dafny-lang/ide-vscode May 6, 2024
@keyboardDrummer keyboardDrummer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label during 2: compilation of correct program Dafny rejects a valid program during compilation labels May 6, 2024
@keyboardDrummer
Copy link
Member

Moved to dafny-lang/dafny since this does not seem IDE related.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
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
Projects
None yet
Development

No branches or pull requests

2 participants