[ivy1.7, ivy1.8] no warning about divergent while-loop

[plredmond]

Summary

If you use a while loop with a condition that doesn't lead to termination, IVy doesn't provide any warning. Instead, you can assert false; after the while loop.

Steps to reproduce

Put the following in a file oops.ivy.

#lang ivy1.8

action foo = {
    while true { }
    assert false;
}

export foo

Check the file with the following command.

$ ivy_check trace=true oops.ivy

• Expected: Line 4 should cause IVy to issue a warning about a non-terminating loop.
• Actual: Whole file passes.

This is an issue because you might have a complex loop condition, invariants, body, and subsequent statements, and never realize that your loop doesn't terminate.

Present in versions

On kenmcmil/ivy@dbe45e7 on macOS Sonoma.

---

Found while working together with @nano-o.