Merge pull request #1695 from GaloisInc/T1691

Fix #1691 by bringing in GaloisInc/crucible#1004
GaloisInc · Jun 24, 2022 · 4666760 · 4666760
2 parents f6c58db + 26f2478
commit 4666760
Show file tree

Hide file tree

Showing 8 changed files with 42 additions and 3 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/llvm-pretty b/deps/llvm-pretty
diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser
diff --git a/intTests/test1691/Makefile b/intTests/test1691/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/test1691/test.bc b/intTests/test1691/test.bc
diff --git a/intTests/test1691/test.c b/intTests/test1691/test.c
@@ -0,0 +1,8 @@
+struct s {
+  unsigned x:1;
+  unsigned y:1;
+};
+
+int f(const struct s *ss) {
+  return ss->x == ss->y;
+}
diff --git a/intTests/test1691/test.saw b/intTests/test1691/test.saw
@@ -0,0 +1,17 @@
+enable_experimental;
+enable_lax_loads_and_stores;
+
+let f_spec = do {
+  ss <- llvm_alloc_readonly (llvm_alias "struct.s");
+  x <- llvm_fresh_var "x" (llvm_int 1);
+  y <- llvm_fresh_var "y" (llvm_int 1);
+  llvm_points_to_bitfield ss "x" (llvm_term x);
+  llvm_points_to_bitfield ss "y" (llvm_term y);
+
+  llvm_execute_func [ss];
+
+  llvm_return (llvm_term {{ if x == y then 1 else 0 : [32] }});
+};
+
+m <- llvm_load_module "test.bc";
+ov <- llvm_verify m "f" [] false f_spec (w4_unint_yices []);
diff --git a/intTests/test1691/test.sh b/intTests/test1691/test.sh
@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw