diff --git a/deps/crucible b/deps/crucible index 9946c88689..95677b97a0 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 9946c8868959350152a1b1c2fda4424e2b2a5a80 +Subproject commit 95677b97a0fc37a45733f900da162f1d917bc4c9 diff --git a/deps/macaw b/deps/macaw index 6a4f406c68..2791b1050f 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit 6a4f406c680dc0438799ef5c95c94311e07e722a +Subproject commit 2791b1050f348922a27192d8a73ee538fed57629 diff --git a/intTests/test1684/Makefile b/intTests/test1684/Makefile new file mode 100644 index 0000000000..f7abdbe50b --- /dev/null +++ b/intTests/test1684/Makefile @@ -0,0 +1,11 @@ +CC = clang +CFLAGS = -g -emit-llvm -frecord-command-line -O0 + +all: test.bc + +test.bc: test.c + $(CC) $(CFLAGS) -c $< -o $@ + +.PHONY: clean +clean: + rm -f test.bc diff --git a/intTests/test1684/test.bc b/intTests/test1684/test.bc new file mode 100644 index 0000000000..7ba1a7072b Binary files /dev/null and b/intTests/test1684/test.bc differ diff --git a/intTests/test1684/test.c b/intTests/test1684/test.c new file mode 100644 index 0000000000..178b8d1682 --- /dev/null +++ b/intTests/test1684/test.c @@ -0,0 +1,12 @@ +#include + +struct a { + uint16_t x; + uint32_t y; +}; + +struct b { + struct a aa; +}; + +void f(struct b *bb) {} diff --git a/intTests/test1684/test.saw b/intTests/test1684/test.saw new file mode 100644 index 0000000000..c0fb026915 --- /dev/null +++ b/intTests/test1684/test.saw @@ -0,0 +1,13 @@ +enable_experimental; +enable_lax_loads_and_stores; + +let f_spec = do { + aa <- llvm_fresh_var "aa" (llvm_alias "struct.a"); + bb <- llvm_alloc (llvm_alias "struct.b"); + llvm_points_to (llvm_field bb "aa") (llvm_term aa); + + llvm_execute_func [bb]; +}; + +m <- llvm_load_module "test.bc"; +llvm_verify m "f" [] false f_spec (w4_unint_yices []); diff --git a/intTests/test1684/test.sh b/intTests/test1684/test.sh new file mode 100644 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test1684/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw