SCT: wrong handling of while loops

[vbgl]

The following program is secure but the S-CT checker rejects in with an incorrect argument.

bug_887.jazz", line 8 (32-35):
speculative constant type checker: the variable msf is not known to be a msf, only ∅ are

fn test(reg u64 msf x) {
  while {
    msf = #init_msf();
  } (x != 0) {
    msf = #update_msf(x != 0, msf);
    x = 0;
  }
  msf = #update_msf(! (x != 0), msf);
}

Based on a report by Santiago (@sarranz).

[vbgl]

In fact, it is not only the MSF that is wrongly handled. The following program is accepted by the SCT checker (but fortunately rejected by the CT checker).

fn test_venv(#secret reg u64 s) {
  reg u64 i r;
  r = 0;
  i = 0;
  while {
    r = s;
  } (i < 10) {
    r = 0;
    i += 1;
  }
  [r] = 0;
}