Support assignment in conditional parts of an expression

[keyboardDrummer]

Changes

• Support assignment in conditional parts of an expression

Testing

• Added conditionalAssignmentInExpression test-case to test-file T2_ImpureExpressions

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[atomb]

This looks nice. My one comment could be addressed in a future PR, if at all.

[joscoh]

This seems to have a lot of overlap with #358. What is the difference between them?

[keyboardDrummer]

This seems to have a lot of overlap with #358. What is the difference between them?

This is stacked on top of that PR so it includes all the changes from that one, which sadly GH does not support well. Best to review this after that is merged.

From a user perspective, this PR enables this test:

procedure conditionalAssignmentInExpression(x: int) {
  var y: int := 0;
  var z: int := (if (x > 0) { y := y + 1; } else { 0 }) + y;
  if (x > 0) {
    assert y == 1;
    assert z == 2;
  } else {
    assert z == 0;
    assert y == 0;
  }
}

[joscoh]

Looks good once the partials have been removed. The termination proofs will become easier once #392 is merged.