Wow! I wasn't expecting that to work. Obviously we know that there is currently no handler for binop_svalue in the constraints so I would have to watch it run with state merging disabled to see how it is managing the unroll. The fact that merging breaks it is indicative of what we are saying though, that the constraint and merge model is currently insufficient.
Hash algorithms may provide a counterexample for legitimate use of overflow. Anyway, I would prefer tracking the split too, but it is a big change. One way is state split, like you say, but that is a pretty invasive change to the way the graph works. The other way is to handle "or constraints" as I have said. This is an invasive change to the constraint model, but arguably the concept of "or" cannot be ignored forever. Thinking about it, I guess currently the concept of "and" is handled by the constraints (all constraints in a model exist as a big "and") and the concept of "or" is handled by the graph. This could be acceptable but we cannot split the graph arbitrarily, so there is currently no way to handle even a basic if (i == 1 || i == 10) what should be a very simple conditional. Handling a hash algorithm, like you say, is good to keep in mind, because we don't want an explosion of possibilities. If done right, the analyzer should understand for hashing that anything + anything => anything, and we see no explosion of state. By "raise an exception" I did mean issue an analyzer warning, yes. Perhaps the simple answer is to just track the svalue as a possible overflow in the state machine and report the warning for certain uses, like the alloc family, as you said. Regardless, proper overflow handling renders my naive binop handler unusable, because all it does is fold the condition and recur. There is basically no logic to it, and once you reenter eval_condition it is not possible to know how you got there.
