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: iguer.pro at gmail.com (Mohamed Iguernlala)
- Date: Mon, 21 Mar 2016 07:12:26 +0100
- In-reply-to: <845751458525473@web1m.yandex.ru>
- References: <845751458525473@web1m.yandex.ru>
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)))
- Follow-Ups:
- [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)
- [Frama-c-discuss] Problem with werify mod 256 and cast to uint8 equivalence for uint64_t
- From: mmcco at mykolab.com (Michael McConville)
- [Frama-c-discuss] Problem with werify mod 256 and cast to uint8 equivalence for uint64_t
- References:
- [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)
- [Frama-c-discuss] Problem with werify mod 256 and cast to uint8 equivalence for uint64_t
- Prev by Date: [Frama-c-discuss] Problem with werify mod 256 and cast to uint8 equivalence for uint64_t
- Next by Date: [Frama-c-discuss] Problem with werify mod 256 and cast to uint8 equivalence for uint64_t
- Previous by thread: [Frama-c-discuss] Problem with werify mod 256 and cast to uint8 equivalence for uint64_t
- Next by thread: [Frama-c-discuss] Problem with werify mod 256 and cast to uint8 equivalence for uint64_t
- Index(es):