utwente-fmt/vercors

Dividing by zero

Closed this issue · 2 comments

sakehl commented

A division by zero error does not get reported correctly anymore.

This program:

int main(){
    int x = 5/0;
}

Gives:

[INFO] Starting verification
[ERROR] Unrecoverable error: class vct.col.ast.IntegerValue cannot be cast to class vct.col.ast.DividingExpr (vct.col.ast.IntegerValue and vct.col.ast.DividingExpr are in unnamed module of loader 'app')
java.lang.ClassCastException: class vct.col.ast.IntegerValue cannot be cast to class vct.col.ast.DividingExpr (vct.col.ast.IntegerValue and vct.col.ast.DividingExpr are in unnamed module of loader 'app')
        at viper.api.backend.SilverBackend.defer(SilverBackend.scala:312)
        at viper.api.backend.SilverBackend.defer$(SilverBackend.scala:310)
        at viper.api.backend.silicon.Silicon.defer(Silicon.scala:42)

I think the Silver backend gives back the divisor (in this case IntegerValue(0)) instead of the whole division.

duplicate of #965 (thanks though)

sakehl commented

Ah, woops missed that issue, but thanks!