VerCors crashes on modulo with zero

[ArmborstL]

The following C program computes a modulo with k, which might be zero:

int main() {
    int i;
    int k = i;
    //@ assert (i % k == 0 || k == 0);
    return 0;
}

VerCors transforms the file successfully and hands it to Viper, but then crashes with

[ERROR] Unrecoverable error: class vct.col.ast.Local cannot be cast to class vct.col.ast.DividingExpr (vct.col.ast.Local and vct.col.ast.DividingExpr are in unnamed module of loader 'app')
java.lang.ClassCastException: class vct.col.ast.Local cannot be cast to class vct.col.ast.DividingExpr (vct.col.ast.Local and vct.col.ast.DividingExpr are in unnamed module of loader 'app')
        at viper.api.backend.SilverBackend.defer(SilverBackend.scala:303)
        at viper.api.backend.SilverBackend.defer$(SilverBackend.scala:301)
        at viper.api.backend.silicon.Silicon.defer(Silicon.scala:41)
        at viper.api.backend.SilverBackend.processError(SilverBackend.scala:176)
        at viper.api.backend.SilverBackend.processError$(SilverBackend.scala:118)
        at viper.api.backend.silicon.Silicon.processError(Silicon.scala:41)
        at viper.api.backend.SilverBackend.$anonfun$submit$9(SilverBackend.scala:108)
        at viper.api.backend.SilverBackend.$anonfun$submit$9$adapted(SilverBackend.scala:108)
        at scala.collection.immutable.List.foreach(List.scala:333)
        at viper.api.backend.SilverBackend.submit(SilverBackend.scala:108)
        at viper.api.backend.SilverBackend.submit$(SilverBackend.scala:59)
        at viper.api.backend.silicon.Silicon.submit(Silicon.scala:41)
        at vct.main.stages.SilverBackend.verify(Backend.scala:118)

Inspecting the generated backend file with viper directly, it reports "Assert might fail. Divisor k might be zero."

Swapping the order of the two disjuncts (such that the zero check is done first) fixes the issue and VerCors verifies successfully.

[Drevanoorschot]

I have observed similar behaviour with the following PVL program:

int div(int x, int y) {
    return x / y;
}

which drops the following stack trace:

Exception in thread "main" java.lang.ClassCastException: class vct.col.ast.Local cannot be cast to class vct.col.ast.DividingExpr (vct.col.ast.Local and vct.col.ast.DividingExpr are in unnamed module of loader 'app')
	at viper.api.backend.SilverBackend.defer(SilverBackend.scala:307)
	at viper.api.backend.SilverBackend.defer$(SilverBackend.scala:305)
	at viper.api.backend.silicon.Silicon.defer(Silicon.scala:41)
	at viper.api.backend.SilverBackend.processError(SilverBackend.scala:136)
	at viper.api.backend.SilverBackend.processError$(SilverBackend.scala:122)
	at viper.api.backend.silicon.Silicon.processError(Silicon.scala:41)
	at viper.api.backend.SilverBackend.$anonfun$submit$9(SilverBackend.scala:113)
	at viper.api.backend.SilverBackend.$anonfun$submit$9$adapted(SilverBackend.scala:113)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at viper.api.backend.SilverBackend.submit(SilverBackend.scala:113)
	at viper.api.backend.SilverBackend.submit$(SilverBackend.scala:59)
	at viper.api.backend.silicon.Silicon.submit(Silicon.scala:41)
	at vct.main.stages.SilverBackend.verify(Backend.scala:119)
	at vct.main.stages.Backend.$anonfun$run$3(Backend.scala:108)
	at vct.main.stages.Backend.$anonfun$cachedDefinitelyVerifiesOrElseUpdate$1(Backend.scala:74)
	at scala.Option.getOrElse(Option.scala:201)
	at vct.main.stages.Backend.cachedDefinitelyVerifiesOrElseUpdate(Backend.scala:72)
	at vct.main.stages.Backend.cachedDefinitelyVerifiesOrElseUpdate$(Backend.scala:71)
	at vct.main.stages.SilverBackend.cachedDefinitelyVerifiesOrElseUpdate(Backend.scala:117)
	at vct.main.stages.Backend.$anonfun$run$2(Backend.scala:108)
	at vct.main.stages.Backend.$anonfun$run$2$adapted(Backend.scala:107)
	at hre.progress.Progress$.$anonfun$foreach$2(Progress.scala:78)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
	at hre.progress.task.AbstractTask.frame(AbstractTask.scala:143)
	at hre.progress.Progress$.$anonfun$foreach$1(Progress.scala:78)
	at hre.progress.Progress$.$anonfun$foreach$1$adapted(Progress.scala:76)
	at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)
	at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)
	at scala.collection.AbstractIterator.foreach(Iterator.scala:1288)
	at hre.progress.Progress$.foreach(Progress.scala:76)
	at vct.main.stages.Backend.run(Backend.scala:107)
	at vct.main.stages.Backend.run$(Backend.scala:106)
	at vct.main.stages.SilverBackend.run(Backend.scala:117)
	at vct.main.stages.SilverBackend.run(Backend.scala:117)
	at hre.stages.UnitStages.runUnsafely(Stages.scala:42)
	at hre.stages.StagesPair.runUnsafely(Stages.scala:50)
	at hre.stages.StagesPair.runUnsafely(Stages.scala:48)
	at hre.stages.Stages.$anonfun$run$1(Stages.scala:27)
	at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:13)
	at hre.progress.Progress$.stages(Progress.scala:101)
	at hre.stages.Stages.run(Stages.scala:26)
	at hre.stages.Stages.run$(Stages.scala:24)
	at hre.stages.StagesPair.run(Stages.scala:46)
	at vct.main.modes.Verify$.verifyWithOptions(Verify.scala:46)
	at vct.main.modes.Verify$.runOptions(Verify.scala:74)
	at vct.main.Main$.runOptions(Main.scala:88)
	at vct.main.Main$.main(Main.scala:41)
	at vct.main.Main.main(Main.scala)

When placing a breakpoint where the exception is thrown, it does however report the verification error reason: "Divisor y might be zero."

[bobismijnnaam]

This should be fixed in commit 11f483b5ea01bb9ce8a2e21891c02b4265dd3abd, which I hope I can merge into dev soon.