Skip to content

Make blames a bit more concrete. Or should they be on the accesses? #1837

Make blames a bit more concrete. Or should they be on the accesses?

Make blames a bit more concrete. Or should they be on the accesses? #1837

Triggered via push November 21, 2023 16:43
Status Failure
Total duration 15m 56s
Artifacts 12

scalatest.yml

on: push
Matrix: ScalaTest
ScalaTestWindowsBasic
10m 33s
ScalaTestWindowsBasic
ScalaTestMacOsBasic
6m 40s
ScalaTestMacOsBasic
GenerateTestReport
2m 8s
GenerateTestReport
Fit to window
Zoom out
Zoom in

Annotations

15 errors and 14 warnings
ScalaTest (-n MATRIX[6])
Process completed with exit code 1.
ScalaTest (-n MATRIX[0])
Process completed with exit code 1.
ScalaTest (-n MATRIX[4])
Process completed with exit code 1.
ScalaTest (-n MATRIX[3])
Process completed with exit code 1.
ScalaTest (-n MATRIX[5])
Process completed with exit code 1.
ScalaTest (-n MATRIX[7])
Process completed with exit code 1.
ScalaTest (-n MATRIX[1])
Process completed with exit code 1.
vct.test.integration.examples.GpgpuSpec ► Examples examples/concepts/gpgpu/cuda.cu produces verdict pass with Silicon: test/main/vct/test/integration/helper/VercorsSpec.scala#L120
Failed test found in: reports/ubuntu-0/TEST-vct.test.integration.examples.GpgpuSpec.xml reports/ubuntu-0/TEST-vct.test.integration.examples.TechnicalVeyMontSpec2.xml reports/ubuntu-4/TEST-vct.test.integration.examples.TechnicalVeyMontSpec.xml reports/ubuntu-6/TEST-vct.test.integration.examples.TechnicalVeyMontSpec.xml Error: org.scalatest.exceptions.TestFailedException: Expected the test to pass, but it crashed with the above error instead.
vct.test.integration.examples.TechnicalVeyMontSpec ► Assigning shld change state produces verdict error with Silicon: test/main/vct/test/integration/helper/VercorsSpec.scala#L163
Failed test found in: reports/ubuntu-0/TEST-vct.test.integration.examples.TechnicalVeyMontSpec.xml Error: org.scalatest.exceptions.TestFailedException: Expected the test to error, but got a pass or fail instead.
vct.test.integration.examples.TechnicalVeyMontSpec ► Permission shld be generated for constructors as well produces verdict pass with Silicon: test/main/vct/test/integration/helper/VercorsSpec.scala#L124
Failed test found in: reports/ubuntu-0/TEST-vct.test.integration.examples.TechnicalVeyMontSpec.xml reports/ubuntu-1/TEST-vct.test.integration.examples.TechnicalVeyMontSpec.xml reports/ubuntu-3/TEST-vct.test.integration.examples.TechnicalVeyMontSpec.xml reports/ubuntu-3/TEST-vct.test.integration.examples.TechnicalVeyMontSpec2.xml reports/ubuntu-7/TEST-vct.test.integration.examples.TechnicalVeyMontSpec.xml reports/ubuntu-7/TEST-vct.test.integration.examples.TechnicalVeyMontSpec.xml Error: org.scalatest.exceptions.TestFailedException: Expected the test to pass, but it returned verification failures instead.
vct.test.integration.examples.TechnicalVeyMontSpec ► Programs where branch condition unanimity cannot be maintained shld fail produces verdict fail with Silicon: test/main/vct/test/integration/helper/VercorsSpec.scala#L143
Failed test found in: reports/ubuntu-3/TEST-vct.test.integration.examples.TechnicalVeyMontSpec.xml Error: org.scalatest.exceptions.TestFailedException: Expected the test to fail with code loopUnanimityNotMaintained, but it crashed with the above error instead.
vct.test.integration.examples.TechnicalVeyMontSpec ► Parts of condition in branch have to agree inside seqprog produces verdict fail with Silicon: test/main/vct/test/integration/helper/VercorsSpec.scala#L150
Failed test found in: reports/ubuntu-4/TEST-vct.test.integration.examples.TechnicalVeyMontSpec.xml reports/ubuntu-5/TEST-vct.test.integration.examples.TechnicalVeyMontSpec.xml Error: org.scalatest.exceptions.TestFailedException: Expected the test to fail with error code branchNotUnanimous, but got perm instead.
vct.test.integration.examples.TechnicalVeyMontSpec ► Plain endpoint field dereference shld be possible produces verdict fail with Silicon: test/main/vct/test/integration/helper/VercorsSpec.scala#L150
Failed test found in: reports/ubuntu-7/TEST-vct.test.integration.examples.TechnicalVeyMontSpec.xml Error: org.scalatest.exceptions.TestFailedException: Expected the test to fail with error code assertFailed:false, but got perm instead.
vct.test.integration.examples.TechnicalVeyMontSpec ► Programs where branch condition unanimity cannot be established shld fail produces verdict fail with Silicon: test/main/vct/test/integration/helper/VercorsSpec.scala#L150
Failed test found in: reports/ubuntu-7/TEST-vct.test.integration.examples.TechnicalVeyMontSpec.xml Error: org.scalatest.exceptions.TestFailedException: Expected the test to fail with error code loopUnanimityNotEstablished, but got perm instead.
GenerateTestReport
Failed test were found and 'fail-on-error' option is set to true
Compile
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-l MATRIX)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[6])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[0])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[2])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[4])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[3])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[5])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[7])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTestMacOsBasic
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTest (-n MATRIX[1])
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
ScalaTestWindowsBasic
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2, actions/setup-java@v1, actions/cache@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
GenerateTestReport
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
GenerateTestReport
Test report summary exceeded limit of 65535 bytes and will be trimmed

Artifacts

Produced during runtime
Name Size
allTests Expired
121 MB
test-report-macos-latest Expired
22.3 KB
test-report-ubuntu-latest--l MATRIX Expired
263 KB
test-report-ubuntu-latest--n MATRIX[0] Expired
295 KB
test-report-ubuntu-latest--n MATRIX[1] Expired
283 KB
test-report-ubuntu-latest--n MATRIX[2] Expired
275 KB
test-report-ubuntu-latest--n MATRIX[3] Expired
294 KB
test-report-ubuntu-latest--n MATRIX[4] Expired
284 KB
test-report-ubuntu-latest--n MATRIX[5] Expired
283 KB
test-report-ubuntu-latest--n MATRIX[6] Expired
280 KB
test-report-ubuntu-latest--n MATRIX[7] Expired
301 KB
test-report-windows-latest Expired
24.7 KB