File tree Expand file tree Collapse file tree 2 files changed +52
-0
lines changed
regression/cbmc/integral-trace Expand file tree Collapse file tree 2 files changed +52
-0
lines changed Original file line number Diff line number Diff line change
1
+ #include <assert.h>
2
+ #include <inttypes.h>
3
+ #include <math.h>
4
+ #include <stdbool.h>
5
+ #include <stddef.h>
6
+ #include <stdlib.h>
7
+
8
+ int main ()
9
+ {
10
+ int8_t i1 = 2 ;
11
+ int16_t i2 = 3 ;
12
+ int32_t i3 = 4 ;
13
+ int64_t i4 = 5 ;
14
+
15
+ int8_t in1 = -2 ;
16
+ int16_t in2 = -3 ;
17
+ int32_t in3 = -4 ;
18
+ int64_t in4 = -5 ;
19
+
20
+ uint8_t u8 = 'a' ;
21
+ uint16_t u16 = 8 ;
22
+ uint32_t u32 = 16 ;
23
+ uint64_t u64 = 32 ;
24
+
25
+ void * ptr = malloc (1 );
26
+
27
+ assert (false);
28
+
29
+ return 0 ;
30
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ test.c
3
+ --trace --xml-ui
4
+ activate-multi-line-match
5
+ ^EXIT=10$
6
+ ^SIGNAL=0$
7
+ VERIFICATION FAILED
8
+ <full_lhs>u8</full_lhs>\n\s*<full_lhs_value binary="01100001">97</full_lhs_value>
9
+ <full_lhs>u16</full_lhs>\n\s*<full_lhs_value binary="0{12}1000">8</full_lhs_value>
10
+ <full_lhs>u32</full_lhs>\n\s*<full_lhs_value binary="0{16}0{11}10000">16u</full_lhs_value>
11
+ <full_lhs>u64</full_lhs>\n\s*<full_lhs_value binary="0{32}0{16}0{10}100000">32ul</full_lhs_value>
12
+ <full_lhs>i1</full_lhs>\n\s*<full_lhs_value binary="0{6}10">2</full_lhs_value>
13
+ <full_lhs>i2</full_lhs>\n\s*<full_lhs_value binary="0{14}11">3</full_lhs_value>
14
+ <full_lhs>i3</full_lhs>\n\s*<full_lhs_value binary="0{29}100">4</full_lhs_value>
15
+ <full_lhs>i4</full_lhs>\n\s*<full_lhs_value binary="0{61}101">5l</full_lhs_value>
16
+ <full_lhs>in1</full_lhs>\n\s*<full_lhs_value binary="1{6}10">-2</full_lhs_value>
17
+ <full_lhs>in2</full_lhs>\n\s*<full_lhs_value binary="1{14}01">-3</full_lhs_value>
18
+ <full_lhs>in3</full_lhs>\n\s*<full_lhs_value binary="1{29}100">-4</full_lhs_value>
19
+ <full_lhs>in4</full_lhs>\n\s*<full_lhs_value binary="1{61}011">-5l</full_lhs_value>
20
+ --
21
+ --
22
+ Checks that the binary value is printed for integral types.
You can’t perform that action at this time.
0 commit comments