Skip to content

Commit d63f36a

Browse files
committed
Fix #1684 by bringing in GaloisInc/crucible#998
Now that the `crucible-llvm` memory model can reason about struct padding with `lax-loads-and-stores` enabled, bumping the `crucible` submodule to bring in that change fixes #1684 as a consequence. I have also added a regression test.
1 parent 8edd9cf commit d63f36a

File tree

7 files changed

+41
-2
lines changed

7 files changed

+41
-2
lines changed

intTests/test1684/Makefile

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CC = clang
2+
CFLAGS = -g -emit-llvm -frecord-command-line -O0
3+
4+
all: test.bc
5+
6+
test.bc: test.c
7+
$(CC) $(CFLAGS) -c $< -o $@
8+
9+
.PHONY: clean
10+
clean:
11+
rm -f test.bc

intTests/test1684/test.bc

2.89 KB
Binary file not shown.

intTests/test1684/test.c

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <stdint.h>
2+
3+
struct a {
4+
uint16_t x;
5+
uint32_t y;
6+
};
7+
8+
struct b {
9+
struct a aa;
10+
};
11+
12+
void f(struct b *bb) {}

intTests/test1684/test.saw

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
enable_experimental;
2+
enable_lax_loads_and_stores;
3+
4+
let f_spec = do {
5+
aa <- llvm_fresh_var "aa" (llvm_alias "struct.a");
6+
bb <- llvm_alloc (llvm_alias "struct.b");
7+
llvm_points_to (llvm_field bb "aa") (llvm_term aa);
8+
9+
llvm_execute_func [bb];
10+
};
11+
12+
m <- llvm_load_module "test.bc";
13+
llvm_verify m "f" [] false f_spec (w4_unint_yices []);

intTests/test1684/test.sh

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
set -e
2+
3+
$SAW test.saw

0 commit comments

Comments
 (0)