[HW7] SSA in if-else statement

[3-24]

I wonder if

int a;
if (condition) {
  a = 1;
} else {
  a = 2
}

is SSA form. I think it is okay because we know only one of a=1; and a=2; is executed. If we are using LLVM IR, then we can use the phi node to handle such cases. But the homework asks us to apply SSA on C code.

[moonzoo]

No. To convert the above code to a pure logic formula, both occurrences of a should be distinguished by using new names.

[3-24]

Suppose we have a code with assertion.

int a;
if (condition) {
  a = 1;
} else {
  a = 2
}
assert(stmt)

For integer a, we can express the program logic into the following logic formula.

$$ ((condition \wedge (a = 1)) \vee (\neg condition \wedge (a = 2))) \wedge \neg stmt $$

Then, why do we need to distinguish two occurrences in this case?