7
edits
Changes
→Interpreting Branch Conditions
== Interpreting Branch Conditions ==
Way back in our original example, you may have noticed a fact that our abstract interpretation failed to discover: than that m is constant with value zero at the end of the function. The reason we don't discover this is that on the "a == 0" branch of the conditional, we do "m := a", and our state has "a = ?", so we set "m = ?". But if we're on the "a == 0" branch, then a has to be zero, right?
Of course. But basic abstract interpretation doesn't try to interpret branch conditions. One reason is that the branch has no side effects, so interpreting it abstractly doesn't assign anything.
