1 files changed, 39 insertions, 0 deletions
diff --git a/test/Feature/RaiseAsm.c b/test/Feature/RaiseAsm.c
new file mode 100644
index 00000000..5b8acab4
--- /dev/null
+++ b/test/Feature/RaiseAsm.c
@@ -0,0 +1,39 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --exit-on-error %t1.bc
+
+#include <assert.h>
+
+typedef unsigned short uint16;
+typedef unsigned int   uint32;
+
+uint16 byteswap_uint16(uint16 x) {
+  return (x << 8) | (x >> 8);
+}
+uint32 byteswap_uint32(uint32 x) {
+  return ((byteswap_uint16(x) << 16) |
+          (byteswap_uint16(x >> 16)));
+}
+
+uint16 byteswap_uint16_asm(uint16 x) {
+  uint16 res;
+  __asm__("rorw $8, %w0" : "=r" (res) : "0" (x) : "cc");
+  return res;
+}
+
+uint32 byteswap_uint32_asm(uint32 x) {
+  uint32 res;
+  __asm__("rorw $8, %w0;"
+          "rorl $16, %0;"
+          "rorw $8, %w0" : "=r" (res) : "0" (x) : "cc");
+  return res;
+}
+
+int main() {
+  uint16 ui16 = klee_int("ui16");
+  uint32 ui32 = klee_int("ui32");
+
+  assert(ui16 == byteswap_uint16(byteswap_uint16_asm(ui16)));
+  assert(ui32 == byteswap_uint32(byteswap_uint32_asm(ui32)));
+
+  return 0;
+}