search

pirapira / dry-analyzer

Dr. Y's Ethereum Contract Analyzer
GNU Lesser General Public License v2.1
42 stars 10 forks source link

Consider divide by zero #15

Open pirapira opened 8 years ago

pirapira commented 8 years ago

A division instruction should produce two behaviors, one for divide by zero and the other for divide by non-zero. (When the divisor is known to be non-zero, only one behavior is fine.)

Instructions involving division return zero when the divisor is zero. This should be taken into account for *DIV and *MOD instructions.

pirapira commented 8 years ago

Or, we can cut corners by saying "a / 0 = 0 for any a" (like in ssreflect).