Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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

  • Subject: [Frama-c-discuss] Problem with werify mod 256 and cast to uint8 equivalence for uint64_t
  • From: sztfg at yandex.ru (sztfg at yandex.ru)
  • Date: Mon, 21 Mar 2016 04:57:53 +0300
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