constructor: optional body, add out args #1944
scalatest.yml
on: push
Annotations
22 errors and 14 warnings
ScalaTest (-n MATRIX[0])
Process completed with exit code 1.
|
ScalaTest (-n MATRIX[4])
Process completed with exit code 1.
|
ScalaTestWindowsBasic
Process completed with exit code 1.
|
ScalaTest (-n MATRIX[7])
Process completed with exit code 1.
|
ScalaTest (-n MATRIX[6])
Process completed with exit code 1.
|
ScalaTestMacOsBasic
Process completed with exit code 1.
|
ScalaTest (-n MATRIX[2])
Process completed with exit code 1.
|
ScalaTest (-n MATRIX[5])
Process completed with exit code 1.
|
ScalaTest (-n MATRIX[3])
Process completed with exit code 1.
|
ScalaTest (-n MATRIX[1])
Process completed with exit code 1.
|
vct.test.integration.examples.BasicExamplesSpec ► Examples examples/concepts/basic/AddAssignJava.java produces verdict pass with Silicon:
src/col/vct/col/typerules/CoercingRewriter.scala#L1556
Failed test found in:
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
Error:
scala.MatchError: ??Constructor??({ }) (of class vct.col.ast.Constructor)
|
vct.test.integration.examples.BasicExamplesSpec ► Examples examples/concepts/basic/AddAssignJava.java produces verdict pass with Carbon:
src/col/vct/col/typerules/CoercingRewriter.scala#L1556
Failed test found in:
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
Error:
scala.MatchError: ??Constructor??({ }) (of class vct.col.ast.Constructor)
|
vct.test.integration.examples.BasicExamplesSpec ► Examples examples/concepts/basic/BasicAssert.java produces verdict pass with Silicon:
src/col/vct/col/typerules/CoercingRewriter.scala#L1556
Failed test found in:
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
Error:
scala.MatchError: ??Constructor??({ this.Test_1493277758 = false; }, ensures Perm(this.Test_1493277758, write);) (of class vct.col.ast.Constructor)
|
vct.test.integration.examples.BasicExamplesSpec ► Examples examples/concepts/basic/BasicAssert.java produces verdict pass with Carbon:
src/col/vct/col/typerules/CoercingRewriter.scala#L1556
Failed test found in:
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
Error:
scala.MatchError: ??Constructor??({ this.Test_68099179 = false; }, ensures Perm(this.Test_68099179, write);) (of class vct.col.ast.Constructor)
|
vct.test.integration.examples.BasicExamplesSpec ► Examples examples/concepts/basic/BasicAssert-e1.java produces verdict pass with Silicon:
src/col/vct/col/typerules/CoercingRewriter.scala#L1556
Failed test found in:
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
Error:
scala.MatchError: ??Constructor??({ this.Test_1522840787 = false; }, ensures Perm(this.Test_1522840787, write);) (of class vct.col.ast.Constructor)
|
vct.test.integration.examples.BasicExamplesSpec ► Examples examples/concepts/basic/BasicAssert-e1.java produces verdict pass with Carbon:
src/col/vct/col/typerules/CoercingRewriter.scala#L1556
Failed test found in:
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
Error:
scala.MatchError: ??Constructor??({ this.Test_36411324 = false; }, ensures Perm(this.Test_36411324, write);) (of class vct.col.ast.Constructor)
|
vct.test.integration.examples.BasicExamplesSpec ► Examples examples/concepts/basic/CollectionTest.pvl produces verdict pass with Silicon:
test/main/vct/test/integration/helper/VercorsSpec.scala#L120
Failed test found in:
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
reports/windows/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
Error:
org.scalatest.exceptions.TestFailedException: Expected the test to pass, but it crashed with the above error instead.
|
vct.test.integration.examples.BasicExamplesSpec ► Examples examples/concepts/basic/DafnyIncr.java produces verdict pass with Silicon:
src/col/vct/col/typerules/CoercingRewriter.scala#L1556
Failed test found in:
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
Error:
scala.MatchError: ??Constructor??({ this.Y_2028602543 = 0; }, ensures Perm(this.Y_2028602543, write);) (of class vct.col.ast.Constructor)
|
vct.test.integration.examples.BasicExamplesSpec ► Examples examples/concepts/basic/DafnyIncr.java produces verdict pass with Carbon:
src/col/vct/col/typerules/CoercingRewriter.scala#L1556
Failed test found in:
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
Error:
scala.MatchError: ??Constructor??({ this.Y_1288558702 = 0; }, ensures Perm(this.Y_1288558702, write);) (of class vct.col.ast.Constructor)
|
vct.test.integration.examples.BasicExamplesSpec ► Examples examples/concepts/basic/DafnyIncrE1.java produces verdict pass with Silicon:
src/col/vct/col/typerules/CoercingRewriter.scala#L1556
Failed test found in:
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
Error:
scala.MatchError: ??Constructor??({ this.Y_1219204130 = 0; }, ensures Perm(this.Y_1219204130, write);) (of class vct.col.ast.Constructor)
|
vct.test.integration.examples.BasicExamplesSpec ► Examples examples/concepts/basic/DafnyIncrE1.java produces verdict fail with Carbon:
src/col/vct/col/typerules/CoercingRewriter.scala#L1556
Failed test found in:
reports/macos/TEST-vct.test.integration.examples.BasicExamplesSpec.xml
Error:
scala.MatchError: ??Constructor??({ this.Y_1896381627 = 0; }, ensures Perm(this.Y_1896381627, write);) (of class vct.col.ast.Constructor)
|
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[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[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/
|
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/
|
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/
|
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/
|
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[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[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[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[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/
|
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
|
122 MB |
|
test-report-macos-latest
Expired
|
691 KB |
|
test-report-ubuntu-latest--l MATRIX
Expired
|
263 KB |
|
test-report-ubuntu-latest--n MATRIX[0]
Expired
|
647 KB |
|
test-report-ubuntu-latest--n MATRIX[1]
Expired
|
745 KB |
|
test-report-ubuntu-latest--n MATRIX[2]
Expired
|
763 KB |
|
test-report-ubuntu-latest--n MATRIX[3]
Expired
|
726 KB |
|
test-report-ubuntu-latest--n MATRIX[4]
Expired
|
660 KB |
|
test-report-ubuntu-latest--n MATRIX[5]
Expired
|
787 KB |
|
test-report-ubuntu-latest--n MATRIX[6]
Expired
|
735 KB |
|
test-report-ubuntu-latest--n MATRIX[7]
Expired
|
828 KB |
|
test-report-windows-latest
Expired
|
694 KB |
|