ten.cc

#define ROLL_R(x, n) ({ typeof(x) tmp = x; (tmp >> n) | (tmp << (32-n)); })

unsigned bcd_next(unsigned n) {
    n = n + 1;
   
    for(unsigned i=0; i<5; i++) {
        if ((n & 0xf) == 0xa) {
            n += 0x6;
        }
        n = ROLL_R(n, 4);
    }

    return n >> 12;
}

#if CPROVER
int nondet_int16();
int decimal_to_bcd(int x) {
    int scale = 1;
    int result = 0;
    for(int i = 0; i<5; i++) {
        result += scale * (x % 10);
        x /= 10;
        scale *= 16;
    }
    return result;
}
int main() {
    unsigned x = nondet_int16();
    __CPROVER_assume(x < 100000);
    int di = decimal_to_bcd(x), dj = decimal_to_bcd((x + 1) % 100000);
    __CPROVER_assert(dj == bcd_next(di), "bcd_next");
}
#elif MAIN
#include <stdio.h>
#define ARRAY_ELEM(x) (sizeof(x) / sizeof(x[0]))
int test_cases[] = {0x1, 0x9, 0x10, 0x11, 0x19, 0x99, 0x100, 0x199, 0x999, 0x9999, 0x99998, 0x99999 };

int main() {
    for(size_t j=0; j<ARRAY_ELEM(test_cases); j++) {
        int i = test_cases[j];
        printf("%05x -> %05x\n", i, bcd_next(i));
    }
}
#endif