Skip to content

Commit 3c86db2

Browse files
committed
Extend test to cover negative integrals
In order to confirm that there is no negative number related bug.
1 parent 2ba6c07 commit 3c86db2

File tree

2 files changed

+9
-0
lines changed

2 files changed

+9
-0
lines changed

regression/cbmc/integral-trace/test.c

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,11 @@ int main()
1212
int32_t i3 = 4;
1313
int64_t i4 = 5;
1414

15+
int8_t in1 = -2;
16+
int16_t in2 = -3;
17+
int32_t in3 = -4;
18+
int64_t in4 = -5;
19+
1520
uint8_t u8 = 'a';
1621
uint16_t u16 = 8;
1722
uint32_t u32 = 16;

regression/cbmc/integral-trace/test.desc

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,10 @@ VERIFICATION FAILED
1313
<full_lhs>i2</full_lhs>\n\s*<full_lhs_value binary="0{14}11">3</full_lhs_value>
1414
<full_lhs>i3</full_lhs>\n\s*<full_lhs_value binary="0{29}100">4</full_lhs_value>
1515
<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>
1620
--
1721
--
1822
Checks that the binary value is printed for integral types.

0 commit comments

Comments
 (0)