We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
--trace
1 parent 343cf7e commit 8d8dfa9Copy full SHA for 8d8dfa9
regression/cbmc-incr-smt2/unions/padded.c
@@ -0,0 +1,14 @@
1
+#include <assert.h>
2
+#include <stdint.h>
3
+
4
+union my_uniont
5
+{
6
+ uint16_t a;
7
+ uint8_t b;
8
+};
9
10
+int main()
11
12
+ union my_uniont my_union = {.b = 5};
13
+ assert(my_union.a == 5);
14
+}
regression/cbmc-incr-smt2/unions/padded.desc
@@ -0,0 +1,12 @@
+CORE
+padded.c
+--trace
+Passing problem to incremental SMT2 solving
+\[main\.assertion\.1\] line 13 assertion my_union\.a \=\= 5\: FAILURE
+my_union\=\{ \.a\=\d+ \} \(\d{8} 00000101\)
+^EXIT=10$
+^SIGNAL=0$
+--
+Test that we support union values and traces for a example where the trace
+should include non deterministic padding.
0 commit comments