Skip to content

Commit 8c154e2

Browse files
committed
The SMT back-end does not currently support bitvector -> union/struct conversion
Most of those shouldn't even be happening as more support needs to be implemented in byte_extract_lowering. Will be taken care of in follow-up commits.
1 parent a3d77e6 commit 8c154e2

File tree

9 files changed

+9
-9
lines changed

9 files changed

+9
-9
lines changed

regression/cbmc/Pointer_byte_extract3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.c
33

44
^EXIT=0$

regression/cbmc/Pointer_byte_extract7/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.c
33
--big-endian
44
^EXIT=0$

regression/cbmc/equality_through_union1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.c
33

44
^EXIT=0$

regression/cbmc/equality_through_union2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.c
33

44
^EXIT=0$

regression/cbmc/equality_through_union3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.c
33

44
^EXIT=0$

regression/cbmc/gcc_vector1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.c
33

44
^EXIT=0$

regression/cbmc/trace_address_arithmetic1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.c
33
--trace
44
^EXIT=10$

regression/cbmc/union11/union_list.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE broken-smt-backend
22
union_list.c
33

44
^EXIT=0$

regression/cbmc/union8/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.c
33

44
^EXIT=0$

0 commit comments

Comments
 (0)