WIP

regression/cbmc/loop-busy-wait/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+volatile char zero_to_unlock;
+
+void busy_wait (void) {
+  while (zero_to_unlock);
+  return;
+}
+
+int main (int argc, char **argv) {
+  // Obviously we would need to spawn some other threads here...
+
+  zero_to_unlock = 1;
+  busy_wait();
+
+  assert(0);
+
+  return 0;
+}

regression/cbmc/loop-busy-wait/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] line \d+ assertion 0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Relies on symex converting empty loops into assumptions

regression/cbmc/loop-empty/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+void empty_loop (void) {
+ loop : goto loop;
+  return;
+}
+
+int main (int argc, char **argv) {
+  empty_loop();
+
+  assert(0);
+
+  return 0;
+}

regression/cbmc/loop-empty/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] line \d+ assertion 0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Relies on symex converting empty loops into assumptions

regression/cbmc/loop-sequence-of-instructions/main.c

@@ -0,0 +1,70 @@
+#include <assert.h>
+#include <stdio.h>
+
+unsigned int control = 0;
+unsigned int history = 0;
+
+unsigned int choose (void) {
+  unsigned int lsb = control & 0x1u;
+  control = control >> 1;
+  history = (history << 1) | lsb;
+  return lsb;
+}
+
+void red (void) {
+  printf("Red\n");
+}
+void blue (void) {
+  printf("Blue\n");
+}
+
+void test (void) {
+  while (choose()) {
+    if (choose()) {
+      red();  // Is this in the loop?
+      break;
+
+    } else if (choose()) {
+      goto out;
+    }
+  }
+
+  if (0) {
+  out: blue();  // What about this?
+  }
+
+  return;
+}
+
+
+int main (int argc, char **argv) {
+  scanf("%u", &control);
+
+  test();
+
+  printf("%u\n", history);
+  // History is (100)*(0|11|101)
+
+  // Let's check that
+  if (history == 0u) {
+    // Fine
+  } else {
+    if ((history & 0x7) == 0x5) {
+      history = history >> 3;
+    } else if ((history & 0x3) == 0x3) {
+      history = history >> 2;
+    } else if ((history & 0x1) == 0x0) {
+      history = history >> 1;
+    } else {
+      assert(0);
+    }
+
+    while ((history & 0x7) == 0x4) {
+      history = history >> 3;
+    }
+
+    assert(history == 0);
+  }
+
+  return 0;
+}

regression/cbmc/loop-sequence-of-instructions/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--unwind 22
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ assertion 0: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion history == 0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This investigates whether red or blue is in the loop.