Goose  Artifact [3a10c9b691]

Artifact 3a10c9b691c83bfe59c17edc79d0034be8c3fbd6be3aa6d8bc50424bf6fe7165:

• File tests/g0/verification/c-fail-test-1.g0 — part of check-in [45f663093d] at 2021-09-12 13:42:15 on branch trunk — Adopted a new convention for source extensions: .g0 for prelude code (where most language features won't be available), .g1 for user code (user: achavasse size: 277)
• File tests/noprelude/diagnostics/compile-verif-test-1.g — part of check-in [717a1ea6d4] at 2019-10-07 21:58:32 on branch trunk —
  • Fixed incorrect logic when generating z3 expressions to track the value of variables accross basic blocks.
  • Implemented basic error reporting for verification failure that highlights all the failed assertions.
  • Added a test program that demonstrates a simple case of failed static verification.
  (user: achavasse size: 277)
• File tests/noprelude/verification/c-fail-test-1.g — part of check-in [5e757567a6] at 2021-03-01 12:32:32 on branch trunk — Reorganized tests, they are now grouped by language feature. (user: achavasse size: 277)

void testfunc( sint(32) a, sint(32) b ) //requires [ a != b ]
{
    var ta, var tb = a,b

    if ta < tb
        ta,tb = tb,ta

    // This will fail to compile because a can be equal to b
    // (due to the commented out requirement)
    assert( ta > tb )
}

testfunc( 2, 1 )