7
edits
Abstract Interpretation: Difference between revisions
Jump to navigation
Jump to search
→Interpreting Branch Conditions
mNo edit summary |
|||
| Line 301: | Line 301: | ||
== 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: | Way back in our original example, you may have noticed a fact that our abstract interpretation failed to discover: 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. | 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. | ||