Weakest-precondition computation over a loop that carries no invariant splits a disjunctive exit fact into independent conjuncts.
For a loop whose exit condition establishes x == 0 || y == 0, WP emits both x == 0 and y == 0 as separate facts. Each is individually unjustified; only the disjunction follows from the loop exit.
Currently mitigated, not fixed, in spec_inference.rs: when a function has an invariant-less loop with a non-empty havoc target set, the derived conditions are marked vacuous (CONDITION_INFERRED_VACUOUS) and dropped rather than emitted. So inference does not currently produce unsound output from this, but the underlying WP transformer is still wrong, and the mitigation is coarse — it discards conditions that a correct disjunctive treatment would keep.
Found while splitting the overloaded sathard marker into sathard (genuinely hard quantified conditions) and vacuous (unreliable ones) in #20470.
Weakest-precondition computation over a loop that carries no invariant splits a disjunctive exit fact into independent conjuncts.
For a loop whose exit condition establishes
x == 0 || y == 0, WP emits bothx == 0andy == 0as separate facts. Each is individually unjustified; only the disjunction follows from the loop exit.Currently mitigated, not fixed, in
spec_inference.rs: when a function has an invariant-less loop with a non-empty havoc target set, the derived conditions are markedvacuous(CONDITION_INFERRED_VACUOUS) and dropped rather than emitted. So inference does not currently produce unsound output from this, but the underlying WP transformer is still wrong, and the mitigation is coarse — it discards conditions that a correct disjunctive treatment would keep.Found while splitting the overloaded
sathardmarker intosathard(genuinely hard quantified conditions) andvacuous(unreliable ones) in #20470.