Skip to content

Merge branch 'dev' into generic-channels

Sign in for the full log view
GitHub Actions / TestReport failed May 1, 2024 in 1s

1023 passed, 1 failed and 42 skipped

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

Annotations

Check failure on line 241 in src/viper/viper/api/backend/SilverBackend.scala

See this annotation in the file changed.

@github-actions github-actions / TestReport

vct.test.integration.examples.VerifyThisSpec ► Examples examples/verifythis/2019/challenge3_complete.pvl produces verdict pass with Silicon 

Failed test found in:
  reports/ubuntu-0/TEST-vct.test.integration.examples.VerifyThisSpec.xml
Error:
        java.lang.ClassCastException: class vct.col.ast.InvokeProcedure cannot be cast to class vct.col.ast.Invocation (vct.col.ast.InvokeProcedure and vct.col.ast.Invocation are in unnamed module of loader 'app')
Raw output 
      java.lang.ClassCastException: class vct.col.ast.InvokeProcedure cannot be cast to class vct.col.ast.Invocation (vct.col.ast.InvokeProcedure and vct.col.ast.Invocation are in unnamed module of loader 'app')
      at viper.api.backend.SilverBackend.processError(SilverBackend.scala:241)
      at viper.api.backend.SilverBackend.processError$(SilverBackend.scala:137)
      at viper.api.backend.silicon.Silicon.processError(Silicon.scala:42)
      at viper.api.backend.SilverBackend.$anonfun$submit$1(SilverBackend.scala:127)
      at viper.api.backend.SilverBackend.$anonfun$submit$1$adapted(SilverBackend.scala:127)
      at scala.collection.immutable.List.foreach(List.scala:333)
      at viper.api.backend.SilverBackend.submit(SilverBackend.scala:127)
      at viper.api.backend.SilverBackend.submit$(SilverBackend.scala:112)
      at viper.api.backend.silicon.Silicon.submit(Silicon.scala:42)
      at vct.main.stages.SilverBackend.verify(Backend.scala:147)
      at vct.main.stages.Backend.$anonfun$run$6(Backend.scala:126)
      at vct.main.stages.Backend.$anonfun$cachedDefinitelyVerifiesOrElseUpdate$1(Backend.scala:80)
      at scala.Option.getOrElse(Option.scala:201)
      at vct.main.stages.Backend.cachedDefinitelyVerifiesOrElseUpdate(Backend.scala:78)
      at vct.main.stages.Backend.cachedDefinitelyVerifiesOrElseUpdate$(Backend.scala:77)
      at vct.main.stages.SilverBackend.cachedDefinitelyVerifiesOrElseUpdate(Backend.scala:141)
      at vct.main.stages.Backend.$anonfun$run$5(Backend.scala:126)
      at vct.main.stages.Backend.$anonfun$run$5$adapted(Backend.scala:125)
      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.Backend.$anonfun$run$1(Backend.scala:125)
      at hre.progress.Progress$.stages(Progress.scala:104)
      at vct.main.stages.Backend.run(Backend.scala:115)
      at vct.main.stages.Backend.run$(Backend.scala:112)
      at vct.main.stages.SilverBackend.run(Backend.scala:141)
      at vct.main.stages.SilverBackend.run(Backend.scala:141)
      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)
View more details on GitHub Actions