jepler/ProvenDelights
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Fix unintended signed shifts

Browse source
This commit is contained in:
Jeff Epler 2020-06-12 15:23:34 -05:00
parent e26ee5b061
commit 4fd49cd511
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
proofs/secded.txt
View file

@ -83,7 +83,7 @@ inline int correct(unsigned pr, unsigned *ur) {
// One error, and syn bits 5:0 tell where it is in ur.
b = syn - 31 - (syn >> 5); // Map syn to range 0 to 31.
*ur = *ur ^ (1 << b); // Correct the bit.
*ur = *ur ^ (1u << b); // Correct the bit.
return 1;
}

2
proofs/turn_off_rightmost_one.txt
View file

@ -13,6 +13,6 @@ int main() {
unsigned x = nondet_unsigned() | 1;
unsigned y = nondet_unsigned() & 31;
unsigned z = x << y;
assert(turn_off_rightmost_one(z) == (z ^ (1<<y)));
assert(turn_off_rightmost_one(z) == (z ^ (1u<<y)));
}
----