Dividing by zero
sakehl opened 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.
pieter-bos commented
duplicate of #965 (thanks though)
sakehl commented
Ah, woops missed that issue, but thanks!