--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on March 2016 ---
I was trying to prove this code using alt-ergo: /* ALWAYS TRUE */ /*@ ensures \result == 1; */ uint8_t test_uint8_cast_mod256_eq (uint64_t a) { return ((a)%256 == (uint8_t)(a)); } how it looks like: goal test_uint8_cast_mod256_eq_post: forall i : int. is_uint64(i) -> (to_uint8(i) = (safe_comp_mod(i, 256))) but it failed. Maybe need to add some axioms related safe_comp_mod? Adding new axioms to .mlw file: axiom A_1 : forall i : int. (0 <= i) -> (to_uint8(i) = (safe_comp_mod(i, 256))) axiom A_2 : forall i : int. (0 <= i) -> (to_uint16(i) = (safe_comp_mod(i, 65536))) axiom A_3 : forall i : int. (0 <= i) -> (to_uint32(i) = (safe_comp_mod(i, 4294967296))) axiom A_4 : forall i : int. (0 <= i) -> (to_uint64(i) = (safe_comp_mod(i, 18446744073709551616))) ... and after that I can prove it. But maybe I doing something wrong, and this thing can be proved without adding axioms? Or maybe need to add more general axiom? I tried this axiom: axiom A_GENERIC : forall i,j : int. ((0 <= i) and (i < j)) -> (i = (safe_comp_mod(i, j))) but it doesn't work