search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

Missing division by zero treatment in MaySignedOverflow #1419

Closed DrMichaelPetter closed 2 months ago

DrMichaelPetter commented 2 months ago

During the treatment of expressions within the MaySignedOverflow query treatment in base.ml, we compute possible value ranges for expressions. We do so for division expressions too, but do not catch a possible division by zero within this treatment.

The first solution proposal to this would is in the case of such an exception just do the safe thing and return true.

michael-schwarz commented 2 months ago

Can you also maybe commit the example where this used to cause an exception and now works?