Erase ghost code in a separate phase #19231
Annotations
10 errors and 10 warnings
|
Run integration tests (non-Windows)
The name 'y' does not exist in the current context
|
|
Run integration tests (non-Windows)
The name 'y' does not exist in the current context
|
|
Run integration tests (non-Windows)
The name 'y' does not exist in the current context
|
|
Run integration tests (non-Windows)
The name 'y' does not exist in the current context
|
|
Run integration tests (non-Windows)
undefined: y
|
|
Run integration tests (non-Windows)
The name 'y' does not exist in the current context
|
|
Run integration tests (non-Windows)
The name 'y' does not exist in the current context
|
|
Run integration tests (non-Windows)
The name 'y' does not exist in the current context
|
|
Run integration tests (non-Windows)
The name 'y' does not exist in the current context
|
|
Run integration tests (non-Windows)
undefined: y
|
|
Run integration tests (non-Windows):
Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
|
|
Run integration tests (non-Windows):
Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
|
|
Run integration tests (non-Windows):
Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
|
|
Run integration tests (non-Windows)
Unreachable code detected
|
|
Run integration tests (non-Windows)
Unreachable code detected
|
|
Run integration tests (non-Windows)
Unreachable code detected
|
|
Run integration tests (non-Windows)
Unreachable code detected
|
|
Run integration tests (non-Windows)
Unreachable code detected
|
|
Run integration tests (non-Windows)
Unreachable code detected
|
|
Run integration tests (non-Windows)
Unreachable code detected
|
Loading