Skip to content
Run ScalaTest

Merge branch 'small-fix' into PointerADT #123

Sign in to view logs

Merge branch 'small-fix' into PointerADT

Merge branch 'small-fix' into PointerADT #123

GitHub Actions / TestReport failed May 6, 2024 in 0s

1010 passed, 8 failed and 42 skipped

Tests failed
Report exceeded GitHub limit of 65535 bytes and has been trimmed

Annotations

Check failure on line 46 in src/col/vct/col/typerules/CoercingRewriter.scala

See this annotation in the file changed.

@github-actions github-actions / TestReport

vct.test.integration.features.AmbiguousOps ► Example showing collapsed pointer arithmetic produces verdict pass with Silicon 

Failed test found in:
  reports/ubuntu-1/TEST-vct.test.integration.features.AmbiguousOps.xml
Error:
        scala.NotImplementedError: an implementation is missing
Raw output 
      scala.NotImplementedError: an implementation is missing
      at scala.Predef$.$qmark$qmark$qmark(Predef.scala:344)
      at vct.col.rewrite.adt.ImportArrayPointer.postCoerce(ImportPointer.scala:263)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:25)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:21)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.$anonfun$dispatch$1(BaseCoercingRewriter.scala:23)
      at vct.col.typerules.CoercingRewriter.applyCoercion(CoercingRewriter.scala:70)
      at vct.col.rewrite.adt.ImportArrayPointer.applyCoercion(ImportPointer.scala:196)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:23)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:21)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.AssignRewrite.rewrite(AssignRewrite.scala:9)
      at vct.col.ast.ops.rewrite.AssignRewrite.rewrite$(AssignRewrite.scala:4)
      at vct.col.ast.Assign.rewrite(Node.scala:195)
      at vct.col.ast.ops.rewrite.AssignRewrite.rewriteDefault(AssignRewrite.scala:3)
      at vct.col.ast.ops.rewrite.AssignRewrite.rewriteDefault$(AssignRewrite.scala:3)
      at vct.col.ast.Assign.rewriteDefault(Node.scala:195)
      at vct.col.ast.Assign.rewriteDefault(Node.scala:195)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:173)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:173)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:12)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:12)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.BlockRewrite.$anonfun$rewrite$1(BlockRewrite.scala:6)
      at scala.collection.immutable.List.map(List.scala:250)
      at scala.collection.immutable.List.map(List.scala:79)
      at vct.col.ast.ops.rewrite.BlockRewrite.rewrite(BlockRewrite.scala:6)
      at vct.col.ast.ops.rewrite.BlockRewrite.rewrite$(BlockRewrite.scala:4)
      at vct.col.ast.Block.rewrite(Node.scala:235)
      at vct.col.ast.ops.rewrite.BlockRewrite.rewriteDefault(BlockRewrite.scala:3)
      at vct.col.ast.ops.rewrite.BlockRewrite.rewriteDefault$(BlockRewrite.scala:3)
      at vct.col.ast.Block.rewriteDefault(Node.scala:235)
      at vct.col.ast.Block.rewriteDefault(Node.scala:235)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:173)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:173)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:12)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:12)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.ScopeRewrite.$anonfun$rewrite$4(ScopeRewrite.scala:13)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ScopeRewrite.$anonfun$rewrite$3(ScopeRewrite.scala:8)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ScopeRewrite.$anonfun$rewrite$2(ScopeRewrite.scala:7)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ScopeRewrite.$anonfun$rewrite$1(ScopeRewrite.scala:6)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ScopeRewrite.rewrite(ScopeRewrite.scala:5)
      at vct.col.ast.ops.rewrite.ScopeRewrite.rewrite$(ScopeRewrite.scala:4)
      at vct.col.ast.Scope.rewrite(Node.scala:236)
      at vct.col.ast.ops.rewrite.ScopeRewrite.rewriteDefault(ScopeRewrite.scala:3)
      at vct.col.ast.ops.rewrite.ScopeRewrite.rewriteDefault$(ScopeRewrite.scala:3)
      at vct.col.ast.Scope.rewriteDefault(Node.scala:236)
      at vct.col.ast.Scope.rewriteDefault(Node.scala:236)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:173)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:173)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:12)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:12)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.$anonfun$rewrite$2(ProcedureRewrite.scala:19)
      at scala.Option.map(Option.scala:242)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.$anonfun$rewrite$1(ProcedureRewrite.scala:19)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewrite(ProcedureRewrite.scala:5)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewrite$(ProcedureRewrite.scala:4)
      at vct.col.ast.Procedure.rewrite(Node.scala:262)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewriteDefault(ProcedureRewrite.scala:3)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewriteDefault$(ProcedureRewrite.scala:3)
      at vct.col.ast.Procedure.rewriteDefault(Node.scala:262)
      at vct.col.ast.Procedure.rewriteDefault(Node.scala:262)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:273)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:277)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$4(ImportADT.scala:96)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$4$adapted(ImportADT.scala:96)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$3(ImportADT.scala:96)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.collect(Scopes.scala:68)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$2(ImportADT.scala:96)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$6(ProgramRewrite.scala:11)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$5(ProgramRewrite.scala:10)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$4(ProgramRewrite.scala:9)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$3(ProgramRewrite.scala:8)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$2(ProgramRewrite.scala:7)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$1(ProgramRewrite.scala:6)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.rewrite(ProgramRewrite.scala:5)
      at vct.col.ast.ops.rewrite.ProgramRewrite.rewrite$(ProgramRewrite.scala:4)
      at vct.col.ast.Program.rewrite(Node.scala:104)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$1(ImportADT.scala:95)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.rewrite.adt.ImportADT.postCoerce(ImportADT.scala:95)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:6)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:6)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewrite(VerificationContextRewrite.scala:6)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewrite$(VerificationContextRewrite.scala:4)
      at vct.col.ast.VerificationContext.rewrite(Node.scala:95)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewriteDefault(VerificationContextRewrite.scala:3)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewriteDefault$(VerificationContextRewrite.scala:3)
      at vct.col.ast.VerificationContext.rewriteDefault(Node.scala:95)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:166)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:166)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:5)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:5)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.VerificationRewrite.$anonfun$rewrite$1(VerificationRewrite.scala:6)
      at scala.collection.immutable.List.map(List.scala:246)
      at scala.collection.immutable.List.map(List.scala:79)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewrite(VerificationRewrite.scala:6)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewrite$(VerificationRewrite.scala:4)
      at vct.col.ast.Verification.rewrite(Node.scala:94)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewriteDefault(VerificationRewrite.scala:3)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewriteDefault$(VerificationRewrite.scala:3)
      at vct.col.ast.Verification.rewriteDefault(Node.scala:94)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:165)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:165)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:4)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:4)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.main.stages.Transformation.$anonfun$run$4(Transformation.scala:126)
      at vct.main.stages.Transformation.$anonfun$run$4$adapted(Transformation.scala:121)
      at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
      at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
      at scala.collection.AbstractIterator.foreach(Iterator.scala:1300)
      at hre.progress.Progress$.foreach(Progress.scala:83)
      at vct.main.stages.Transformation.$anonfun$run$2(Transformation.scala:121)
      at hre.debug.TimeTravel$.safelyRepeatable(TimeTravel.scala:31)
      at vct.main.stages.Transformation.run(Transformation.scala:118)
      at vct.main.stages.Transformation.run(Transformation.scala:96)
      at hre.stages.Stages.$anonfun$run$3(Stages.scala:28)
      at hre.stages.Stages.$anonfun$run$3$adapted(Stages.scala:26)
      at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
      at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
      at scala.collection.AbstractIterable.foreach(Iterable.scala:933)
      at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:903)
      at hre.stages.Stages.$anonfun$run$1(Stages.scala:26)
      at hre.progress.Progress$.stages(Progress.scala:104)
      at hre.stages.Stages.run(Stages.scala:23)
      at hre.stages.Stages.run$(Stages.scala:20)
      at hre.stages.StagesPair.run(Stages.scala:52)
      at vct.main.modes.Verify$.verifyWithOptions(Verify.scala:49)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$2(VercorsSpec.scala:90)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
      at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
      at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
      at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
      at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$1(VercorsSpec.scala:85)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
      at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
      at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
      at org.scalatest.Transformer.apply(Transformer.scala:22)
      at org.scalatest.Transformer.apply(Transformer.scala:20)
      at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
      at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
      at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
      at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
      at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
      at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
      at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
      at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
      at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
      at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.run(Suite.scala:1112)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
      at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
      at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
      at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
      at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
      at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
      at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
      at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
      at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
      at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
      at org.scalatest.Suite.run(Suite.scala:1109)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
      at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
      at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
      at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
      at org.scalatest.tools.Runner$.main(Runner.scala:775)
      at org.scalatest.tools.Runner.main(Runner.scala)

Check failure on line 117 in test/main/vct/test/integration/helper/VercorsSpec.scala

See this annotation in the file changed.

@github-actions github-actions / TestReport

vct.test.integration.examples.CSpec ► Examples examples/concepts/c/math.c produces verdict pass with Silicon 

Failed test found in:
  reports/ubuntu-2/TEST-vct.test.integration.examples.CSpec.xml
Error:
        org.scalatest.exceptions.TestFailedException: Expected the test to pass, but it returned an error with code noSuchName instead.
Raw output 
      org.scalatest.exceptions.TestFailedException: Expected the test to pass, but it returned an error with code noSuchName instead.
      at org.scalatest.Assertions.newAssertionFailedException(Assertions.scala:472)
      at org.scalatest.Assertions.newAssertionFailedException$(Assertions.scala:471)
      at org.scalatest.flatspec.AnyFlatSpec.newAssertionFailedException(AnyFlatSpec.scala:1685)
      at org.scalatest.Assertions.fail(Assertions.scala:933)
      at org.scalatest.Assertions.fail$(Assertions.scala:929)
      at org.scalatest.flatspec.AnyFlatSpec.fail(AnyFlatSpec.scala:1685)
      at vct.test.integration.helper.VercorsSpec.matchVerdict(VercorsSpec.scala:117)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$2(VercorsSpec.scala:86)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
      at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
      at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
      at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
      at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$1(VercorsSpec.scala:85)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
      at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
      at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
      at org.scalatest.Transformer.apply(Transformer.scala:22)
      at org.scalatest.Transformer.apply(Transformer.scala:20)
      at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
      at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
      at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
      at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
      at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
      at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
      at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
      at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
      at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
      at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.run(Suite.scala:1112)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
      at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
      at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
      at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
      at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
      at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
      at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
      at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
      at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
      at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
      at org.scalatest.Suite.run(Suite.scala:1109)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
      at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
      at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
      at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
      at org.scalatest.tools.Runner$.main(Runner.scala:775)
      at org.scalatest.tools.Runner.main(Runner.scala)

Check failure on line 46 in src/col/vct/col/typerules/CoercingRewriter.scala

See this annotation in the file changed.

@github-actions github-actions / TestReport

vct.test.integration.features.AmbiguousOps ► Example showing collapsed pointer arithmetic produces verdict pass with Carbon 

Failed test found in:
  reports/ubuntu-3/TEST-vct.test.integration.features.AmbiguousOps.xml
Error:
        scala.NotImplementedError: an implementation is missing
Raw output 
      scala.NotImplementedError: an implementation is missing
      at scala.Predef$.$qmark$qmark$qmark(Predef.scala:344)
      at vct.col.rewrite.adt.ImportArrayPointer.postCoerce(ImportPointer.scala:263)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:25)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:21)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.$anonfun$dispatch$1(BaseCoercingRewriter.scala:23)
      at vct.col.typerules.CoercingRewriter.applyCoercion(CoercingRewriter.scala:70)
      at vct.col.rewrite.adt.ImportArrayPointer.applyCoercion(ImportPointer.scala:196)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:23)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:21)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.AssignRewrite.rewrite(AssignRewrite.scala:9)
      at vct.col.ast.ops.rewrite.AssignRewrite.rewrite$(AssignRewrite.scala:4)
      at vct.col.ast.Assign.rewrite(Node.scala:195)
      at vct.col.ast.ops.rewrite.AssignRewrite.rewriteDefault(AssignRewrite.scala:3)
      at vct.col.ast.ops.rewrite.AssignRewrite.rewriteDefault$(AssignRewrite.scala:3)
      at vct.col.ast.Assign.rewriteDefault(Node.scala:195)
      at vct.col.ast.Assign.rewriteDefault(Node.scala:195)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:173)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:173)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:12)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:12)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.BlockRewrite.$anonfun$rewrite$1(BlockRewrite.scala:6)
      at scala.collection.immutable.List.map(List.scala:250)
      at scala.collection.immutable.List.map(List.scala:79)
      at vct.col.ast.ops.rewrite.BlockRewrite.rewrite(BlockRewrite.scala:6)
      at vct.col.ast.ops.rewrite.BlockRewrite.rewrite$(BlockRewrite.scala:4)
      at vct.col.ast.Block.rewrite(Node.scala:235)
      at vct.col.ast.ops.rewrite.BlockRewrite.rewriteDefault(BlockRewrite.scala:3)
      at vct.col.ast.ops.rewrite.BlockRewrite.rewriteDefault$(BlockRewrite.scala:3)
      at vct.col.ast.Block.rewriteDefault(Node.scala:235)
      at vct.col.ast.Block.rewriteDefault(Node.scala:235)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:173)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:173)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:12)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:12)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.ScopeRewrite.$anonfun$rewrite$4(ScopeRewrite.scala:13)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ScopeRewrite.$anonfun$rewrite$3(ScopeRewrite.scala:8)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ScopeRewrite.$anonfun$rewrite$2(ScopeRewrite.scala:7)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ScopeRewrite.$anonfun$rewrite$1(ScopeRewrite.scala:6)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ScopeRewrite.rewrite(ScopeRewrite.scala:5)
      at vct.col.ast.ops.rewrite.ScopeRewrite.rewrite$(ScopeRewrite.scala:4)
      at vct.col.ast.Scope.rewrite(Node.scala:236)
      at vct.col.ast.ops.rewrite.ScopeRewrite.rewriteDefault(ScopeRewrite.scala:3)
      at vct.col.ast.ops.rewrite.ScopeRewrite.rewriteDefault$(ScopeRewrite.scala:3)
      at vct.col.ast.Scope.rewriteDefault(Node.scala:236)
      at vct.col.ast.Scope.rewriteDefault(Node.scala:236)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:173)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:173)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:12)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:12)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.$anonfun$rewrite$2(ProcedureRewrite.scala:19)
      at scala.Option.map(Option.scala:242)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.$anonfun$rewrite$1(ProcedureRewrite.scala:19)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewrite(ProcedureRewrite.scala:5)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewrite$(ProcedureRewrite.scala:4)
      at vct.col.ast.Procedure.rewrite(Node.scala:262)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewriteDefault(ProcedureRewrite.scala:3)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewriteDefault$(ProcedureRewrite.scala:3)
      at vct.col.ast.Procedure.rewriteDefault(Node.scala:262)
      at vct.col.ast.Procedure.rewriteDefault(Node.scala:262)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:273)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:277)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$4(ImportADT.scala:96)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$4$adapted(ImportADT.scala:96)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$3(ImportADT.scala:96)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.collect(Scopes.scala:68)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$2(ImportADT.scala:96)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$6(ProgramRewrite.scala:11)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$5(ProgramRewrite.scala:10)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$4(ProgramRewrite.scala:9)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$3(ProgramRewrite.scala:8)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$2(ProgramRewrite.scala:7)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$1(ProgramRewrite.scala:6)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.rewrite(ProgramRewrite.scala:5)
      at vct.col.ast.ops.rewrite.ProgramRewrite.rewrite$(ProgramRewrite.scala:4)
      at vct.col.ast.Program.rewrite(Node.scala:104)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$1(ImportADT.scala:95)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.rewrite.adt.ImportADT.postCoerce(ImportADT.scala:95)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:6)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:6)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewrite(VerificationContextRewrite.scala:6)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewrite$(VerificationContextRewrite.scala:4)
      at vct.col.ast.VerificationContext.rewrite(Node.scala:95)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewriteDefault(VerificationContextRewrite.scala:3)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewriteDefault$(VerificationContextRewrite.scala:3)
      at vct.col.ast.VerificationContext.rewriteDefault(Node.scala:95)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:166)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:166)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:5)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:5)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.VerificationRewrite.$anonfun$rewrite$1(VerificationRewrite.scala:6)
      at scala.collection.immutable.List.map(List.scala:246)
      at scala.collection.immutable.List.map(List.scala:79)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewrite(VerificationRewrite.scala:6)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewrite$(VerificationRewrite.scala:4)
      at vct.col.ast.Verification.rewrite(Node.scala:94)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewriteDefault(VerificationRewrite.scala:3)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewriteDefault$(VerificationRewrite.scala:3)
      at vct.col.ast.Verification.rewriteDefault(Node.scala:94)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:165)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:165)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:4)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:4)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.main.stages.Transformation.$anonfun$run$4(Transformation.scala:126)
      at vct.main.stages.Transformation.$anonfun$run$4$adapted(Transformation.scala:121)
      at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
      at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
      at scala.collection.AbstractIterator.foreach(Iterator.scala:1300)
      at hre.progress.Progress$.foreach(Progress.scala:83)
      at vct.main.stages.Transformation.$anonfun$run$2(Transformation.scala:121)
      at hre.debug.TimeTravel$.safelyRepeatable(TimeTravel.scala:31)
      at vct.main.stages.Transformation.run(Transformation.scala:118)
      at vct.main.stages.Transformation.run(Transformation.scala:96)
      at hre.stages.Stages.$anonfun$run$3(Stages.scala:28)
      at hre.stages.Stages.$anonfun$run$3$adapted(Stages.scala:26)
      at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
      at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
      at scala.collection.AbstractIterable.foreach(Iterable.scala:933)
      at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:903)
      at hre.stages.Stages.$anonfun$run$1(Stages.scala:26)
      at hre.progress.Progress$.stages(Progress.scala:104)
      at hre.stages.Stages.run(Stages.scala:23)
      at hre.stages.Stages.run$(Stages.scala:20)
      at hre.stages.StagesPair.run(Stages.scala:52)
      at vct.main.modes.Verify$.verifyWithOptions(Verify.scala:49)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$2(VercorsSpec.scala:95)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
      at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
      at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
      at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
      at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$1(VercorsSpec.scala:85)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
      at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
      at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
      at org.scalatest.Transformer.apply(Transformer.scala:22)
      at org.scalatest.Transformer.apply(Transformer.scala:20)
      at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
      at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
      at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
      at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
      at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
      at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
      at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
      at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
      at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
      at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.run(Suite.scala:1112)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
      at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
      at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
      at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
      at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
      at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
      at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
      at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
      at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
      at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
      at org.scalatest.Suite.run(Suite.scala:1109)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
      at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
      at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
      at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
      at org.scalatest.tools.Runner$.main(Runner.scala:775)
      at org.scalatest.tools.Runner.main(Runner.scala)

Check failure on line 46 in src/col/vct/col/typerules/CoercingRewriter.scala

See this annotation in the file changed.

@github-actions github-actions / TestReport

vct.test.integration.examples.PointerSpec ► Examples examples/concepts/pointerArithmetic/pointerSubtract.c produces verdict pass with Carbon 

Failed test found in:
  reports/ubuntu-5/TEST-vct.test.integration.examples.PointerSpec.xml
Error:
        scala.NotImplementedError: an implementation is missing
Raw output 
      scala.NotImplementedError: an implementation is missing
      at scala.Predef$.$qmark$qmark$qmark(Predef.scala:344)
      at vct.col.rewrite.adt.ImportArrayPointer.postCoerce(ImportPointer.scala:263)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:25)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:21)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.$anonfun$dispatch$1(BaseCoercingRewriter.scala:23)
      at vct.col.typerules.CoercingRewriter.applyCoercion(CoercingRewriter.scala:70)
      at vct.col.rewrite.adt.ImportArrayPointer.applyCoercion(ImportPointer.scala:196)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:23)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:21)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.NeqRewrite.rewrite(NeqRewrite.scala:6)
      at vct.col.ast.ops.rewrite.NeqRewrite.rewrite$(NeqRewrite.scala:4)
      at vct.col.ast.Neq.rewrite(Node.scala:632)
      at vct.col.ast.ops.rewrite.NeqRewrite.rewriteDefault(NeqRewrite.scala:3)
      at vct.col.ast.ops.rewrite.NeqRewrite.rewriteDefault$(NeqRewrite.scala:3)
      at vct.col.ast.Neq.rewriteDefault(Node.scala:632)
      at vct.col.ast.Neq.rewriteDefault(Node.scala:632)
      at vct.col.ast.AbstractRewriter.rewriteDefault(AbstractRewriter.scala:118)
      at vct.col.ast.AbstractRewriter.rewriteDefault$(AbstractRewriter.scala:118)
      at vct.col.typerules.CoercingRewriter.rewriteDefault(CoercingRewriter.scala:46)
      at vct.col.rewrite.adt.ImportArrayPointer.postCoerce(ImportPointer.scala:282)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:25)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:21)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.$anonfun$dispatch$1(BaseCoercingRewriter.scala:23)
      at vct.col.typerules.CoercingRewriter.applyCoercion(CoercingRewriter.scala:172)
      at vct.col.rewrite.adt.ImportArrayPointer.applyCoercion(ImportPointer.scala:196)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:23)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:21)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.UnitAccountedPredicateRewrite.rewrite(UnitAccountedPredicateRewrite.scala:6)
      at vct.col.ast.ops.rewrite.UnitAccountedPredicateRewrite.rewrite$(UnitAccountedPredicateRewrite.scala:4)
      at vct.col.ast.UnitAccountedPredicate.rewrite(Node.scala:361)
      at vct.col.ast.ops.rewrite.UnitAccountedPredicateRewrite.rewriteDefault(UnitAccountedPredicateRewrite.scala:3)
      at vct.col.ast.ops.rewrite.UnitAccountedPredicateRewrite.rewriteDefault$(UnitAccountedPredicateRewrite.scala:3)
      at vct.col.ast.UnitAccountedPredicate.rewriteDefault(Node.scala:361)
      at vct.col.ast.UnitAccountedPredicate.rewriteDefault(Node.scala:361)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:179)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:179)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:18)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:18)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.SplitAccountedPredicateRewrite.rewrite(SplitAccountedPredicateRewrite.scala:9)
      at vct.col.ast.ops.rewrite.SplitAccountedPredicateRewrite.rewrite$(SplitAccountedPredicateRewrite.scala:4)
      at vct.col.ast.SplitAccountedPredicate.rewrite(Node.scala:362)
      at vct.col.ast.ops.rewrite.SplitAccountedPredicateRewrite.rewriteDefault(SplitAccountedPredicateRewrite.scala:3)
      at vct.col.ast.ops.rewrite.SplitAccountedPredicateRewrite.rewriteDefault$(SplitAccountedPredicateRewrite.scala:3)
      at vct.col.ast.SplitAccountedPredicate.rewriteDefault(Node.scala:362)
      at vct.col.ast.SplitAccountedPredicate.rewriteDefault(Node.scala:362)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:179)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:179)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:18)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:18)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.ApplicableContractRewrite.rewrite(ApplicableContractRewrite.scala:9)
      at vct.col.ast.ops.rewrite.ApplicableContractRewrite.rewrite$(ApplicableContractRewrite.scala:4)
      at vct.col.ast.ApplicableContract.rewrite(Node.scala:356)
      at vct.col.ast.ops.rewrite.ApplicableContractRewrite.rewriteDefault(ApplicableContractRewrite.scala:3)
      at vct.col.ast.ops.rewrite.ApplicableContractRewrite.rewriteDefault$(ApplicableContractRewrite.scala:3)
      at vct.col.ast.ApplicableContract.rewriteDefault(Node.scala:356)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:178)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:178)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:17)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:17)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.$anonfun$rewrite$1(ProcedureRewrite.scala:22)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewrite(ProcedureRewrite.scala:5)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewrite$(ProcedureRewrite.scala:4)
      at vct.col.ast.Procedure.rewrite(Node.scala:262)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewriteDefault(ProcedureRewrite.scala:3)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewriteDefault$(ProcedureRewrite.scala:3)
      at vct.col.ast.Procedure.rewriteDefault(Node.scala:262)
      at vct.col.ast.Procedure.rewriteDefault(Node.scala:262)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:273)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:277)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$4(ImportADT.scala:96)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$4$adapted(ImportADT.scala:96)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$3(ImportADT.scala:96)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.collect(Scopes.scala:68)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$2(ImportADT.scala:96)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$6(ProgramRewrite.scala:11)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$5(ProgramRewrite.scala:10)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$4(ProgramRewrite.scala:9)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$3(ProgramRewrite.scala:8)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$2(ProgramRewrite.scala:7)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$1(ProgramRewrite.scala:6)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.rewrite(ProgramRewrite.scala:5)
      at vct.col.ast.ops.rewrite.ProgramRewrite.rewrite$(ProgramRewrite.scala:4)
      at vct.col.ast.Program.rewrite(Node.scala:104)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$1(ImportADT.scala:95)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.rewrite.adt.ImportADT.postCoerce(ImportADT.scala:95)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:6)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:6)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewrite(VerificationContextRewrite.scala:6)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewrite$(VerificationContextRewrite.scala:4)
      at vct.col.ast.VerificationContext.rewrite(Node.scala:95)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewriteDefault(VerificationContextRewrite.scala:3)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewriteDefault$(VerificationContextRewrite.scala:3)
      at vct.col.ast.VerificationContext.rewriteDefault(Node.scala:95)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:166)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:166)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:5)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:5)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.VerificationRewrite.$anonfun$rewrite$1(VerificationRewrite.scala:6)
      at scala.collection.immutable.List.map(List.scala:246)
      at scala.collection.immutable.List.map(List.scala:79)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewrite(VerificationRewrite.scala:6)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewrite$(VerificationRewrite.scala:4)
      at vct.col.ast.Verification.rewrite(Node.scala:94)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewriteDefault(VerificationRewrite.scala:3)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewriteDefault$(VerificationRewrite.scala:3)
      at vct.col.ast.Verification.rewriteDefault(Node.scala:94)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:165)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:165)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:4)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:4)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.main.stages.Transformation.$anonfun$run$4(Transformation.scala:126)
      at vct.main.stages.Transformation.$anonfun$run$4$adapted(Transformation.scala:121)
      at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
      at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
      at scala.collection.AbstractIterator.foreach(Iterator.scala:1300)
      at hre.progress.Progress$.foreach(Progress.scala:83)
      at vct.main.stages.Transformation.$anonfun$run$2(Transformation.scala:121)
      at hre.debug.TimeTravel$.safelyRepeatable(TimeTravel.scala:31)
      at vct.main.stages.Transformation.run(Transformation.scala:118)
      at vct.main.stages.Transformation.run(Transformation.scala:96)
      at hre.stages.Stages.$anonfun$run$3(Stages.scala:28)
      at hre.stages.Stages.$anonfun$run$3$adapted(Stages.scala:26)
      at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
      at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
      at scala.collection.AbstractIterable.foreach(Iterable.scala:933)
      at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:903)
      at hre.stages.Stages.$anonfun$run$1(Stages.scala:26)
      at hre.progress.Progress$.stages(Progress.scala:104)
      at hre.stages.Stages.run(Stages.scala:23)
      at hre.stages.Stages.run$(Stages.scala:20)
      at hre.stages.StagesPair.run(Stages.scala:52)
      at vct.main.modes.Verify$.verifyWithOptions(Verify.scala:49)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$2(VercorsSpec.scala:95)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
      at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
      at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
      at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
      at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$1(VercorsSpec.scala:85)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
      at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
      at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
      at org.scalatest.Transformer.apply(Transformer.scala:22)
      at org.scalatest.Transformer.apply(Transformer.scala:20)
      at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
      at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
      at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
      at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
      at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
      at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
      at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
      at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
      at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
      at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.run(Suite.scala:1112)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
      at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
      at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
      at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
      at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
      at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
      at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
      at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
      at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
      at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
      at org.scalatest.Suite.run(Suite.scala:1109)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
      at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
      at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
      at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
      at org.scalatest.tools.Runner$.main(Runner.scala:775)
      at org.scalatest.tools.Runner.main(Runner.scala)

Check failure on line 120 in test/main/vct/test/integration/helper/VercorsSpec.scala

See this annotation in the file changed.

@github-actions github-actions / TestReport

vct.test.integration.examples.CSpec ► Examples examples/concepts/c/structs.c produces verdict pass with Silicon 

Failed test found in:
  reports/ubuntu-6/TEST-vct.test.integration.examples.CSpec.xml
Error:
        org.scalatest.exceptions.TestFailedException: Expected the test to pass, but it crashed with the above error instead.
Raw output 
      org.scalatest.exceptions.TestFailedException: Expected the test to pass, but it crashed with the above error instead.
      at org.scalatest.Assertions.newAssertionFailedException(Assertions.scala:472)
      at org.scalatest.Assertions.newAssertionFailedException$(Assertions.scala:471)
      at org.scalatest.flatspec.AnyFlatSpec.newAssertionFailedException(AnyFlatSpec.scala:1685)
      at org.scalatest.Assertions.fail(Assertions.scala:933)
      at org.scalatest.Assertions.fail$(Assertions.scala:929)
      at org.scalatest.flatspec.AnyFlatSpec.fail(AnyFlatSpec.scala:1685)
      at vct.test.integration.helper.VercorsSpec.matchVerdict(VercorsSpec.scala:120)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$2(VercorsSpec.scala:86)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
      at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
      at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
      at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
      at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$1(VercorsSpec.scala:85)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
      at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
      at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
      at org.scalatest.Transformer.apply(Transformer.scala:22)
      at org.scalatest.Transformer.apply(Transformer.scala:20)
      at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
      at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
      at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
      at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
      at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
      at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
      at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
      at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
      at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
      at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.run(Suite.scala:1112)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
      at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
      at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
      at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
      at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
      at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
      at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
      at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
      at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
      at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
      at org.scalatest.Suite.run(Suite.scala:1109)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
      at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
      at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
      at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
      at org.scalatest.tools.Runner$.main(Runner.scala:775)
      at org.scalatest.tools.Runner.main(Runner.scala)

Check failure on line 46 in src/col/vct/col/typerules/CoercingRewriter.scala

See this annotation in the file changed.

@github-actions github-actions / TestReport

vct.test.integration.examples.CSpec ► Free offset 1 pointer produces verdict fail with Silicon 

Failed test found in:
  reports/ubuntu-6/TEST-vct.test.integration.examples.CSpec.xml
Error:
        scala.NotImplementedError: an implementation is missing
Raw output 
      scala.NotImplementedError: an implementation is missing
      at scala.Predef$.$qmark$qmark$qmark(Predef.scala:344)
      at vct.col.rewrite.adt.ImportArrayPointer.postCoerce(ImportPointer.scala:263)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:25)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:21)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.$anonfun$dispatch$1(BaseCoercingRewriter.scala:23)
      at vct.col.typerules.CoercingRewriter.applyCoercion(CoercingRewriter.scala:70)
      at vct.col.rewrite.adt.ImportArrayPointer.applyCoercion(ImportPointer.scala:196)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:23)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:21)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.InvokeProcedureRewrite.$anonfun$rewrite$2(InvokeProcedureRewrite.scala:9)
      at scala.collection.immutable.List.map(List.scala:250)
      at scala.collection.immutable.List.map(List.scala:79)
      at vct.col.ast.ops.rewrite.InvokeProcedureRewrite.rewrite(InvokeProcedureRewrite.scala:9)
      at vct.col.ast.ops.rewrite.InvokeProcedureRewrite.rewrite$(InvokeProcedureRewrite.scala:4)
      at vct.col.ast.InvokeProcedure.rewrite(Node.scala:226)
      at vct.col.ast.ops.rewrite.InvokeProcedureRewrite.rewriteDefault(InvokeProcedureRewrite.scala:3)
      at vct.col.ast.ops.rewrite.InvokeProcedureRewrite.rewriteDefault$(InvokeProcedureRewrite.scala:3)
      at vct.col.ast.InvokeProcedure.rewriteDefault(Node.scala:226)
      at vct.col.ast.InvokeProcedure.rewriteDefault(Node.scala:226)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:173)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:173)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:12)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:12)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.BlockRewrite.$anonfun$rewrite$1(BlockRewrite.scala:6)
      at scala.collection.immutable.List.map(List.scala:250)
      at scala.collection.immutable.List.map(List.scala:79)
      at vct.col.ast.ops.rewrite.BlockRewrite.rewrite(BlockRewrite.scala:6)
      at vct.col.ast.ops.rewrite.BlockRewrite.rewrite$(BlockRewrite.scala:4)
      at vct.col.ast.Block.rewrite(Node.scala:235)
      at vct.col.ast.ops.rewrite.BlockRewrite.rewriteDefault(BlockRewrite.scala:3)
      at vct.col.ast.ops.rewrite.BlockRewrite.rewriteDefault$(BlockRewrite.scala:3)
      at vct.col.ast.Block.rewriteDefault(Node.scala:235)
      at vct.col.ast.Block.rewriteDefault(Node.scala:235)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:173)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:173)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:12)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:12)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.ScopeRewrite.$anonfun$rewrite$4(ScopeRewrite.scala:13)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ScopeRewrite.$anonfun$rewrite$3(ScopeRewrite.scala:8)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ScopeRewrite.$anonfun$rewrite$2(ScopeRewrite.scala:7)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ScopeRewrite.$anonfun$rewrite$1(ScopeRewrite.scala:6)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ScopeRewrite.rewrite(ScopeRewrite.scala:5)
      at vct.col.ast.ops.rewrite.ScopeRewrite.rewrite$(ScopeRewrite.scala:4)
      at vct.col.ast.Scope.rewrite(Node.scala:236)
      at vct.col.ast.ops.rewrite.ScopeRewrite.rewriteDefault(ScopeRewrite.scala:3)
      at vct.col.ast.ops.rewrite.ScopeRewrite.rewriteDefault$(ScopeRewrite.scala:3)
      at vct.col.ast.Scope.rewriteDefault(Node.scala:236)
      at vct.col.ast.Scope.rewriteDefault(Node.scala:236)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:173)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:173)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:12)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:12)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.$anonfun$rewrite$2(ProcedureRewrite.scala:19)
      at scala.Option.map(Option.scala:242)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.$anonfun$rewrite$1(ProcedureRewrite.scala:19)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewrite(ProcedureRewrite.scala:5)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewrite$(ProcedureRewrite.scala:4)
      at vct.col.ast.Procedure.rewrite(Node.scala:262)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewriteDefault(ProcedureRewrite.scala:3)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewriteDefault$(ProcedureRewrite.scala:3)
      at vct.col.ast.Procedure.rewriteDefault(Node.scala:262)
      at vct.col.ast.Procedure.rewriteDefault(Node.scala:262)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:273)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:277)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$4(ImportADT.scala:96)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$4$adapted(ImportADT.scala:96)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$3(ImportADT.scala:96)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.collect(Scopes.scala:68)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$2(ImportADT.scala:96)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$6(ProgramRewrite.scala:11)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$5(ProgramRewrite.scala:10)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$4(ProgramRewrite.scala:9)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$3(ProgramRewrite.scala:8)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$2(ProgramRewrite.scala:7)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$1(ProgramRewrite.scala:6)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.rewrite(ProgramRewrite.scala:5)
      at vct.col.ast.ops.rewrite.ProgramRewrite.rewrite$(ProgramRewrite.scala:4)
      at vct.col.ast.Program.rewrite(Node.scala:104)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$1(ImportADT.scala:95)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.rewrite.adt.ImportADT.postCoerce(ImportADT.scala:95)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:6)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:6)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewrite(VerificationContextRewrite.scala:6)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewrite$(VerificationContextRewrite.scala:4)
      at vct.col.ast.VerificationContext.rewrite(Node.scala:95)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewriteDefault(VerificationContextRewrite.scala:3)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewriteDefault$(VerificationContextRewrite.scala:3)
      at vct.col.ast.VerificationContext.rewriteDefault(Node.scala:95)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:166)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:166)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:5)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:5)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.VerificationRewrite.$anonfun$rewrite$1(VerificationRewrite.scala:6)
      at scala.collection.immutable.List.map(List.scala:246)
      at scala.collection.immutable.List.map(List.scala:79)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewrite(VerificationRewrite.scala:6)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewrite$(VerificationRewrite.scala:4)
      at vct.col.ast.Verification.rewrite(Node.scala:94)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewriteDefault(VerificationRewrite.scala:3)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewriteDefault$(VerificationRewrite.scala:3)
      at vct.col.ast.Verification.rewriteDefault(Node.scala:94)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:165)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:165)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:4)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:4)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.main.stages.Transformation.$anonfun$run$4(Transformation.scala:126)
      at vct.main.stages.Transformation.$anonfun$run$4$adapted(Transformation.scala:121)
      at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
      at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
      at scala.collection.AbstractIterator.foreach(Iterator.scala:1300)
      at hre.progress.Progress$.foreach(Progress.scala:83)
      at vct.main.stages.Transformation.$anonfun$run$2(Transformation.scala:121)
      at hre.debug.TimeTravel$.safelyRepeatable(TimeTravel.scala:31)
      at vct.main.stages.Transformation.run(Transformation.scala:118)
      at vct.main.stages.Transformation.run(Transformation.scala:96)
      at hre.stages.Stages.$anonfun$run$3(Stages.scala:28)
      at hre.stages.Stages.$anonfun$run$3$adapted(Stages.scala:26)
      at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
      at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
      at scala.collection.AbstractIterable.foreach(Iterable.scala:933)
      at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:903)
      at hre.stages.Stages.$anonfun$run$1(Stages.scala:26)
      at hre.progress.Progress$.stages(Progress.scala:104)
      at hre.stages.Stages.run(Stages.scala:23)
      at hre.stages.Stages.run$(Stages.scala:20)
      at hre.stages.StagesPair.run(Stages.scala:52)
      at vct.main.modes.Verify$.verifyWithOptions(Verify.scala:49)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$2(VercorsSpec.scala:90)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
      at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
      at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
      at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
      at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$1(VercorsSpec.scala:85)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
      at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
      at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
      at org.scalatest.Transformer.apply(Transformer.scala:22)
      at org.scalatest.Transformer.apply(Transformer.scala:20)
      at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
      at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
      at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
      at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
      at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
      at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
      at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
      at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
      at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
      at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.run(Suite.scala:1112)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
      at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
      at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
      at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
      at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
      at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
      at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
      at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
      at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
      at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
      at org.scalatest.Suite.run(Suite.scala:1109)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
      at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
      at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
      at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
      at org.scalatest.tools.Runner$.main(Runner.scala:775)
      at org.scalatest.tools.Runner.main(Runner.scala)

Check failure on line 46 in src/col/vct/col/typerules/CoercingRewriter.scala

See this annotation in the file changed.

@github-actions github-actions / TestReport

vct.test.integration.examples.PointerSpec ► Examples examples/concepts/pointerArithmetic/pointerSubtract.c produces verdict pass with Silicon 

Failed test found in:
  reports/ubuntu-7/TEST-vct.test.integration.examples.PointerSpec.xml
Error:
        scala.NotImplementedError: an implementation is missing
Raw output 
      scala.NotImplementedError: an implementation is missing
      at scala.Predef$.$qmark$qmark$qmark(Predef.scala:344)
      at vct.col.rewrite.adt.ImportArrayPointer.postCoerce(ImportPointer.scala:263)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:25)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:21)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.$anonfun$dispatch$1(BaseCoercingRewriter.scala:23)
      at vct.col.typerules.CoercingRewriter.applyCoercion(CoercingRewriter.scala:70)
      at vct.col.rewrite.adt.ImportArrayPointer.applyCoercion(ImportPointer.scala:196)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:23)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:21)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.NeqRewrite.rewrite(NeqRewrite.scala:6)
      at vct.col.ast.ops.rewrite.NeqRewrite.rewrite$(NeqRewrite.scala:4)
      at vct.col.ast.Neq.rewrite(Node.scala:632)
      at vct.col.ast.ops.rewrite.NeqRewrite.rewriteDefault(NeqRewrite.scala:3)
      at vct.col.ast.ops.rewrite.NeqRewrite.rewriteDefault$(NeqRewrite.scala:3)
      at vct.col.ast.Neq.rewriteDefault(Node.scala:632)
      at vct.col.ast.Neq.rewriteDefault(Node.scala:632)
      at vct.col.ast.AbstractRewriter.rewriteDefault(AbstractRewriter.scala:118)
      at vct.col.ast.AbstractRewriter.rewriteDefault$(AbstractRewriter.scala:118)
      at vct.col.typerules.CoercingRewriter.rewriteDefault(CoercingRewriter.scala:46)
      at vct.col.rewrite.adt.ImportArrayPointer.postCoerce(ImportPointer.scala:282)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:25)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:21)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.$anonfun$dispatch$1(BaseCoercingRewriter.scala:23)
      at vct.col.typerules.CoercingRewriter.applyCoercion(CoercingRewriter.scala:172)
      at vct.col.rewrite.adt.ImportArrayPointer.applyCoercion(ImportPointer.scala:196)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:23)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:21)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.UnitAccountedPredicateRewrite.rewrite(UnitAccountedPredicateRewrite.scala:6)
      at vct.col.ast.ops.rewrite.UnitAccountedPredicateRewrite.rewrite$(UnitAccountedPredicateRewrite.scala:4)
      at vct.col.ast.UnitAccountedPredicate.rewrite(Node.scala:361)
      at vct.col.ast.ops.rewrite.UnitAccountedPredicateRewrite.rewriteDefault(UnitAccountedPredicateRewrite.scala:3)
      at vct.col.ast.ops.rewrite.UnitAccountedPredicateRewrite.rewriteDefault$(UnitAccountedPredicateRewrite.scala:3)
      at vct.col.ast.UnitAccountedPredicate.rewriteDefault(Node.scala:361)
      at vct.col.ast.UnitAccountedPredicate.rewriteDefault(Node.scala:361)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:179)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:179)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:18)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:18)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.SplitAccountedPredicateRewrite.rewrite(SplitAccountedPredicateRewrite.scala:9)
      at vct.col.ast.ops.rewrite.SplitAccountedPredicateRewrite.rewrite$(SplitAccountedPredicateRewrite.scala:4)
      at vct.col.ast.SplitAccountedPredicate.rewrite(Node.scala:362)
      at vct.col.ast.ops.rewrite.SplitAccountedPredicateRewrite.rewriteDefault(SplitAccountedPredicateRewrite.scala:3)
      at vct.col.ast.ops.rewrite.SplitAccountedPredicateRewrite.rewriteDefault$(SplitAccountedPredicateRewrite.scala:3)
      at vct.col.ast.SplitAccountedPredicate.rewriteDefault(Node.scala:362)
      at vct.col.ast.SplitAccountedPredicate.rewriteDefault(Node.scala:362)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:179)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:179)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:18)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:18)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.ApplicableContractRewrite.rewrite(ApplicableContractRewrite.scala:9)
      at vct.col.ast.ops.rewrite.ApplicableContractRewrite.rewrite$(ApplicableContractRewrite.scala:4)
      at vct.col.ast.ApplicableContract.rewrite(Node.scala:356)
      at vct.col.ast.ops.rewrite.ApplicableContractRewrite.rewriteDefault(ApplicableContractRewrite.scala:3)
      at vct.col.ast.ops.rewrite.ApplicableContractRewrite.rewriteDefault$(ApplicableContractRewrite.scala:3)
      at vct.col.ast.ApplicableContract.rewriteDefault(Node.scala:356)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:178)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:178)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:17)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:17)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.$anonfun$rewrite$1(ProcedureRewrite.scala:22)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewrite(ProcedureRewrite.scala:5)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewrite$(ProcedureRewrite.scala:4)
      at vct.col.ast.Procedure.rewrite(Node.scala:262)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewriteDefault(ProcedureRewrite.scala:3)
      at vct.col.ast.ops.rewrite.ProcedureRewrite.rewriteDefault$(ProcedureRewrite.scala:3)
      at vct.col.ast.Procedure.rewriteDefault(Node.scala:262)
      at vct.col.ast.Procedure.rewriteDefault(Node.scala:262)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:273)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:277)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$4(ImportADT.scala:96)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$4$adapted(ImportADT.scala:96)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$3(ImportADT.scala:96)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.collect(Scopes.scala:68)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$2(ImportADT.scala:96)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$6(ProgramRewrite.scala:11)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$5(ProgramRewrite.scala:10)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$4(ProgramRewrite.scala:9)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$3(ProgramRewrite.scala:8)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$2(ProgramRewrite.scala:7)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.$anonfun$rewrite$1(ProgramRewrite.scala:6)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.util.Scopes.scope(Scopes.scala:60)
      at vct.col.ast.ops.rewrite.ProgramRewrite.rewrite(ProgramRewrite.scala:5)
      at vct.col.ast.ops.rewrite.ProgramRewrite.rewrite$(ProgramRewrite.scala:4)
      at vct.col.ast.Program.rewrite(Node.scala:104)
      at vct.col.rewrite.adt.ImportADT.$anonfun$postCoerce$1(ImportADT.scala:95)
      at hre.util.ScopedStack.having(ScopedStack.scala:36)
      at vct.col.rewrite.adt.ImportADT.postCoerce(ImportADT.scala:95)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:6)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:6)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewrite(VerificationContextRewrite.scala:6)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewrite$(VerificationContextRewrite.scala:4)
      at vct.col.ast.VerificationContext.rewrite(Node.scala:95)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewriteDefault(VerificationContextRewrite.scala:3)
      at vct.col.ast.ops.rewrite.VerificationContextRewrite.rewriteDefault$(VerificationContextRewrite.scala:3)
      at vct.col.ast.VerificationContext.rewriteDefault(Node.scala:95)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:166)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:166)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:5)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:5)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.col.ast.ops.rewrite.VerificationRewrite.$anonfun$rewrite$1(VerificationRewrite.scala:6)
      at scala.collection.immutable.List.map(List.scala:246)
      at scala.collection.immutable.List.map(List.scala:79)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewrite(VerificationRewrite.scala:6)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewrite$(VerificationRewrite.scala:4)
      at vct.col.ast.Verification.rewrite(Node.scala:94)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewriteDefault(VerificationRewrite.scala:3)
      at vct.col.ast.ops.rewrite.VerificationRewrite.rewriteDefault$(VerificationRewrite.scala:3)
      at vct.col.ast.Verification.rewriteDefault(Node.scala:94)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce(BaseCoercingRewriter.scala:165)
      at vct.col.ast.rewrite.BaseCoercingRewriter.postCoerce$(BaseCoercingRewriter.scala:165)
      at vct.col.typerules.CoercingRewriter.postCoerce(CoercingRewriter.scala:46)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch(BaseCoercingRewriter.scala:4)
      at vct.col.ast.rewrite.BaseCoercingRewriter.dispatch$(BaseCoercingRewriter.scala:4)
      at vct.col.typerules.CoercingRewriter.dispatch(CoercingRewriter.scala:46)
      at vct.main.stages.Transformation.$anonfun$run$4(Transformation.scala:126)
      at vct.main.stages.Transformation.$anonfun$run$4$adapted(Transformation.scala:121)
      at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
      at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
      at scala.collection.AbstractIterator.foreach(Iterator.scala:1300)
      at hre.progress.Progress$.foreach(Progress.scala:83)
      at vct.main.stages.Transformation.$anonfun$run$2(Transformation.scala:121)
      at hre.debug.TimeTravel$.safelyRepeatable(TimeTravel.scala:31)
      at vct.main.stages.Transformation.run(Transformation.scala:118)
      at vct.main.stages.Transformation.run(Transformation.scala:96)
      at hre.stages.Stages.$anonfun$run$3(Stages.scala:28)
      at hre.stages.Stages.$anonfun$run$3$adapted(Stages.scala:26)
      at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
      at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
      at scala.collection.AbstractIterable.foreach(Iterable.scala:933)
      at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:903)
      at hre.stages.Stages.$anonfun$run$1(Stages.scala:26)
      at hre.progress.Progress$.stages(Progress.scala:104)
      at hre.stages.Stages.run(Stages.scala:23)
      at hre.stages.Stages.run$(Stages.scala:20)
      at hre.stages.StagesPair.run(Stages.scala:52)
      at vct.main.modes.Verify$.verifyWithOptions(Verify.scala:49)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$2(VercorsSpec.scala:90)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
      at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
      at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
      at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
      at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$1(VercorsSpec.scala:85)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
      at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
      at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
      at org.scalatest.Transformer.apply(Transformer.scala:22)
      at org.scalatest.Transformer.apply(Transformer.scala:20)
      at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
      at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
      at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
      at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
      at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
      at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
      at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
      at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
      at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
      at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.run(Suite.scala:1112)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
      at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
      at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
      at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
      at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
      at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
      at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
      at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
      at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
      at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
      at org.scalatest.Suite.run(Suite.scala:1109)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
      at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
      at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
      at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
      at org.scalatest.tools.Runner$.main(Runner.scala:775)
      at org.scalatest.tools.Runner.main(Runner.scala)

Check failure on line 124 in test/main/vct/test/integration/helper/VercorsSpec.scala

See this annotation in the file changed.

@github-actions github-actions / TestReport

vct.test.integration.examples.SYCLFullProgramsSpec ► Examples examples/concepts/sycl/fullExamples/MatrixTransposeWithF.cpp produces verdict pass with Silicon 

Failed test found in:
  reports/ubuntu-7/TEST-vct.test.integration.examples.SYCLFullProgramsSpec.xml
Error:
        org.scalatest.exceptions.TestFailedException: Expected the test to pass, but it returned verification failures instead.
Raw output 
      org.scalatest.exceptions.TestFailedException: Expected the test to pass, but it returned verification failures instead.
      at org.scalatest.Assertions.newAssertionFailedException(Assertions.scala:472)
      at org.scalatest.Assertions.newAssertionFailedException$(Assertions.scala:471)
      at org.scalatest.flatspec.AnyFlatSpec.newAssertionFailedException(AnyFlatSpec.scala:1685)
      at org.scalatest.Assertions.fail(Assertions.scala:933)
      at org.scalatest.Assertions.fail$(Assertions.scala:929)
      at org.scalatest.flatspec.AnyFlatSpec.fail(AnyFlatSpec.scala:1685)
      at vct.test.integration.helper.VercorsSpec.matchVerdict(VercorsSpec.scala:124)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$2(VercorsSpec.scala:86)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.enablers.Timed$$anon$1.timeoutAfter(Timed.scala:127)
      at org.scalatest.concurrent.TimeLimits$.failAfterImpl(TimeLimits.scala:282)
      at org.scalatest.concurrent.TimeLimits.failAfter(TimeLimits.scala:231)
      at org.scalatest.concurrent.TimeLimits.failAfter$(TimeLimits.scala:230)
      at org.scalatest.concurrent.TimeLimits$.failAfter(TimeLimits.scala:274)
      at vct.test.integration.helper.VercorsSpec.$anonfun$registerTest$1(VercorsSpec.scala:85)
      at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
      at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
      at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
      at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
      at org.scalatest.Transformer.apply(Transformer.scala:22)
      at org.scalatest.Transformer.apply(Transformer.scala:20)
      at org.scalatest.flatspec.AnyFlatSpecLike$$anon$5.apply(AnyFlatSpecLike.scala:1684)
      at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
      at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
      at org.scalatest.flatspec.AnyFlatSpec.withFixture(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.invokeWithFixture$1(AnyFlatSpecLike.scala:1682)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTest$1(AnyFlatSpecLike.scala:1694)
      at org.scalatest.SuperEngine.runTestImpl(Engine.scala:306)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest(AnyFlatSpecLike.scala:1694)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTest$(AnyFlatSpecLike.scala:1676)
      at org.scalatest.flatspec.AnyFlatSpec.runTest(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$runTests$1(AnyFlatSpecLike.scala:1752)
      at org.scalatest.SuperEngine.$anonfun$runTestsInBranch$1(Engine.scala:413)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:401)
      at org.scalatest.SuperEngine.runTestsInBranch(Engine.scala:396)
      at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:475)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests(AnyFlatSpecLike.scala:1752)
      at org.scalatest.flatspec.AnyFlatSpecLike.runTests$(AnyFlatSpecLike.scala:1751)
      at org.scalatest.flatspec.AnyFlatSpec.runTests(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.run(Suite.scala:1112)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.flatspec.AnyFlatSpec.org$scalatest$flatspec$AnyFlatSpecLike$$super$run(AnyFlatSpec.scala:1685)
      at org.scalatest.flatspec.AnyFlatSpecLike.$anonfun$run$1(AnyFlatSpecLike.scala:1797)
      at org.scalatest.SuperEngine.runImpl(Engine.scala:535)
      at org.scalatest.flatspec.AnyFlatSpecLike.run(AnyFlatSpecLike.scala:1797)
      at org.scalatest.flatspec.AnyFlatSpecLike.run$(AnyFlatSpecLike.scala:1795)
      at org.scalatest.flatspec.AnyFlatSpec.run(AnyFlatSpec.scala:1685)
      at org.scalatest.Suite.callExecuteOnSuite$1(Suite.scala:1175)
      at org.scalatest.Suite.$anonfun$runNestedSuites$1(Suite.scala:1222)
      at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
      at org.scalatest.Suite.runNestedSuites(Suite.scala:1220)
      at org.scalatest.Suite.runNestedSuites$(Suite.scala:1154)
      at org.scalatest.tools.DiscoverySuite.runNestedSuites(DiscoverySuite.scala:30)
      at org.scalatest.Suite.run(Suite.scala:1109)
      at org.scalatest.Suite.run$(Suite.scala:1094)
      at org.scalatest.tools.DiscoverySuite.run(DiscoverySuite.scala:30)
      at org.scalatest.tools.SuiteRunner.run(SuiteRunner.scala:45)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13(Runner.scala:1322)
      at org.scalatest.tools.Runner$.$anonfun$doRunRunRunDaDoRunRun$13$adapted(Runner.scala:1316)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at org.scalatest.tools.Runner$.doRunRunRunDaDoRunRun(Runner.scala:1316)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24(Runner.scala:993)
      at org.scalatest.tools.Runner$.$anonfun$runOptionallyWithPassFailReporter$24$adapted(Runner.scala:971)
      at org.scalatest.tools.Runner$.withClassLoaderAndDispatchReporter(Runner.scala:1482)
      at org.scalatest.tools.Runner$.runOptionallyWithPassFailReporter(Runner.scala:971)
      at org.scalatest.tools.Runner$.main(Runner.scala:775)
      at org.scalatest.tools.Runner.main(Runner.scala)
View more details on GitHub Actions