Comment by hyghjiyhu

Imo if you run into the halting problem it's because you are trying to do too much. In particular I think what you actually want is to check soundness based on the "shape" of the code rather than the reason about which variables can have which values and what that means for soundness.

  flag=false;
  if flag {
    use_after_free();
  }

can be rejected with a clear conscience.