atf_check_sbttons
atf_check_sbttons(0, 0);
atf_check_sbttons(0, 1);
atf_check_sbttons(1, (1ll << 32) / 1000000000);
atf_check_sbttons(1000000000, 1ll << 32);
atf_check_sbttons(1999999999, (1ll << 33) - 1);
atf_check_sbttons(1999999999, (1ll << 33) - 1);
atf_check_sbttons(2000000000, 1ll << 33);
atf_check_sbttons(3999999999, (1ll << 34) - 1);
atf_check_sbttons(4000000000, 1ll << 34);
atf_check_sbttons(999999999, (1ll << 32) - 1);
atf_check_sbttons((1ll << 31) * 1000000000, (1ull << 63) - 1);