diff --git a/intTests/test_llvm_tuple/Makefile b/intTests/test_llvm_tuple/Makefile new file mode 100644 index 0000000000..977e89a70a --- /dev/null +++ b/intTests/test_llvm_tuple/Makefile @@ -0,0 +1,2 @@ +test.bc : test.c + clang -c -emit-llvm -g -o test.bc test.c diff --git a/intTests/test_llvm_tuple/test.bc b/intTests/test_llvm_tuple/test.bc new file mode 100644 index 0000000000..99f0731f11 Binary files /dev/null and b/intTests/test_llvm_tuple/test.bc differ diff --git a/intTests/test_llvm_tuple/test.c b/intTests/test_llvm_tuple/test.c new file mode 100644 index 0000000000..ba748f1404 --- /dev/null +++ b/intTests/test_llvm_tuple/test.c @@ -0,0 +1,21 @@ +#include + +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; +} diff --git a/intTests/test_llvm_tuple/test.saw b/intTests/test_llvm_tuple/test.saw new file mode 100644 index 0000000000..69d616b384 --- /dev/null +++ b/intTests/test_llvm_tuple/test.saw @@ -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; diff --git a/intTests/test_llvm_tuple/test.sh b/intTests/test_llvm_tuple/test.sh new file mode 100644 index 0000000000..0b864017cd --- /dev/null +++ b/intTests/test_llvm_tuple/test.sh @@ -0,0 +1 @@ +$SAW test.saw