Skip to content

Commit 88b0dfc

Browse files
hotfix regression tests
1 parent ccb13c1 commit 88b0dfc

File tree

5 files changed

+6
-8
lines changed

5 files changed

+6
-8
lines changed
File renamed without changes.

tests/regression/82-bitfield/08-refine-with-bitfield.c

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,6 @@ int main() {
4343
// Testing OR operations with patterns
4444
int OR_MASK = 0x55; // 01010101 in binary
4545
if ((a | OR_MASK) == 0x55) {
46-
__goblint_assert(a == 0); // Only possible if a is 0
4746
__goblint_assert((a | 0xFF) == 0xFF); // ORing with all 1s gives all 1s
4847
}
4948

@@ -74,7 +73,7 @@ int main() {
7473
if ((a & SHIFT_MASK) == SHIFT_MASK) {
7574
__goblint_assert((a & 12) == 12); // Both bits must be set
7675
__goblint_assert(((a >> 2) & 3) == 3); // When shifted right, lowest bits must be 11
77-
__goblint_assert(((a << 2) & 12) == 12); // When shifted left, highest bits must be 1100
76+
__goblint_assert(((a << 2) & 48) == 48); // When shifted left, highest bits must be 11
7877
}
7978

8079
int SHIFTED = 0x7 << 3; // 111000 in binary
@@ -89,10 +88,9 @@ int main() {
8988
}
9089

9190
// Testing bitwise complement
92-
int COMP_MASK = ~0xF0; // Complement of 11110000
91+
int COMP_MASK = ~0x0F;
9392
if ((a & COMP_MASK) == 0x0F) {
94-
__goblint_assert((a & 0xF0) == 0); // Upper 4 bits must be 0
95-
__goblint_assert((a & 0x0F) == 0x0F); // Lower 4 bits must be all 1s
93+
__goblint_check(0); // NOWARN (unreachable)
9694
}
9795

9896
return 0;

tests/regression/82-bitfield/09-refine-interval.c renamed to tests/regression/82-bitfield/09-refine-intervalA.c

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,10 @@ int main() {
1111

1212
if ((a & inv_mask) == 0) {
1313
__goblint_check(a <= 14); // SUCCESS
14-
__goblint_check(a >= 1); // SUCCESS
14+
__goblint_check(a >= 0); // SUCCESS
1515

16-
if (1 <= a && a <= 14) {
17-
printf("a is in the interval [1, 14]\n");
16+
if (0 <= a && a <= 14) {
17+
printf("a is in the interval [0, 14]\n");
1818
} else {
1919
__goblint_check(0); // NOWARN (unreachable)
2020
}
File renamed without changes.
File renamed without changes.

0 commit comments

Comments
 (0)