Add integration test for using llvm_points_to with Cryptol tuples.

Fixes #159.

Author: Brian Huffman

intTests/test_llvm_tuple/Makefile

@@ -0,0 +1,2 @@
+test.bc : test.c
+	clang -c -emit-llvm -g -o test.bc test.c

intTests/test_llvm_tuple/test.bc

@@ -0,0 +1,21 @@
+#include <stdint.h>
+
+struct triple {
+    uint8_t first[4];
+    uint16_t second;
+    uint16_t third;
+};
+
+void swap (struct triple *p) {
+    uint8_t temp1;
+    uint16_t temp2;
+    temp1 = p->first[0];
+    p->first[0] = p->first[3];
+    p->first[3] = temp1;
+    temp1 = p->first[1];
+    p->first[1] = p->first[2];
+    p->first[2] = temp1;
+    temp2 = p->second;
+    p->second = p->third;
+    p->third = temp2;
+}

intTests/test_llvm_tuple/test.c

@@ -0,0 +1,25 @@
+// This is a test demonstrating the use of `llvm_points_to` with a
+// struct pointer and a single Cryptol term of tuple type.
+// https://github.com/GaloisInc/saw-script/issues/159
+
+bc <- llvm_load_module "test.bc";
+
+let i8 = llvm_int 8;
+let i16 = llvm_int 16;
+
+let {{
+  swap_spec : ([4][8], [16], [16]) -> ([4][8], [16], [16])
+  swap_spec (xs, y, z) = (reverse xs, z, y)
+}};
+
+swap_ov <-
+  llvm_verify bc "swap" [] false
+    do {
+      let t = llvm_struct "struct.triple";
+      p <- llvm_alloc t;
+      x <- llvm_fresh_var "x" t;
+      llvm_points_to p (llvm_term x);
+      llvm_execute_func [p];
+      llvm_points_to p (llvm_term {{ swap_spec x }});
+    }
+    z3;

intTests/test_llvm_tuple/test.saw

@@ -0,0 +1 @@
+$SAW test.saw