Skip to content
Build and Test

Speed up dafny verify by reducing memory pressure #19218

Sign in to view logs

Speed up dafny verify by reducing memory pressure

Speed up dafny verify by reducing memory pressure #19218

Triggered via pull request October 11, 2024 12:03
@keyboardDrummerkeyboardDrummer
opened #5827
keyboardDrummer:onlyClaimVerificationMemoryPerModule
Status Cancelled
Total duration 18m 19s
Artifacts 8

msbuild.yml

on: pull_request
check-deep-tests  /  check-deep-tests
12s
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
1m 29s
singletons
Matrix: integration-tests / test
Matrix: xunit-tests / build
test-coverage-analysis
0s
test-coverage-analysis
Fit to window
Zoom out
Zoom in

Annotations

18 errors and 55 warnings
singletons
Process completed with exit code 2.
xunit-tests / ubuntu-20.04 (1)
Process completed with exit code 1.
xunit-tests / osx (1)
Process completed with exit code 1.
xunit-tests / win (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, 3)
The type or namespace name 'C' does not exist in the namespace 'B' (are you missing an assembly reference?)
integration-tests / test (ubuntu-20.04, 3)
The type or namespace name 'C' does not exist in the namespace 'B' (are you missing an assembly reference?)
integration-tests / test (ubuntu-20.04, 3)
The type or namespace name 'C' does not exist in the namespace 'B' (are you missing an assembly reference?)
integration-tests / test (ubuntu-20.04, 3)
The type or namespace name 'C' does not exist in the namespace 'B' (are you missing an assembly reference?)
integration-tests / test (ubuntu-20.04, 3)
The type or namespace name 'C' does not exist in the namespace 'B' (are you missing an assembly reference?)
integration-tests / test (ubuntu-20.04, 3)
The type or namespace name 'C' does not exist in the namespace 'B' (are you missing an assembly reference?)
integration-tests / test (ubuntu-20.04, 3)
The type or namespace name 'C' does not exist in the namespace 'B' (are you missing an assembly reference?)
integration-tests / test (ubuntu-20.04, 3)
The type or namespace name 'C' does not exist in the namespace 'B' (are you missing an assembly reference?)
integration-tests / test (ubuntu-20.04, 3)
The type or namespace name 'C' does not exist in the namespace 'B' (are you missing an assembly reference?)
integration-tests / test (ubuntu-20.04, 3)
The type or namespace name 'C' does not exist in the namespace 'B' (are you missing an assembly reference?)
integration-tests / test (ubuntu-20.04, 1)
Process completed with exit code 1.
integration-tests / test (ubuntu-20.04, 5)
Process completed with exit code 1.
integration-tests / test (ubuntu-20.04, 2)
Process completed with exit code 1.
xunit-tests / ubuntu-20.04 (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L16
Possible null reference return.
xunit-tests / ubuntu-20.04 (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L27
Dereference of a possibly null reference.
xunit-tests / ubuntu-20.04 (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L35
Dereference of a possibly null reference.
xunit-tests / ubuntu-20.04 (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L73
Dereference of a possibly null reference.
xunit-tests / ubuntu-20.04 (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L85
Possible null reference argument for parameter 'impl' in 'ImplementationRunResult? VerificationResultCache.Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)'.
xunit-tests / ubuntu-20.04 (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L16
Possible null reference return.
xunit-tests / ubuntu-20.04 (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L27
Dereference of a possibly null reference.
xunit-tests / ubuntu-20.04 (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L35
Dereference of a possibly null reference.
xunit-tests / ubuntu-20.04 (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L73
Dereference of a possibly null reference.
xunit-tests / ubuntu-20.04 (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L85
Possible null reference argument for parameter 'impl' in 'ImplementationRunResult? VerificationResultCache.Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)'.
xunit-tests / osx (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L16
Possible null reference return.
xunit-tests / osx (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L27
Dereference of a possibly null reference.
xunit-tests / osx (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L35
Dereference of a possibly null reference.
xunit-tests / osx (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L73
Dereference of a possibly null reference.
xunit-tests / osx (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L85
Possible null reference argument for parameter 'impl' in 'ImplementationRunResult? VerificationResultCache.Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)'.
xunit-tests / osx (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L16
Possible null reference return.
xunit-tests / osx (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L27
Dereference of a possibly null reference.
xunit-tests / osx (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L35
Dereference of a possibly null reference.
xunit-tests / osx (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L73
Dereference of a possibly null reference.
xunit-tests / osx (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L85
Possible null reference argument for parameter 'impl' in 'ImplementationRunResult? VerificationResultCache.Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)'.
xunit-tests / win (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L16
Possible null reference return.
xunit-tests / win (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L27
Dereference of a possibly null reference.
xunit-tests / win (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L35
Dereference of a possibly null reference.
xunit-tests / win (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L73
Dereference of a possibly null reference.
xunit-tests / win (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L85
Possible null reference argument for parameter 'impl' in 'ImplementationRunResult? VerificationResultCache.Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)'.
xunit-tests / win (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L16
Possible null reference return.
xunit-tests / win (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L27
Dereference of a possibly null reference.
xunit-tests / win (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L35
Dereference of a possibly null reference.
xunit-tests / win (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L73
Dereference of a possibly null reference.
xunit-tests / win (1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L85
Possible null reference argument for parameter 'impl' in 'ImplementationRunResult? VerificationResultCache.Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)'.
integration-tests / test (ubuntu-20.04, 4): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L16
Possible null reference return.
integration-tests / test (ubuntu-20.04, 4): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L27
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 4): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L35
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 4): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L73
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 4): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L85
Possible null reference argument for parameter 'impl' in 'ImplementationRunResult? VerificationResultCache.Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)'.
integration-tests / test (ubuntu-20.04, 3): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L16
Possible null reference return.
integration-tests / test (ubuntu-20.04, 3): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L27
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 3): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L35
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 3): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L73
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 3): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L85
Possible null reference argument for parameter 'impl' in 'ImplementationRunResult? VerificationResultCache.Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)'.
integration-tests / test (ubuntu-20.04, 1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L16
Possible null reference return.
integration-tests / test (ubuntu-20.04, 1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L27
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L35
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L73
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 1): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L85
Possible null reference argument for parameter 'impl' in 'ImplementationRunResult? VerificationResultCache.Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)'.
integration-tests / test (ubuntu-20.04, 5): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L16
Possible null reference return.
integration-tests / test (ubuntu-20.04, 5): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L27
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 5): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L35
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 5): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L73
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 5): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L85
Possible null reference argument for parameter 'impl' in 'ImplementationRunResult? VerificationResultCache.Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)'.
integration-tests / test (ubuntu-20.04, 2): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L16
Possible null reference return.
integration-tests / test (ubuntu-20.04, 2): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L27
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 2): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L35
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 2): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L73
Dereference of a possibly null reference.
integration-tests / test (ubuntu-20.04, 2): boogie/Source/ExecutionEngine/Caching/VerificationResultCache.cs#L85
Possible null reference argument for parameter 'impl' in 'ImplementationRunResult? VerificationResultCache.Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)'.

Artifacts

Produced during runtime
Name Size Digest
integration-test-results-ubuntu-20.04-1 Expired
2.41 MB
sha256:60c7484093d3c5f9af3a572b3c95a6c966bee1859daeb2d2f4935e84954ab7ce
integration-test-results-ubuntu-20.04-2 Expired
2.39 MB
sha256:b99a2fabf0c1f4bd02f7c7e5715eb7cad94b228641b04eee136021d49ad27bf0
integration-test-results-ubuntu-20.04-3 Expired
2.39 MB
sha256:37d2754a22a84a7dcafe405fa85619409286b01ca324d2821640eeed21b94b9d
integration-test-results-ubuntu-20.04-4 Expired
2.39 MB
sha256:fcdb521f9b17483ac736c265969659cde8ef3fcae8d49824425041cd5f587b06
integration-test-results-ubuntu-20.04-5 Expired
2.43 MB
sha256:7e0130b035a693bda12fe366a76f241ad443f66ba48559d54bbe80337e8f1773
unit-test-results-macos-13 Expired
5.29 MB
sha256:873c0ac3effd5d6aa71ebe4b70b1669e6f044cadaab4dc3a3a4649db48ac0f8a
unit-test-results-ubuntu-20.04 Expired
5.32 MB
sha256:74a0eb991ea4e3dcbe3757ad12cd197e1f1e8e761e6ef70f6100bc63b4a9e923
unit-test-results-windows-2019 Expired
5.29 MB
sha256:1217b525600e9595cea31103ea64b7783625513575fa2f0b39e0dd822ede7990