/* TAGS: c sym big */ /* VERIFY_OPTS: --symbolic --sequential -o nofail:malloc -o ignore:integer */ extern void __VERIFIER_assume(int); extern void __VERIFIER_error() __attribute__ ((__noreturn__)); extern unsigned int __VERIFIER_nondet_uint(void); void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); /* ERROR */ } return; } /* https://graphics.stanford.edu/~seander/bithacks.html#ModulusDivisionEasy */ int main() { /* Compute modulus division by (1 << s) - 1 without a division operator */ unsigned int n = __VERIFIER_nondet_uint(); /* numerator */ unsigned int s = __VERIFIER_nondet_uint(); /* s > 0 */ unsigned int d; unsigned int m; /* n % d goes here. */ __VERIFIER_assume(s < 32); d = (1 << s) - 1; /* so d is either 1, 3, 7, 15, 31, ...) */ if (d > 0) { m = n; while (n > d) { m = 0; while (n > 0) { m += n & d; n = n >> s; } n = m; } /* Now m is a value from 0 to d, but since with modulus division * we want m to be 0 when it is d. */ if (m == d) { m = 0; } __VERIFIER_assert(m == n % d); } return 0; }