Skip to content

Erase ghost code in a separate phase #19231

Erase ghost code in a separate phase

Erase ghost code in a separate phase #19231

Triggered via pull request October 14, 2024 14:41
Status Failure
Total duration 58m 2s
Artifacts 8

msbuild.yml

on: pull_request
check-deep-tests  /  check-deep-tests
9s
check-deep-tests / check-deep-tests
integration-tests  /  populate-matrix-dimensions
0s
integration-tests / populate-matrix-dimensions
xunit-tests  /  populate-matrix-dimensions
0s
xunit-tests / populate-matrix-dimensions
singletons
59s
singletons
Matrix: integration-tests / test
Matrix: xunit-tests / build
test-coverage-analysis
0s
test-coverage-analysis
Fit to window
Zoom out
Zoom in

Annotations

27 errors and 59 warnings
singletons
Process completed with exit code 2.
xunit-tests / ubuntu-20.04 (1)
Process completed with exit code 1.
xunit-tests / win (1)
Process completed with exit code 1.
integration-tests / test (ubuntu-20.04, 2)
The name '_1_z' does not exist in the current context
integration-tests / test (ubuntu-20.04, 2)
The name '_2_bb' does not exist in the current context
integration-tests / test (ubuntu-20.04, 2)
'__default' does not contain a definition for 'F'
integration-tests / test (ubuntu-20.04, 2)
The name '_1_z' does not exist in the current context
integration-tests / test (ubuntu-20.04, 2)
The name '_3_t0' does not exist in the current context
integration-tests / test (ubuntu-20.04, 2)
The name '_1_z' does not exist in the current context
integration-tests / test (ubuntu-20.04, 2)
The name '_5_t1' does not exist in the current context
integration-tests / test (ubuntu-20.04, 2)
The name '_1_z' does not exist in the current context
integration-tests / test (ubuntu-20.04, 2)
The name '_1_z' does not exist in the current context
integration-tests / test (ubuntu-20.04, 2)
The name '_2_bb' does not exist in the current context
integration-tests / test (ubuntu-20.04, 3)
Process completed with exit code 1.
integration-tests / test (ubuntu-20.04, 1)
Process completed with exit code 1.
integration-tests / test (ubuntu-20.04, 4)
Process completed with exit code 1.
integration-tests / test (ubuntu-20.04, 5)
The name 'y' does not exist in the current context
integration-tests / test (ubuntu-20.04, 5)
The name 'y' does not exist in the current context
integration-tests / test (ubuntu-20.04, 5)
The name 'y' does not exist in the current context
integration-tests / test (ubuntu-20.04, 5)
The name 'y' does not exist in the current context
integration-tests / test (ubuntu-20.04, 5)
undefined: y
integration-tests / test (ubuntu-20.04, 5)
The name 'y' does not exist in the current context
integration-tests / test (ubuntu-20.04, 5)
The name 'y' does not exist in the current context
integration-tests / test (ubuntu-20.04, 5)
The name 'y' does not exist in the current context
integration-tests / test (ubuntu-20.04, 5)
The name 'y' does not exist in the current context
integration-tests / test (ubuntu-20.04, 5)
undefined: y
xunit-tests / osx (1)
Process completed with exit code 1.
xunit-tests / ubuntu-20.04 (1): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / ubuntu-20.04 (1): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / ubuntu-20.04 (1): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / ubuntu-20.04 (1): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / ubuntu-20.04 (1): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / ubuntu-20.04 (1): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / ubuntu-20.04 (1): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / ubuntu-20.04 (1): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / ubuntu-20.04 (1): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / ubuntu-20.04 (1): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / ubuntu-20.04 (1): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / ubuntu-20.04 (1): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / win (1): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / win (1): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / win (1): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / win (1): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / win (1): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / win (1): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / win (1): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / win (1): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / win (1): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 2): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 2): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 2): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 2)
This label has not been referenced
integration-tests / test (ubuntu-20.04, 2)
Non-nullable field 'd' must contain a non-null value when exiting constructor. Consider adding the 'required' modifier or declaring the field as nullable.
integration-tests / test (ubuntu-20.04, 2)
This label has not been referenced
integration-tests / test (ubuntu-20.04, 2)
Non-nullable field 'd' must contain a non-null value when exiting constructor. Consider adding the 'required' modifier or declaring the field as nullable.
integration-tests / test (ubuntu-20.04, 2)
This label has not been referenced
integration-tests / test (ubuntu-20.04, 2)
Non-nullable field 'd' must contain a non-null value when exiting constructor. Consider adding the 'required' modifier or declaring the field as nullable.
integration-tests / test (ubuntu-20.04, 2)
This label has not been referenced
integration-tests / test (ubuntu-20.04, 3): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 3): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 3): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 1): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 1): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 1): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 4): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 4): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 4): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 5): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 5): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 5): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
integration-tests / test (ubuntu-20.04, 5)
Unreachable code detected
integration-tests / test (ubuntu-20.04, 5)
Unreachable code detected
integration-tests / test (ubuntu-20.04, 5)
Unreachable code detected
integration-tests / test (ubuntu-20.04, 5)
Unreachable code detected
integration-tests / test (ubuntu-20.04, 5)
Unreachable code detected
integration-tests / test (ubuntu-20.04, 5)
Unreachable code detected
integration-tests / test (ubuntu-20.04, 5)
Unreachable code detected
xunit-tests / osx (1): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / osx (1): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / osx (1): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / osx (1): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / osx (1): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / osx (1): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / osx (1): Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / osx (1): Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
xunit-tests / osx (1): Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.

Artifacts

Produced during runtime
Name Size Digest
integration-test-results-ubuntu-20.04-1 Expired
1.68 MB
sha256:c30ff237ddb83b88bc21d541d0181fb4fd7991a3c1b673390ae562c5fbf3e92e
integration-test-results-ubuntu-20.04-2 Expired
1.68 MB
sha256:eb59134aaa3e27f3c17db52c299d690fdf46f511bebea277547d7734e1899cdc
integration-test-results-ubuntu-20.04-3 Expired
1.67 MB
sha256:de1111c7775e1090440e1efa28c5f958451733887afb4fa2b343e38c61cf40c2
integration-test-results-ubuntu-20.04-4 Expired
1.68 MB
sha256:5a0e337f8681d2cdd10c6bbb4a610963e1da9ead985cd32617de5634d38b89f2
integration-test-results-ubuntu-20.04-5 Expired
1.65 MB
sha256:4486e7f5884adca56cf810afc580c822ecc75a8731422863602dcb7d63636653
unit-test-results-macos-13 Expired
3.91 MB
sha256:b00c307aa1d664c21380b49db42f7a37d20ba9991bd6d19509c45e6efa431b1e
unit-test-results-ubuntu-20.04 Expired
3.94 MB
sha256:9da175ea005a43331728ebce8c88b8ee9b0abf76338abb43bbde0fae8e9af8a3
unit-test-results-windows-2019 Expired
3.91 MB
sha256:55801c655a49b9fe29cb6a6809ab28b870b406e19178944050c08bac17fb2112