From 899dacecca18382ab8ee5c02faf7bfb21a9e85d3 Mon Sep 17 00:00:00 2001
From: Martin Brain <martin.brain@city.ac.uk>
Date: Wed, 2 Aug 2023 16:13:24 +0100
Subject: [PATCH] Add Duff's device

---
 regression/cbmc/loop-duffs-device/main.c    | 44 +++++++++++++++++++++
 regression/cbmc/loop-duffs-device/test.desc | 12 ++++++
 2 files changed, 56 insertions(+)
 create mode 100644 regression/cbmc/loop-duffs-device/main.c
 create mode 100644 regression/cbmc/loop-duffs-device/test.desc

diff --git a/regression/cbmc/loop-duffs-device/main.c b/regression/cbmc/loop-duffs-device/main.c
new file mode 100644
index 00000000000..0dfb48b6743
--- /dev/null
+++ b/regression/cbmc/loop-duffs-device/main.c
@@ -0,0 +1,44 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdio.h>
+
+#define ARRAYMAX 256
+
+uint8_t *strndfy (uint8_t *dest, const uint8_t *src, size_t n) {
+  int i = 0;
+  int j = 0;
+  
+  switch (n & 0x3) {
+    do {
+      case 0 :   dest[i++] = src[j++];
+      case 1 :   dest[i++] = src[j++];
+      case 2 :   dest[i++] = src[j++];
+      case 3 :   dest[i++] = src[j++];
+    } while (j < n);
+  }
+  
+  return dest;
+}
+
+
+int main (int argc, char **argv) {
+  uint8_t src[ARRAYMAX];
+  uint8_t dest[ARRAYMAX];
+  
+  int length = 0;  
+  scanf("%u", &length);
+
+  if (length <= ARRAYMAX) {
+    for (int i = 0; i < length; ++i) {
+      src[i] = (uint8_t)i;
+    }
+
+    strndfy(dest, src, length);
+    
+    for (int i = 0; i < length; ++i) {
+      assert(dest[i] == (uint8_t)i);
+    }
+  }
+  
+  return 0;
+}
diff --git a/regression/cbmc/loop-duffs-device/test.desc b/regression/cbmc/loop-duffs-device/test.desc
new file mode 100644
index 00000000000..0789e50e488
--- /dev/null
+++ b/regression/cbmc/loop-duffs-device/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--unwind 257
+^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 checks whether Duff's device is handled correctly.