--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on March 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with werify mod 256 and cast to uint8 equivalence for uint64_t



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