dafny icon indicating copy to clipboard operation
dafny copied to clipboard

Incorrectly generated Boogie code

Open keyboardDrummer opened this issue 5 months ago • 0 comments

Run dafny verify --type-system-refresh on:


trait Enumerable<T> extends object {}
trait Animal {}
trait Dog extends Animal {}

method foo(xs: Enumerable<Dog>) {
  var a: Enumerable<Animal> := TraitCast<Enumerable<Dog>, Enumerable<Animal>>(xs);
}

function TraitCast<T extends object, U extends object>(value: T): U {
  value as object as U
}

To get:

Unhandled exception. System.ArgumentException: Boogie program had 1 type errors:
Microsoft.Dafny.SourceOrigin: invalid type for argument 0 in application of $IsBox: ref (expected: Box)
   at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs:line 65
   at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<<VerifyUnverifiedSymbol>b__1>d.MoveNext() in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Pipeline/Compilation.cs:line 344
--- End of stack trace from previous location ---
   at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func`2 taskFilter, Nullable`1 randomSeed) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Pipeline/Compilation.cs:line 343
   at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func`2 taskFilter, Nullable`1 randomSeed) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Pipeline/Compilation.cs:line 343
   at DafnyDriver.Commands.CliCompilation.VerifyAllLazily(Nullable`1 randomSeed)+MoveNext() in /Users/runner/work/dafny/dafny/dafny/Source/DafnyDriver/CliCompilation.cs:line 275
   at DafnyDriver.Commands.CliCompilation.VerifyAllLazily(Nullable`1 randomSeed)+System.Threading.Tasks.Sources.IValueTaskSource<System.Boolean>.GetResult()
   at System.Linq.AsyncEnumerable.ToObservableObservable`1.<>c__DisplayClass2_0.<<Subscribe>g__Core|0>d.MoveNext() in /_/Ix.NET/Source/System.Linq.Async/System/Linq/Operators/ToObservable.cs:line 50
--- End of stack trace from previous location ---
   at System.Reactive.PlatformServices.ExceptionServicesImpl.Rethrow(Exception exception) in /_/Rx.NET/Source/src/System.Reactive/Internal/ExceptionServicesImpl.cs:line 16
   at System.Reactive.ExceptionHelpers.Throw(Exception exception) in /_/Rx.NET/Source/src/System.Reactive/Internal/ExceptionServices.cs:line 14
   at System.Reactive.Stubs.<>c.<.cctor>b__2_1(Exception ex) in /_/Rx.NET/Source/src/System.Reactive/Internal/Stubs.cs:line 16
   at System.Reactive.AnonymousObserver`1.OnErrorCore(Exception error) in /_/Rx.NET/Source/src/System.Reactive/AnonymousObserver.cs:line 73
   at System.Reactive.ObserverBase`1.OnError(Exception error) in /_/Rx.NET/Source/src/System.Reactive/ObserverBase.cs:line 59
   at System.Reactive.Subjects.Subject`1.OnError(Exception error) in /_/Rx.NET/Source/src/System.Reactive/Subjects/Subject.cs:line 103
   at System.Linq.AsyncEnumerable.ToObservableObservable`1.<>c__DisplayClass2_0.<<Subscribe>g__Core|0>d.MoveNext() in /_/Ix.NET/Source/System.Linq.Async/System/Linq/Operators/ToObservable.cs:line 60
--- End of stack trace from previous location ---
   at System.Linq.AsyncEnumerable.ToObservableObservable`1.<>c__DisplayClass2_0.<<Subscribe>g__Core|0>d.MoveNext() in /_/Ix.NET/Source/System.Linq.Async/System/Linq/Operators/ToObservable.cs:line 74
--- End of stack trace from previous location ---
   at System.Threading.Tasks.Task.<>c.<ThrowAsync>b__128_1(Object state)
   at System.Threading.ThreadPoolWorkQueue.Dispatch()
   at System.Threading.PortableThreadPool.WorkerThread.WorkerThreadStart()
   at System.Threading.Thread.StartCallback()

keyboardDrummer avatar Jun 25 '25 12:06 keyboardDrummer