Crash report: class vct.col.ast.Loop cannot be cast to class vct.col.ast.Invocation (vct.col.ast.Loop and vct.col.

[marcoeilers]

Crash Message

class vct.col.ast.Loop cannot be cast to class vct.col.ast.Invocation (vct.col.ast.Loop and vct.col.ast.Invocation are in unnamed module of loader 'app')
  at viper.api.backend.SilverBackend.processError(SilverBackend.scala:297)
  at viper.api.backend.SilverBackend.processError$(SilverBackend.scala:172)
  at viper.api.backend.silicon.Silicon.processError(Silicon.scala:34)
  at viper.api.backend.SilverBackend.$anonfun$submit$1(SilverBackend.scala:164)
  at viper.api.backend.SilverBackend.$anonfun$submit$1$adapted(SilverBackend.scala:164)
  at scala.collection.immutable.List.foreach(List.scala:333)
  at viper.api.backend.SilverBackend.submit(SilverBackend.scala:164)
  at viper.api.backend.SilverBackend.submit$(SilverBackend.scala:143)
  at viper.api.backend.silicon.Silicon.submit(Silicon.scala:34)
  at vct.main.stages.SilverBackend.verify(Backend.scala:201)
  at vct.main.stages.Backend.$anonfun$run$6(Backend.scala:166)
  at vct.main.stages.Backend.$anonfun$cachedDefinitelyVerifiesOrElseUpdate$1(Backend.scala:106)
  ...
  at vct.main.Main$.main(Main.scala:50)
  at vct.main.Main.main(Main.scala)

Version Information

• VerCors version 2.2.0
• At commit a6105f9 from branch HEAD (changes=false)

Arguments

/home/marco/git/vercors/examples/concepts/final/finalIntegerImpureError.java

File Inputs

/home/marco/git/vercors/examples/concepts/final/finalIntegerImpureError.java

public class MyClass {

    //@ decreases;
    private int f() {
        while (true) {}
        return 5;
    }

}

Full Log

18:21:51.079 [INFO] Start: VerCors (at 18:21:51)
18:21:56.218 [INFO] Done: VerCors (at 18:21:56, duration: 00:00:05)
18:21:56.221 [ERROR] java.lang.ClassCastException: class vct.col.ast.Loop cannot be cast to class vct.col.ast.Invocation (vct.col.ast.Loop and vct.col.ast.Invocation are in unnamed module of loader 'app')
	at viper.api.backend.SilverBackend.processError(SilverBackend.scala:297)
	at viper.api.backend.SilverBackend.processError$(SilverBackend.scala:172)
	at viper.api.backend.silicon.Silicon.processError(Silicon.scala:34)
	at viper.api.backend.SilverBackend.$anonfun$submit$1(SilverBackend.scala:164)
	at viper.api.backend.SilverBackend.$anonfun$submit$1$adapted(SilverBackend.scala:164)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at viper.api.backend.SilverBackend.submit(SilverBackend.scala:164)
	at viper.api.backend.SilverBackend.submit$(SilverBackend.scala:143)
	at viper.api.backend.silicon.Silicon.submit(Silicon.scala:34)
	at vct.main.stages.SilverBackend.verify(Backend.scala:201)
	at vct.main.stages.Backend.$anonfun$run$6(Backend.scala:166)
	at vct.main.stages.Backend.$anonfun$cachedDefinitelyVerifiesOrElseUpdate$1(Backend.scala:106)
	at scala.Option.getOrElse(Option.scala:201)
	at vct.main.stages.Backend.cachedDefinitelyVerifiesOrElseUpdate(Backend.scala:104)
	at vct.main.stages.Backend.cachedDefinitelyVerifiesOrElseUpdate$(Backend.scala:100)
	at vct.main.stages.SilverBackend.cachedDefinitelyVerifiesOrElseUpdate(Backend.scala:184)
	at vct.main.stages.Backend.$anonfun$run$5(Backend.scala:166)
	at vct.main.stages.Backend.$anonfun$run$5$adapted(Backend.scala:163)
	at hre.progress.Progress$.$anonfun$foreach$2(Progress.scala:25)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
	at hre.progress.task.AbstractTask.frame(AbstractTask.scala:166)
	at hre.progress.Progress$.$anonfun$foreach$1(Progress.scala:25)
	at hre.progress.Progress$.$anonfun$foreach$1$adapted(Progress.scala:24)
	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:24)
	at vct.main.stages.Backend.$anonfun$run$1(Backend.scala:163)
	at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:16)
	at hre.progress.Progress$.stages(Progress.scala:47)
	at vct.main.stages.Backend.run(Backend.scala:145)
	at vct.main.stages.Backend.run$(Backend.scala:137)
	at vct.main.stages.SilverBackend.run(Backend.scala:184)
	at vct.main.stages.SilverBackend.run(Backend.scala:184)
	at hre.stages.Stages.$anonfun$run$3(Stages.scala:104)
	at hre.stages.Stages.$anonfun$run$3$adapted(Stages.scala:101)
	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:101)
	at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:16)
	at hre.progress.Progress$.stages(Progress.scala:47)
	at hre.stages.Stages.run(Stages.scala:98)
	at hre.stages.Stages.run$(Stages.scala:95)
	at hre.stages.StagesPair.run(Stages.scala:145)
	at vct.main.modes.Verify$.verifyWithOptions(Verify.scala:64)
	at vct.main.modes.Verify$.$anonfun$runOptions$3(Verify.scala:99)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.util.Time$.logTime(Time.scala:23)
	at vct.main.modes.Verify$.runOptions(Verify.scala:99)
	at vct.main.Main$.runMode(Main.scala:107)
	at vct.main.Main$.$anonfun$runOptions$3(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.middleware.Middleware$.using(Middleware.scala:78)
	at vct.main.Main$.$anonfun$runOptions$2(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.io.Watch$.booleanWithWatch(Watch.scala:58)
	at vct.main.Main$.$anonfun$runOptions$1(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.middleware.Middleware$.using(Middleware.scala:78)
	at vct.main.Main$.runOptions(Main.scala:95)
	at vct.main.Main$.main(Main.scala:50)
	at vct.main.Main.main(Main.scala)

18:21:56.221 [ERROR] !*!*!*!*!*!*!*!*!*!*!*!
18:21:56.221 [ERROR] ! VerCors has crashed !
18:21:56.221 [ERROR] !*!*!*!*!*!*!*!*!*!*!*!
18:21:56.221 [ERROR] Please report this as a bug here:

[superaxander]

Thanks for the report. This is related to #1065 and #1133. As far as I know we basically don’t handle the cases where the termination checks fail. We should definitely do that at some point though since this message isn’t very helpful.