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

Case constant causing Crash? #4000

Closed
DavePearce opened this issue May 12, 2023 · 0 comments · Fixed by #4170
Closed

Case constant causing Crash? #4000

DavePearce opened this issue May 12, 2023 · 0 comments · Fixed by #4170
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@DavePearce
Copy link

DavePearce commented May 12, 2023

Dafny version

4.1.0

Code to produce this issue

module Gas {
    type State = ()
    const STATICCALL : nat := 0xfa

    function f(op: nat, s: State): State
    {
        match op
            case STATICCALL => s
            case _ => s
    }
}

Command to run and resulting output

dafny-4.1/dafny BugTest.dfy

What happened?

Unhandled exception. System.AggregateException: One or more errors occurred. (Value cannot be null. (Parameter 'source'))
 ---> System.ArgumentNullException: Value cannot be null. (Parameter 'source')
   at System.Linq.ThrowHelper.ThrowArgumentNullException(ExceptionArgument argument)
   at System.Linq.Enumerable.Select[TSource,TResult](IEnumerable`1 source, Func`2 selector)
   at Microsoft.Dafny.Substituter.<>c__DisplayClass7_1.<Substitute>g__SubstituteForPattern|0(ExtendedPattern pattern)
   at Microsoft.Dafny.Substituter.Substitute(Expression expr)
   at Microsoft.Dafny.Translator.GetFunctionAxiom(Function f, Expression body, List`1 lits)
   at Microsoft.Dafny.Translator.AddFunctionAxiom(Function boogieFunction, Function f, Expression body)
   at Microsoft.Dafny.Translator.AddClassMember_Function(Function f)
   at Microsoft.Dafny.Translator.AddFunction_Top(Function f, Boolean includeAllMethods)
   at Microsoft.Dafny.Translator.AddClassMembers(TopLevelDeclWithMembers c, Boolean includeAllMethods, Boolean includeInformationAboutType)
   at Microsoft.Dafny.Translator.AddTypeDecl(RevealableTypeDecl d)
   at Microsoft.Dafny.Translator.DoTranslation(Program p, ModuleDefinition forModule)
   at Microsoft.Dafny.Translator.Translate(Program p, ErrorReporter reporter, TranslatorFlags flags)+MoveNext()
   at Microsoft.Dafny.DafnyDriver.Translate(ExecutionEngineOptions options, Program dafnyProgram)+MoveNext()
   at System.Collections.Generic.List`1..ctor(IEnumerable`1 collection)
   at System.Linq.Enumerable.ToList[TSource](IEnumerable`1 source)
   at Microsoft.Dafny.DafnyDriver.ProcessFilesAsync(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId)
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args)
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass10_0.<Main>b__0()
   at System.Threading.Thread.StartCallback()
Aborted (core dumped)

I should add this this code compiled without problem on Dafny 4.0.

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

Linux

@DavePearce DavePearce added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label May 12, 2023
MikaelMayer added a commit that referenced this issue Jun 12, 2023
keyboardDrummer pushed a commit that referenced this issue Jun 13, 2023
This PR fixes #4000
I added the corresponding test.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
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

Successfully merging a pull request may close this issue.

1 participant