--- layout: fc_discuss_archives title: Message 9 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



Hi,

Axioms about safe_comp_mod are in the model. However, axioms that
give the behavior of to_uint8(i) when (0 <= i < 256) is not true are
probably missing.

I modified a little bit your C code (see below). I have one unproved VC,
for which I get safe_comp_mod(i,256) = 44 in the model.
An axiom like "A_1" would allow to conclude in this case.

For the generic axiom, a case 0 <= i and i >= j is missing ...

Regards,
Mohamed.

#include <stdio.h>

// Proved by Alt-Ergo //
/*@ requires (1 <= a <= 255);
      ensures \result == 1;
*/
int test_uint8_cast_mod256_eq (int a)
{ return ((a)%256 == (unsigned char)(a)); }

// Proved by Qed //
/*@ requires 300 <= a <= 300;
      ensures \result == 1;
*/
int test_uint8_cast_mod256_eq__v2 (int a)
{ return ((a)%256 == (unsigned char)(a)); }

// Not Proved //
/*@ requires 300 <= a <= 302;
     ensures \result == 1;
*/
int test_uint8_cast_mod256_eq__v3 (int a)
{ return ((a)%256 == (unsigned char)(a)); }

int main (){
   int b = 300;
   printf("mod      = %d\n", b%256);
   printf("unsigned = %d\n", (unsigned char) (b));
}


Le 21/03/2016 02:57, sztfg at yandex.ru a écrit :
> 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
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160321/b6981d60/attachment-0001.html>
-------------- section suivante --------------
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
(*                        énergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(* this is a prelude for Alt-Ergo integer arithmetic *)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
(*                        énergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
logic abs_int : int -> int

axiom abs_def : (forall x:int. ((0 <= x) -> (abs_int(x) = x)))

axiom abs_def1 : (forall x:int. ((not (0 <= x)) -> (abs_int(x) = (-x))))

axiom Abs_le :
  (forall x:int. forall y:int. ((abs_int(x) <= y) -> ((-y) <= x)))

axiom Abs_le1 : (forall x:int. forall y:int. ((abs_int(x) <= y) -> (x <= y)))

axiom Abs_le2 :
  (forall x:int. forall y:int. ((((-y) <= x) and (x <= y)) ->
  (abs_int(x) <= y)))

axiom Abs_pos : (forall x:int. (0 <= abs_int(x)))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
(*                        énergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
logic safe_comp_div: int, int -> int
axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y
logic safe_comp_mod: int, int -> int
axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory int_Abs_ must be appended to this file*)
axiom Div_bound :
  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
  (0 <= safe_comp_div(x,y))))

axiom Div_bound1 :
  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
  (safe_comp_div(x,y) <= x)))

axiom Div_1 : (forall x:int. (safe_comp_div(x,1) = x))

axiom Mod_1 : (forall x:int. (safe_comp_mod(x,1) = 0))

axiom Div_inf :
  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) ->
  (safe_comp_div(x,y) = 0)))

axiom Mod_inf :
  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) ->
  (safe_comp_mod(x,y) = x)))

axiom Div_mult :
  (forall x:int. forall y:int. forall z:int [safe_comp_div(((x * y) + z),x)].
  (((0 <  x) and ((0 <= y) and (0 <= z))) ->
  (safe_comp_div(((x * y) + z),x) = (y + safe_comp_div(z,x)))))

axiom Mod_mult :
  (forall x:int. forall y:int. forall z:int [safe_comp_mod(((x * y) + z),x)].
  (((0 <  x) and ((0 <= y) and (0 <= z))) ->
  (safe_comp_mod(((x * y) + z),x) = safe_comp_mod(z,x))))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
(*                        énergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(* this is a prelude for Alt-Ergo real arithmetic *)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
axiom add_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x + y) / z) = ((x / z) + (y / z)))))

axiom sub_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x - y) / z) = ((x / z) - (y / z)))))

axiom neg_div :
  (forall x:real. forall y:real. ((not (y = 0.0)) ->
  (((-x) / y) = (-(x / y)))))

axiom assoc_mul_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x * y) / z) = (x * (y / z)))))

axiom assoc_div_mul :
  (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
  (not (z = 0.0))) -> (((x / y) / z) = (x / (y * z)))))

axiom assoc_div_div :
  (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
  (not (z = 0.0))) -> ((x / (y / z)) = ((x * z) / y))))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
(*                        énergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
(*                        énergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
logic from_int : int -> real

axiom Zero : (from_int(0) = 0.0)

axiom One : (from_int(1) = 1.0)

axiom Add :
  (forall x:int. forall y:int.
  (from_int((x + y)) = (from_int(x) + from_int(y))))

axiom Sub :
  (forall x:int. forall y:int.
  (from_int((x - y)) = (from_int(x) - from_int(y))))

axiom Mul :
  (forall x:int. forall y:int.
  (from_int((x * y)) = (from_int(x) * from_int(y))))

axiom Neg : (forall x:int. (from_int((-x)) = (-from_int(x))))

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2015                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory bool_Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory int_Abs_ must be appended to this file*)
(** The theory int_ComputerDivision_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
(** The theory real_RealInfix_ must be appended to this file*)
(** The theory real_FromInt_ must be appended to this file*)
logic ite : bool, 'a, 'a -> 'a

axiom ite1 :
  (forall p:bool. forall x:'a. forall y:'a [ite(p, x, y)]. (((p = true) and
  (ite(p, x, y) = x)) or ((p = false) and (ite(p, x, y) = y))))

logic eqb : 'a, 'a -> bool

axiom eqb1 : (forall x:'a. forall y:'a. ((eqb(x, y) = true) -> (x = y)))

axiom eqb2 : (forall x:'a. forall y:'a. ((x = y) -> (eqb(x, y) = true)))

logic neqb : 'a, 'a -> bool

axiom neqb1 :
  (forall x:'a. forall y:'a. ((neqb(x, y) = true) -> (not (x = y))))

axiom neqb2 :
  (forall x:'a. forall y:'a. ((not (x = y)) -> (neqb(x, y) = true)))

logic zlt : int, int -> bool

logic zleq : int, int -> bool

axiom zlt1 : (forall x:int. forall y:int. ((zlt(x, y) = true) -> (x <  y)))

axiom zlt2 : (forall x:int. forall y:int. ((x <  y) -> (zlt(x, y) = true)))

axiom zleq1 : (forall x:int. forall y:int. ((zleq(x, y) = true) -> (x <= y)))

axiom zleq2 : (forall x:int. forall y:int. ((x <= y) -> (zleq(x, y) = true)))

logic rlt : real, real -> bool

logic rleq : real, real -> bool

axiom rlt1 : (forall x:real. forall y:real. ((rlt(x, y) = true) -> (x <  y)))

axiom rlt2 : (forall x:real. forall y:real. ((x <  y) -> (rlt(x, y) = true)))

axiom rleq1 :
  (forall x:real. forall y:real. ((rleq(x, y) = true) -> (x <= y)))

axiom rleq2 :
  (forall x:real. forall y:real. ((x <= y) -> (rleq(x, y) = true)))

logic truncate : real -> int

function real_of_int(x: int) : real = from_int(x)

axiom truncate_of_int : (forall x:int. (truncate(real_of_int(x)) = x))

axiom c_euclidian :
  (forall n:int. forall d:int [safe_comp_div(n,d), safe_comp_mod(n,d)].
  ((not (d = 0)) -> (n = ((safe_comp_div(n,d) * d) + safe_comp_mod(n,d)))))

axiom cdiv_cases :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_div(n,d) = (n / d)))))

axiom cdiv_cases1 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_div(n,d) = (-((-n) / d))))))

axiom cdiv_cases2 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_div(n,d) = (-(n / (-d)))))))

axiom cdiv_cases3 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_div(n,d) = ((-n) / (-d))))))

axiom cmod_cases :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_mod(n,d) = (n % d)))))

axiom cmod_cases1 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_mod(n,d) = (-((-n) % d))))))

axiom cmod_cases2 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_mod(n,d) = (n % (-d))))))

axiom cmod_cases3 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_mod(n,d) = (-((-n) % (-d)))))))

axiom cmod_remainder :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (0 <= safe_comp_mod(n,d)))))

axiom cmod_remainder1 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_mod(n,d) <  d))))

axiom cmod_remainder2 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  ((-d) <  safe_comp_mod(n,d)))))

axiom cmod_remainder3 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_mod(n,d) <= 0))))

axiom cmod_remainder4 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (0 <= safe_comp_mod(n,d)))))

axiom cmod_remainder5 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_mod(n,d) <  (-d)))))

axiom cmod_remainder6 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (d <  safe_comp_mod(n,d)))))

axiom cmod_remainder7 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_mod(n,d) <= 0))))

axiom cdiv_neutral :
  (forall a:int [safe_comp_div(a,1)]. (safe_comp_div(a,1) = a))

axiom cdiv_inv :
  (forall a:int [safe_comp_div(a,a)]. ((not (a = 0)) ->
  (safe_comp_div(a,a) = 1)))

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2015                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory bool_Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
logic is_uint8 : int -> prop

axiom is_uint8_def : (forall x:int [is_uint8(x)]. (is_uint8(x) -> (0 <= x)))

axiom is_uint8_def1 :
  (forall x:int [is_uint8(x)]. (is_uint8(x) -> (x <  256)))

axiom is_uint8_def2 :
  (forall x:int [is_uint8(x)]. (((0 <= x) and (x <  256)) -> is_uint8(x)))

logic is_sint8 : int -> prop

axiom is_sint8_def :
  (forall x:int [is_sint8(x)]. (is_sint8(x) -> ((-128) <= x)))

axiom is_sint8_def1 :
  (forall x:int [is_sint8(x)]. (is_sint8(x) -> (x <  128)))

axiom is_sint8_def2 :
  (forall x:int [is_sint8(x)]. ((((-128) <= x) and (x <  128)) ->
  is_sint8(x)))

logic is_uint16 : int -> prop

axiom is_uint16_def :
  (forall x:int [is_uint16(x)]. (is_uint16(x) -> (0 <= x)))

axiom is_uint16_def1 :
  (forall x:int [is_uint16(x)]. (is_uint16(x) -> (x <  65536)))

axiom is_uint16_def2 :
  (forall x:int [is_uint16(x)]. (((0 <= x) and (x <  65536)) ->
  is_uint16(x)))

predicate is_sint16(x: int) = (((-32768) <= x) and (x <  32768))

logic is_uint32 : int -> prop

axiom is_uint32_def :
  (forall x:int [is_uint32(x)]. (is_uint32(x) -> (0 <= x)))

axiom is_uint32_def1 :
  (forall x:int [is_uint32(x)]. (is_uint32(x) -> (x <  4294967296)))

axiom is_uint32_def2 :
  (forall x:int [is_uint32(x)]. (((0 <= x) and (x <  4294967296)) ->
  is_uint32(x)))

logic is_sint32 : int -> prop

axiom is_sint32_def :
  (forall x:int [is_sint32(x)]. (is_sint32(x) -> ((-2147483648) <= x)))

axiom is_sint32_def1 :
  (forall x:int [is_sint32(x)]. (is_sint32(x) -> (x <  2147483648)))

axiom is_sint32_def2 :
  (forall x:int [is_sint32(x)]. ((((-2147483648) <= x) and
  (x <  2147483648)) -> is_sint32(x)))

logic is_uint64 : int -> prop

axiom is_uint64_def :
  (forall x:int [is_uint64(x)]. (is_uint64(x) -> (0 <= x)))

axiom is_uint64_def1 :
  (forall x:int [is_uint64(x)]. (is_uint64(x) ->
  (x <  18446744073709551616)))

axiom is_uint64_def2 :
  (forall x:int [is_uint64(x)]. (((0 <= x) and
  (x <  18446744073709551616)) -> is_uint64(x)))

logic is_sint64 : int -> prop

axiom is_sint64_def :
  (forall x:int [is_sint64(x)]. (is_sint64(x) ->
  ((-9223372036854775808) <= x)))

axiom is_sint64_def1 :
  (forall x:int [is_sint64(x)]. (is_sint64(x) -> (x <  9223372036854775808)))

axiom is_sint64_def2 :
  (forall x:int [is_sint64(x)]. ((((-9223372036854775808) <= x) and
  (x <  9223372036854775808)) -> is_sint64(x)))

logic to_uint8 : int -> int

logic to_sint8 : int -> int

logic to_uint16 : int -> int

logic to_sint16 : int -> int

logic to_uint32 : int -> int

logic to_sint32 : int -> int

logic to_uint64 : int -> int

logic to_sint64 : int -> int

logic two_power_abs : int -> int

predicate is_uint(n: int, x: int) = ((0 <= x) and (x <  two_power_abs(n)))

predicate is_sint(n: int, x: int) = (((-two_power_abs(n)) <= x) and
  (x <  two_power_abs(n)))

logic to_uint : int, int -> int

logic to_sint : int, int -> int

axiom is_to_uint8 :
  (forall x:int [is_uint8(to_uint8(x))]. is_uint8(to_uint8(x)))

axiom is_to_sint8 :
  (forall x:int [is_sint8(to_sint8(x))]. is_sint8(to_sint8(x)))

axiom is_to_uint16 :
  (forall x:int [is_uint16(to_uint16(x))]. is_uint16(to_uint16(x)))

axiom is_to_sint16 :
  (forall x:int [is_sint16(to_sint16(x))]. is_sint16(to_sint16(x)))

axiom is_to_uint32 :
  (forall x:int [is_uint32(to_uint32(x))]. is_uint32(to_uint32(x)))

axiom is_to_sint32 :
  (forall x:int [is_sint32(to_sint32(x))]. is_sint32(to_sint32(x)))

axiom is_to_uint64 :
  (forall x:int [is_uint64(to_uint64(x))]. is_uint64(to_uint64(x)))

axiom is_to_sint64 :
  (forall x:int [is_sint64(to_sint64(x))]. is_sint64(to_sint64(x)))

axiom id_uint8 :
  (forall x:int [to_uint8(x)]. (((0 <= x) and (x <  256)) ->
  (to_uint8(x) = x)))

axiom id_sint8 :
  (forall x:int [to_sint8(x)]. ((((-128) <= x) and (x <  128)) ->
  (to_sint8(x) = x)))

axiom id_uint16 :
  (forall x:int [to_uint16(x)]. (((0 <= x) and (x <  65536)) ->
  (to_uint16(x) = x)))

axiom id_sint16 :
  (forall x:int [to_sint16(x)]. ((((-32768) <= x) and (x <  32768)) ->
  (to_sint16(x) = x)))

axiom id_uint32 :
  (forall x:int [to_uint32(x)]. (((0 <= x) and (x <  4294967296)) ->
  (to_uint32(x) = x)))

axiom id_sint32 :
  (forall x:int [to_sint32(x)]. ((((-2147483648) <= x) and
  (x <  2147483648)) -> (to_sint32(x) = x)))

axiom id_uint64 :
  (forall x:int [to_uint64(x)]. (((0 <= x) and
  (x <  18446744073709551616)) -> (to_uint64(x) = x)))

axiom id_sint64 :
  (forall x:int [to_sint64(x)]. ((((-9223372036854775808) <= x) and
  (x <  9223372036854775808)) -> (to_sint64(x) = x)))

axiom proj_int8 :
  (forall x:int [to_sint8(to_uint8(x))].
  (to_sint8(to_uint8(x)) = to_sint8(x)))

axiom proj_int16 :
  (forall x:int [to_sint16(to_uint16(x))].
  (to_sint16(to_uint16(x)) = to_sint16(x)))

axiom proj_int32 :
  (forall x:int [to_sint32(to_uint32(x))].
  (to_sint32(to_uint32(x)) = to_sint32(x)))

axiom proj_int64 :
  (forall x:int [to_sint64(to_uint64(x))].
  (to_sint64(to_uint64(x)) = to_sint64(x)))

logic lnot : int -> int

logic ac land : int, int -> int

logic ac lxor : int, int -> int

logic ac lor : int, int -> int

logic lsl : int, int -> int

logic lsr : int, int -> int

logic bit_testb : int, int -> bool

logic bit_test : int, int -> prop

(* ---------------------------------------------------------- *)
(* --- Post-condition (file fc.c, line 5) in 'test_uint8_cast_mod256_eq' --- *)
(* ---------------------------------------------------------- *)

goal test_uint8_cast_mod256_eq_post:
  forall i : int.
  (0 < i) ->
  (i <= 255) ->
  is_sint32(i) ->
  (to_uint8(i) = (safe_comp_mod(i, 256)))

-------------- section suivante --------------
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
(*                        énergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(* this is a prelude for Alt-Ergo integer arithmetic *)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
(*                        énergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
logic abs_int : int -> int

axiom abs_def : (forall x:int. ((0 <= x) -> (abs_int(x) = x)))

axiom abs_def1 : (forall x:int. ((not (0 <= x)) -> (abs_int(x) = (-x))))

axiom Abs_le :
  (forall x:int. forall y:int. ((abs_int(x) <= y) -> ((-y) <= x)))

axiom Abs_le1 : (forall x:int. forall y:int. ((abs_int(x) <= y) -> (x <= y)))

axiom Abs_le2 :
  (forall x:int. forall y:int. ((((-y) <= x) and (x <= y)) ->
  (abs_int(x) <= y)))

axiom Abs_pos : (forall x:int. (0 <= abs_int(x)))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
(*                        énergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
logic safe_comp_div: int, int -> int
axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y
logic safe_comp_mod: int, int -> int
axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory int_Abs_ must be appended to this file*)
axiom Div_bound :
  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
  (0 <= safe_comp_div(x,y))))

axiom Div_bound1 :
  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
  (safe_comp_div(x,y) <= x)))

axiom Div_1 : (forall x:int. (safe_comp_div(x,1) = x))

axiom Mod_1 : (forall x:int. (safe_comp_mod(x,1) = 0))

axiom Div_inf :
  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) ->
  (safe_comp_div(x,y) = 0)))

axiom Mod_inf :
  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) ->
  (safe_comp_mod(x,y) = x)))

axiom Div_mult :
  (forall x:int. forall y:int. forall z:int [safe_comp_div(((x * y) + z),x)].
  (((0 <  x) and ((0 <= y) and (0 <= z))) ->
  (safe_comp_div(((x * y) + z),x) = (y + safe_comp_div(z,x)))))

axiom Mod_mult :
  (forall x:int. forall y:int. forall z:int [safe_comp_mod(((x * y) + z),x)].
  (((0 <  x) and ((0 <= y) and (0 <= z))) ->
  (safe_comp_mod(((x * y) + z),x) = safe_comp_mod(z,x))))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
(*                        énergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(* this is a prelude for Alt-Ergo real arithmetic *)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
axiom add_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x + y) / z) = ((x / z) + (y / z)))))

axiom sub_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x - y) / z) = ((x / z) - (y / z)))))

axiom neg_div :
  (forall x:real. forall y:real. ((not (y = 0.0)) ->
  (((-x) / y) = (-(x / y)))))

axiom assoc_mul_div :
  (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
  (((x * y) / z) = (x * (y / z)))))

axiom assoc_div_mul :
  (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
  (not (z = 0.0))) -> (((x / y) / z) = (x / (y * z)))))

axiom assoc_div_div :
  (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
  (not (z = 0.0))) -> ((x / (y / z)) = ((x * z) / y))))

(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
(*                        énergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
(**************************************************************************)
(*                                                                        *)
(*  The Why3 Verification Platform   /   The Why3 Development Team        *)
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University        *)
(*                                                                        *)
(*  This software is distributed under the terms of the GNU Lesser        *)
(*  General Public License version 2.1, with the special exception        *)
(*  on linking described in file LICENSE.                                 *)
(*                                                                        *)
(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
(*                        énergies alternatives).                         *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
logic from_int : int -> real

axiom Zero : (from_int(0) = 0.0)

axiom One : (from_int(1) = 1.0)

axiom Add :
  (forall x:int. forall y:int.
  (from_int((x + y)) = (from_int(x) + from_int(y))))

axiom Sub :
  (forall x:int. forall y:int.
  (from_int((x - y)) = (from_int(x) - from_int(y))))

axiom Mul :
  (forall x:int. forall y:int.
  (from_int((x * y)) = (from_int(x) * from_int(y))))

axiom Neg : (forall x:int. (from_int((-x)) = (-from_int(x))))

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2015                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory bool_Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
(** The theory int_Abs_ must be appended to this file*)
(** The theory int_ComputerDivision_ must be appended to this file*)
(** The theory real_Real_ must be appended to this file*)
(** The theory real_RealInfix_ must be appended to this file*)
(** The theory real_FromInt_ must be appended to this file*)
logic ite : bool, 'a, 'a -> 'a

axiom ite1 :
  (forall p:bool. forall x:'a. forall y:'a [ite(p, x, y)]. (((p = true) and
  (ite(p, x, y) = x)) or ((p = false) and (ite(p, x, y) = y))))

logic eqb : 'a, 'a -> bool

axiom eqb1 : (forall x:'a. forall y:'a. ((eqb(x, y) = true) -> (x = y)))

axiom eqb2 : (forall x:'a. forall y:'a. ((x = y) -> (eqb(x, y) = true)))

logic neqb : 'a, 'a -> bool

axiom neqb1 :
  (forall x:'a. forall y:'a. ((neqb(x, y) = true) -> (not (x = y))))

axiom neqb2 :
  (forall x:'a. forall y:'a. ((not (x = y)) -> (neqb(x, y) = true)))

logic zlt : int, int -> bool

logic zleq : int, int -> bool

axiom zlt1 : (forall x:int. forall y:int. ((zlt(x, y) = true) -> (x <  y)))

axiom zlt2 : (forall x:int. forall y:int. ((x <  y) -> (zlt(x, y) = true)))

axiom zleq1 : (forall x:int. forall y:int. ((zleq(x, y) = true) -> (x <= y)))

axiom zleq2 : (forall x:int. forall y:int. ((x <= y) -> (zleq(x, y) = true)))

logic rlt : real, real -> bool

logic rleq : real, real -> bool

axiom rlt1 : (forall x:real. forall y:real. ((rlt(x, y) = true) -> (x <  y)))

axiom rlt2 : (forall x:real. forall y:real. ((x <  y) -> (rlt(x, y) = true)))

axiom rleq1 :
  (forall x:real. forall y:real. ((rleq(x, y) = true) -> (x <= y)))

axiom rleq2 :
  (forall x:real. forall y:real. ((x <= y) -> (rleq(x, y) = true)))

logic truncate : real -> int

function real_of_int(x: int) : real = from_int(x)

axiom truncate_of_int : (forall x:int. (truncate(real_of_int(x)) = x))

axiom c_euclidian :
  (forall n:int. forall d:int [safe_comp_div(n,d), safe_comp_mod(n,d)].
  ((not (d = 0)) -> (n = ((safe_comp_div(n,d) * d) + safe_comp_mod(n,d)))))

axiom cdiv_cases :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_div(n,d) = (n / d)))))

axiom cdiv_cases1 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_div(n,d) = (-((-n) / d))))))

axiom cdiv_cases2 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_div(n,d) = (-(n / (-d)))))))

axiom cdiv_cases3 :
  (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_div(n,d) = ((-n) / (-d))))))

axiom cmod_cases :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_mod(n,d) = (n % d)))))

axiom cmod_cases1 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_mod(n,d) = (-((-n) % d))))))

axiom cmod_cases2 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_mod(n,d) = (n % (-d))))))

axiom cmod_cases3 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_mod(n,d) = (-((-n) % (-d)))))))

axiom cmod_remainder :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (0 <= safe_comp_mod(n,d)))))

axiom cmod_remainder1 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 <  d) ->
  (safe_comp_mod(n,d) <  d))))

axiom cmod_remainder2 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  ((-d) <  safe_comp_mod(n,d)))))

axiom cmod_remainder3 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 <  d) ->
  (safe_comp_mod(n,d) <= 0))))

axiom cmod_remainder4 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (0 <= safe_comp_mod(n,d)))))

axiom cmod_remainder5 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d <  0) ->
  (safe_comp_mod(n,d) <  (-d)))))

axiom cmod_remainder6 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (d <  safe_comp_mod(n,d)))))

axiom cmod_remainder7 :
  (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d <  0) ->
  (safe_comp_mod(n,d) <= 0))))

axiom cdiv_neutral :
  (forall a:int [safe_comp_div(a,1)]. (safe_comp_div(a,1) = a))

axiom cdiv_inv :
  (forall a:int [safe_comp_div(a,a)]. ((not (a = 0)) ->
  (safe_comp_div(a,a) = 1)))

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2015                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* this is a prelude for Alt-Ergo*)
(** The theory BuiltIn_ must be appended to this file*)
(** The theory Bool_ must be appended to this file*)
(** The theory bool_Bool_ must be appended to this file*)
(** The theory int_Int_ must be appended to this file*)
logic is_uint8 : int -> prop

axiom is_uint8_def : (forall x:int [is_uint8(x)]. (is_uint8(x) -> (0 <= x)))

axiom is_uint8_def1 :
  (forall x:int [is_uint8(x)]. (is_uint8(x) -> (x <  256)))

axiom is_uint8_def2 :
  (forall x:int [is_uint8(x)]. (((0 <= x) and (x <  256)) -> is_uint8(x)))

logic is_sint8 : int -> prop

axiom is_sint8_def :
  (forall x:int [is_sint8(x)]. (is_sint8(x) -> ((-128) <= x)))

axiom is_sint8_def1 :
  (forall x:int [is_sint8(x)]. (is_sint8(x) -> (x <  128)))

axiom is_sint8_def2 :
  (forall x:int [is_sint8(x)]. ((((-128) <= x) and (x <  128)) ->
  is_sint8(x)))

logic is_uint16 : int -> prop

axiom is_uint16_def :
  (forall x:int [is_uint16(x)]. (is_uint16(x) -> (0 <= x)))

axiom is_uint16_def1 :
  (forall x:int [is_uint16(x)]. (is_uint16(x) -> (x <  65536)))

axiom is_uint16_def2 :
  (forall x:int [is_uint16(x)]. (((0 <= x) and (x <  65536)) ->
  is_uint16(x)))

predicate is_sint16(x: int) = (((-32768) <= x) and (x <  32768))

logic is_uint32 : int -> prop

axiom is_uint32_def :
  (forall x:int [is_uint32(x)]. (is_uint32(x) -> (0 <= x)))

axiom is_uint32_def1 :
  (forall x:int [is_uint32(x)]. (is_uint32(x) -> (x <  4294967296)))

axiom is_uint32_def2 :
  (forall x:int [is_uint32(x)]. (((0 <= x) and (x <  4294967296)) ->
  is_uint32(x)))

logic is_sint32 : int -> prop

axiom is_sint32_def :
  (forall x:int [is_sint32(x)]. (is_sint32(x) -> ((-2147483648) <= x)))

axiom is_sint32_def1 :
  (forall x:int [is_sint32(x)]. (is_sint32(x) -> (x <  2147483648)))

axiom is_sint32_def2 :
  (forall x:int [is_sint32(x)]. ((((-2147483648) <= x) and
  (x <  2147483648)) -> is_sint32(x)))

logic is_uint64 : int -> prop

axiom is_uint64_def :
  (forall x:int [is_uint64(x)]. (is_uint64(x) -> (0 <= x)))

axiom is_uint64_def1 :
  (forall x:int [is_uint64(x)]. (is_uint64(x) ->
  (x <  18446744073709551616)))

axiom is_uint64_def2 :
  (forall x:int [is_uint64(x)]. (((0 <= x) and
  (x <  18446744073709551616)) -> is_uint64(x)))

logic is_sint64 : int -> prop

axiom is_sint64_def :
  (forall x:int [is_sint64(x)]. (is_sint64(x) ->
  ((-9223372036854775808) <= x)))

axiom is_sint64_def1 :
  (forall x:int [is_sint64(x)]. (is_sint64(x) -> (x <  9223372036854775808)))

axiom is_sint64_def2 :
  (forall x:int [is_sint64(x)]. ((((-9223372036854775808) <= x) and
  (x <  9223372036854775808)) -> is_sint64(x)))

logic to_uint8 : int -> int

logic to_sint8 : int -> int

logic to_uint16 : int -> int

logic to_sint16 : int -> int

logic to_uint32 : int -> int

logic to_sint32 : int -> int

logic to_uint64 : int -> int

logic to_sint64 : int -> int

logic two_power_abs : int -> int

predicate is_uint(n: int, x: int) = ((0 <= x) and (x <  two_power_abs(n)))

predicate is_sint(n: int, x: int) = (((-two_power_abs(n)) <= x) and
  (x <  two_power_abs(n)))

logic to_uint : int, int -> int

logic to_sint : int, int -> int

axiom is_to_uint8 :
  (forall x:int [is_uint8(to_uint8(x))]. is_uint8(to_uint8(x)))

axiom is_to_sint8 :
  (forall x:int [is_sint8(to_sint8(x))]. is_sint8(to_sint8(x)))

axiom is_to_uint16 :
  (forall x:int [is_uint16(to_uint16(x))]. is_uint16(to_uint16(x)))

axiom is_to_sint16 :
  (forall x:int [is_sint16(to_sint16(x))]. is_sint16(to_sint16(x)))

axiom is_to_uint32 :
  (forall x:int [is_uint32(to_uint32(x))]. is_uint32(to_uint32(x)))

axiom is_to_sint32 :
  (forall x:int [is_sint32(to_sint32(x))]. is_sint32(to_sint32(x)))

axiom is_to_uint64 :
  (forall x:int [is_uint64(to_uint64(x))]. is_uint64(to_uint64(x)))

axiom is_to_sint64 :
  (forall x:int [is_sint64(to_sint64(x))]. is_sint64(to_sint64(x)))

axiom id_uint8 :
  (forall x:int [to_uint8(x)]. (((0 <= x) and (x <  256)) ->
  (to_uint8(x) = x)))

axiom id_sint8 :
  (forall x:int [to_sint8(x)]. ((((-128) <= x) and (x <  128)) ->
  (to_sint8(x) = x)))

axiom id_uint16 :
  (forall x:int [to_uint16(x)]. (((0 <= x) and (x <  65536)) ->
  (to_uint16(x) = x)))

axiom id_sint16 :
  (forall x:int [to_sint16(x)]. ((((-32768) <= x) and (x <  32768)) ->
  (to_sint16(x) = x)))

axiom id_uint32 :
  (forall x:int [to_uint32(x)]. (((0 <= x) and (x <  4294967296)) ->
  (to_uint32(x) = x)))

axiom id_sint32 :
  (forall x:int [to_sint32(x)]. ((((-2147483648) <= x) and
  (x <  2147483648)) -> (to_sint32(x) = x)))

axiom id_uint64 :
  (forall x:int [to_uint64(x)]. (((0 <= x) and
  (x <  18446744073709551616)) -> (to_uint64(x) = x)))

axiom id_sint64 :
  (forall x:int [to_sint64(x)]. ((((-9223372036854775808) <= x) and
  (x <  9223372036854775808)) -> (to_sint64(x) = x)))

axiom proj_int8 :
  (forall x:int [to_sint8(to_uint8(x))].
  (to_sint8(to_uint8(x)) = to_sint8(x)))

axiom proj_int16 :
  (forall x:int [to_sint16(to_uint16(x))].
  (to_sint16(to_uint16(x)) = to_sint16(x)))

axiom proj_int32 :
  (forall x:int [to_sint32(to_uint32(x))].
  (to_sint32(to_uint32(x)) = to_sint32(x)))

axiom proj_int64 :
  (forall x:int [to_sint64(to_uint64(x))].
  (to_sint64(to_uint64(x)) = to_sint64(x)))

logic lnot : int -> int

logic ac land : int, int -> int

logic ac lxor : int, int -> int

logic ac lor : int, int -> int

logic lsl : int, int -> int

logic lsr : int, int -> int

logic bit_testb : int, int -> bool

logic bit_test : int, int -> prop

(* ---------------------------------------------------------- *)
(* --- Post-condition (file fc.c, line 19) in 'test_uint8_cast_mod256_eq__v3' --- *)
(* ---------------------------------------------------------- *)

goal test_uint8_cast_mod256_eq__v3_post:
  forall i : int.
  (300 <= i) ->
  (i <= 302) ->
  is_sint32(i) ->
  (to_uint8(i) = (safe_comp_mod(i, 256)))