Skip to content

Commit

Permalink
hotfix regression tests
Browse files Browse the repository at this point in the history
  • Loading branch information
ManuelLerchner committed Dec 10, 2024
1 parent ccb13c1 commit 88b0dfc
Show file tree
Hide file tree
Showing 5 changed files with 6 additions and 8 deletions.
8 changes: 3 additions & 5 deletions tests/regression/82-bitfield/08-refine-with-bitfield.c
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,6 @@ int main() {
// Testing OR operations with patterns
int OR_MASK = 0x55; // 01010101 in binary
if ((a | OR_MASK) == 0x55) {
__goblint_assert(a == 0); // Only possible if a is 0
__goblint_assert((a | 0xFF) == 0xFF); // ORing with all 1s gives all 1s
}

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

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

// Testing bitwise complement
int COMP_MASK = ~0xF0; // Complement of 11110000
int COMP_MASK = ~0x0F;
if ((a & COMP_MASK) == 0x0F) {
__goblint_assert((a & 0xF0) == 0); // Upper 4 bits must be 0
__goblint_assert((a & 0x0F) == 0x0F); // Lower 4 bits must be all 1s
__goblint_check(0); // NOWARN (unreachable)
}

return 0;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,10 @@ int main() {

if ((a & inv_mask) == 0) {
__goblint_check(a <= 14); // SUCCESS
__goblint_check(a >= 1); // SUCCESS
__goblint_check(a >= 0); // SUCCESS

if (1 <= a && a <= 14) {
printf("a is in the interval [1, 14]\n");
if (0 <= a && a <= 14) {
printf("a is in the interval [0, 14]\n");
} else {
__goblint_check(0); // NOWARN (unreachable)
}
Expand Down

0 comments on commit 88b0dfc

Please sign in to comment.