Smoke detector triggered even without absurd
unreachable code in WhyML should be marked as absurd
and it is known that the VC generated is special in the sense that the smoke detector brings a false alarm (issues #376 and #297).
Yet, the following code exhibit a similar behavior
use int.Int
let f () =
[@vc:divergent]
let ref x = 0 in
while true do
x <- x + 1;
if x = 10 then break;
done;
assert { x = 10 }
There are two VCs after split, the second being after loop exit, which is indeed impossible. As normal loop exit, one may think that absurd
should be added after done
. But this would be wrong as the break
while then jump to absurd
which is not want we want.
Would it be desirable in the VC gen to make a special case for while true do ... done
to disable any VC generation after the normal loop exit ?