adds more testcases to showcase the behavior of branching or looping on a SIF expression

Author: ArquintL

src/test/resources/sif/sif_branch_condition.vpr

@@ -0,0 +1,39 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// this testcase demonstrates how branching on a SIF expression behaves semantically
+
+requires lowEvent
+method InLowEventContexts(t: Int)
+{
+    if (low(t)) {
+        assert low(t)
+    } else {
+        // this case is reachable as `t` might be the same in both executions or it might not
+        //:: ExpectedOutput(assert.failed:assertion.false)
+        assert false
+    }
+}
+
+requires lowEvent
+method InLowEventContexts2(t: Int)
+{
+    // since `low(t)` evaluates to the same value in both executions, both executions are guaranteed
+    // to enter the same branch
+    if (low(t)) {
+        assert lowEvent
+    } else {
+        assert lowEvent
+    }
+}
+
+requires !lowEvent
+method InNonLowEventContexts(t: Int)
+{
+    if (low(t)) {
+        assert low(t)
+    } else {
+        // this is a dead branch as `low(t)` trivially evaluates to `true` as there is no second execution
+        assert false
+    }
+}

src/test/resources/sif/sif_loop_condition.vpr

@@ -0,0 +1,44 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// this testcase demonstrates how looping on a SIF expression behaves semantically
+
+requires lowEvent
+method InLowEventContexts(t: Int)
+{
+    while (low(t))
+    {
+        assert low(t)
+    }
+
+    // this case is reachable as `t` might be the same in both executions or it might not
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+requires lowEvent
+method InLowEventContexts2(t: Int)
+{
+    // since `low(t)` evaluates to the same value in both executions, both executions are guaranteed
+    // to execute the loop bodies in sync
+
+    while (low(t))
+    invariant lowEvent
+    {
+        assert lowEvent
+    }
+
+    assert lowEvent
+}
+
+requires !lowEvent
+method InNonLowEventContexts(t: Int)
+{
+    while (low(t))
+    {
+        assert low(t)
+    }
+
+    // the loop will never terminate as `low(t)` trivially evaluates to `true` as there is no second execution
+    assert false
+}