Skip to content

Erase ghost code in a separate phase #19229

Erase ghost code in a separate phase

Erase ghost code in a separate phase #19229

Triggered via pull request October 14, 2024 13:21
Status Failure
Total duration 23m 37s
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
Matrix: integration-tests / test
Matrix: xunit-tests / build
test-coverage-analysis
0s
test-coverage-analysis
Fit to window
Zoom out
Zoom in

Annotations

44 errors and 71 warnings
xunit-tests / ubuntu-20.04 (1)
Process completed with exit code 1.
xunit-tests / win (1)
Process completed with exit code 1.
xunit-tests / osx (1)
Process completed with exit code 1.
integration-tests / test (ubuntu-20.04, 3)
A local or parameter named 'x' cannot be declared in this scope because that name is used in an enclosing local scope to define a local or parameter
integration-tests / test (ubuntu-20.04, 3)
The out parameter 'x' must be assigned to before control leaves the current method
integration-tests / test (ubuntu-20.04, 3)
The out parameter 'y' must be assigned to before control leaves the current method
integration-tests / test (ubuntu-20.04, 3)
The out parameter 'y' must be assigned to before control leaves the current method
integration-tests / test (ubuntu-20.04, 3)
The out parameter 'y' must be assigned to before control leaves the current method
integration-tests / test (ubuntu-20.04, 3)
The out parameter 'y' must be assigned to before control leaves the current method
integration-tests / test (ubuntu-20.04, 3)
There is no argument given that corresponds to the required parameter 'x' of '__default.M2(out BigInteger, out BigInteger)'
integration-tests / test (ubuntu-20.04, 3)
There is no argument given that corresponds to the required parameter 'x' of '__default.M2(out BigInteger, out BigInteger)'
integration-tests / test (ubuntu-20.04, 3)
There is no argument given that corresponds to the required parameter 'z' of '__default.M3(out BigInteger, out BigInteger, out BigInteger)'
integration-tests / test (ubuntu-20.04, 3)
An object of a type convertible to 'BigInteger' is required
integration-tests / test (ubuntu-20.04, 5)
A local or parameter named 'a' cannot be declared in this scope because that name is used in an enclosing local scope to define a local or parameter
integration-tests / test (ubuntu-20.04, 5)
The out parameter 'a' must be assigned to before control leaves the current method
integration-tests / test (ubuntu-20.04, 5)
The out parameter 'b' must be assigned to before control leaves the current method
integration-tests / test (ubuntu-20.04, 5)
There is no argument given that corresponds to the required parameter 'a' of '__default.P(out BigInteger, out BigInteger)'
integration-tests / test (ubuntu-20.04, 5)
A local or parameter named 'a' cannot be declared in this scope because that name is used in an enclosing local scope to define a local or parameter
integration-tests / test (ubuntu-20.04, 5)
The out parameter 'a' must be assigned to before control leaves the current method
integration-tests / test (ubuntu-20.04, 5)
The out parameter 'b' must be assigned to before control leaves the current method
integration-tests / test (ubuntu-20.04, 5)
There is no argument given that corresponds to the required parameter 'a' of '__default.P(out BigInteger, out BigInteger)'
integration-tests / test (ubuntu-20.04, 5)
A local or parameter named 'a' cannot be declared in this scope because that name is used in an enclosing local scope to define a local or parameter
integration-tests / test (ubuntu-20.04, 5)
The out parameter 'a' must be assigned to before control leaves the current method
integration-tests / test (ubuntu-20.04, 1)
There is no argument given that corresponds to the required parameter 'b' of '__default.GetTest0cInput(out uint, out char)'
integration-tests / test (ubuntu-20.04, 1)
A local or parameter named 'b' cannot be declared in this scope because that name is used in an enclosing local scope to define a local or parameter
integration-tests / test (ubuntu-20.04, 1)
The out parameter 'b' must be assigned to before control leaves the current method
integration-tests / test (ubuntu-20.04, 1)
The out parameter 'c' must be assigned to before control leaves the current method
integration-tests / test (ubuntu-20.04, 1)
There is no argument given that corresponds to the required parameter 'b' of '__default.GetTest0cInput(out uint, out char)'
integration-tests / test (ubuntu-20.04, 1)
A local or parameter named 'b' cannot be declared in this scope because that name is used in an enclosing local scope to define a local or parameter
integration-tests / test (ubuntu-20.04, 1)
The out parameter 'b' must be assigned to before control leaves the current method
integration-tests / test (ubuntu-20.04, 1)
The out parameter 'c' must be assigned to before control leaves the current method
integration-tests / test (ubuntu-20.04, 1)
There is no argument given that corresponds to the required parameter 'b' of '__default.GetTest0cInput(out uint, out char)'
integration-tests / test (ubuntu-20.04, 1)
A local or parameter named 'b' cannot be declared in this scope because that name is used in an enclosing local scope to define a local or parameter
integration-tests / test (ubuntu-20.04, 4)
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
singletons: Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
singletons: Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
singletons: Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
singletons: Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
singletons: Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
singletons: Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
singletons: Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
singletons: Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
singletons: Source/DafnyCore/Backends/SymbolTable.cs#L141
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
singletons: Source/DafnyCore/Backends/SymbolTable.cs#L126
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
singletons: Source/DafnyCore/Backends/SymbolTable.cs#L131
The annotation for nullable reference types should only be used in code within a '#nullable' annotations context.
singletons: 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 / 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.
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.
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, 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, 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, 1)
Comparison made to same variable; did you mean to compare something else?
integration-tests / test (ubuntu-20.04, 1)
Comparison made to same variable; did you mean to compare something else?
integration-tests / test (ubuntu-20.04, 1)
Comparison made to same variable; did you mean to compare something else?
integration-tests / test (ubuntu-20.04, 1)
Comparison made to same variable; did you mean to compare something else?
integration-tests / test (ubuntu-20.04, 1)
Comparison made to same variable; did you mean to compare something else?
integration-tests / test (ubuntu-20.04, 1)
Comparison made to same variable; did you mean to compare something else?
integration-tests / test (ubuntu-20.04, 1)
Comparison made to same variable; did you mean to compare something else?
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, 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)
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, 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.

Artifacts

Produced during runtime
Name Size Digest
integration-test-results-ubuntu-20.04-1 Expired
1.72 MB
sha256:cc1e97174f442ba52fd2ddaf23f901548edafa629aee374e55d9217129f2e181
integration-test-results-ubuntu-20.04-2 Expired
1.69 MB
sha256:3bb9f08d4c120719f5209c1294138e413c765fbaafcf9cc7a9b85bfb4284c68b
integration-test-results-ubuntu-20.04-3 Expired
1.7 MB
sha256:ad749966f41ae285332bbb6a3ebd0458ef79cc6557a48bd4c90ddabb60db67d7
integration-test-results-ubuntu-20.04-4 Expired
1.69 MB
sha256:1614a1b623342ca26c99bf92e2d22ea59056346e77d5168f297646cc5cd27462
integration-test-results-ubuntu-20.04-5 Expired
1.67 MB
sha256:0fbb1996cf84d4cacee08aa9158216d7823dd8a1a40f6086189f18f446ff2f0d
unit-test-results-macos-13 Expired
3.91 MB
sha256:db7b3bb47aad0c14ff814164ca6df03094b82c8056c2cf5f6e99374739c8222a
unit-test-results-ubuntu-20.04 Expired
3.94 MB
sha256:7502ab1b7f786738470a2cdd643d25db30d82ef243153f36453d59351e391103
unit-test-results-windows-2019 Expired
3.91 MB
sha256:570dab037e09667f5b091158e6d546c5c02689831daafd0000eb5a0457222c3b