diff --git a/src/plugins/wp/share/why3/ArcTrigo.why b/src/plugins/wp/share/why3/ArcTrigo.why deleted file mode 100644 index bf76b70b1fd9bbae8ffdcb49f748faf8030f2583..0000000000000000000000000000000000000000 --- a/src/plugins/wp/share/why3/ArcTrigo.why +++ /dev/null @@ -1,41 +0,0 @@ -(**************************************************************************) -(* *) -(* This file is part of WP plug-in of Frama-C. *) -(* *) -(* Copyright (C) 2007-2019 *) -(* 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). *) -(* *) -(**************************************************************************) - -theory ArcTrigo -use real.Real as Real -use real.Abs as Abs -use real.Square as Square -use real.Trigonometry as Trigonometry - -function atan (x:real) : real = Trigonometry.atan x - -function asin real : real - -function acos real : real - -axiom Sin_asin : forall x:real. (Real.(<=) ((Real.(-_) (1.0))) (x)) /\ - (Real.(<=) (x) (1.0)) -> ((Trigonometry.sin (asin x)) = (x)) - -axiom Cos_acos : forall x:real. (Real.(<=) ((Real.(-_) (1.0))) (x)) /\ - (Real.(<=) (x) (1.0)) -> ((Trigonometry.cos (acos x)) = (x)) - -end diff --git a/src/plugins/wp/share/why3/Cbits.why b/src/plugins/wp/share/why3/Cbits.why deleted file mode 100644 index 28641d4d40546e4ee840f359cb862d02aa73efc2..0000000000000000000000000000000000000000 --- a/src/plugins/wp/share/why3/Cbits.why +++ /dev/null @@ -1,403 +0,0 @@ -(**************************************************************************) -(* *) -(* This file is part of WP plug-in of Frama-C. *) -(* *) -(* Copyright (C) 2007-2019 *) -(* 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). *) -(* *) -(**************************************************************************) - -theory Cbits -use Qed.Qed as Qed -use bool.Bool as Bool -use int.Int as Int -use int.Abs as Abs -use int.ComputerDivision as ComputerDivision -use real.Real as Real -use real.FromInt as FromInt -use Cint.Cint as Cint - -lemma lnot_bool : ((Cint.lnot 0) = ((Int.(-_) (1)))) /\ ((Cint.lnot - (Int.(-_) (1))) = (0)) - -lemma land_idemp : forall x:int [Cint.land x x]. ((Cint.land x x) = (x)) - -lemma land_0 : forall x:int [Cint.land 0 x]. ((Cint.land 0 x) = (0)) - -lemma land_0bis : forall x:int [Cint.land x 0]. ((Cint.land x 0) = (0)) - -lemma land_1 : forall x:int [Cint.land (Int.(-_) (1)) x]. ((Cint.land - (Int.(-_) (1)) x) = (x)) - -lemma land_1bis : forall x:int [Cint.land x (Int.(-_) (1))]. ((Cint.land x - (Int.(-_) (1))) = (x)) - -lemma lor_idemp : forall x:int [Cint.lor x x]. ((Cint.lor x x) = (x)) - -lemma lor_1 : forall x:int [Cint.lor (Int.(-_) (1)) x]. ((Cint.lor - (Int.(-_) (1)) x) = ((Int.(-_) (1)))) - -lemma lor_1bis : forall x:int [Cint.lor x (Int.(-_) (1))]. ((Cint.lor x - (Int.(-_) (1))) = ((Int.(-_) (1)))) - -lemma lor_0 : forall x:int [Cint.lor 0 x]. ((Cint.lor 0 x) = (x)) - -lemma lor_0bis : forall x:int [Cint.lor x 0]. ((Cint.lor x 0) = (x)) - -lemma lxor_nilpotent : forall x:int [Cint.lxor x x]. ((Cint.lxor x x) = (0)) - -lemma lxor_1 : forall x:int [Cint.lxor (Int.(-_) (1)) x]. ((Cint.lxor - (Int.(-_) (1)) x) = (Cint.lnot x)) - -lemma lxor_1bis : forall x:int [Cint.lxor x (Int.(-_) (1))]. ((Cint.lxor x - (Int.(-_) (1))) = (Cint.lnot x)) - -lemma lxor_0 : forall x:int [Cint.lxor 0 x]. ((Cint.lxor 0 x) = (x)) - -lemma lxor_0bis : forall x:int [Cint.lxor x 0]. ((Cint.lxor x 0) = (x)) - -lemma bit_test_def : forall x:int, k:int [Cint.bit_testb x k]. - ((Cint.bit_testb x k) = (Bool.True)) <-> Cint.bit_test x k - -lemma bit_test_extraction : forall x:int, k:int [Cint.land x (Cint.lsl 1 k)| - Cint.land (Cint.lsl 1 k) x]. (Int.(<=) (0) (k)) -> not ((Cint.land x - (Cint.lsl 1 k)) = (0)) <-> Cint.bit_test x k - -lemma lsl_1_0 : ((Cint.lsl 1 0) = (1)) - -lemma bit_test_extraction_bis : forall x:int [Cint.land x 1| Cint.land 1 x]. - not ((Cint.land 1 x) = (0)) -> Cint.bit_test x 0 - -lemma bit_test_extraction_bis_eq : forall x:int [Cint.land x 1| Cint.land 1 - x]. Cint.bit_test x 0 -> ((Cint.land 1 x) = (1)) - -lemma lnot_extraction : forall x:int, i:int [Cint.bit_test (Cint.lnot x) i]. - (Int.(<=) (0) (i)) -> Cint.bit_test (Cint.lnot x) i <-> not Cint.bit_test x - i - -lemma land_extraction : forall x:int, y:int, i:int [Cint.bit_test (Cint.land - x y) i]. (Int.(<=) (0) (i)) -> Cint.bit_test (Cint.land x y) i <-> - Cint.bit_test x i /\ Cint.bit_test y i - -lemma lor_extraction : forall x:int, y:int, i:int [Cint.bit_test (Cint.lor x - y) i]. (Int.(<=) (0) (i)) -> Cint.bit_test (Cint.lor x y) i <-> - Cint.bit_test x i \/ Cint.bit_test y i - -lemma lxor_extraction : forall x:int, y:int, i:int [Cint.bit_test (Cint.lxor - x y) i]. (Int.(<=) (0) (i)) -> Cint.bit_test (Cint.lxor x y) i <-> - Cint.bit_test x i <-> not Cint.bit_test y i - -lemma land_1_lsl_1 : forall a:int, x:int, n:int [Cint.lsl 1 - (Int.(+) (1) (n)), Cint.lsl 1 n, (Int.(+) ((Int.(*) (2) (a))) (Cint.land 1 - x))]. (Int.(<=) (0) (n)) -> (Int.(<) (a) (Cint.lsl 1 n)) -> - (Int.(<) ((Int.(+) ((Int.(*) (2) (a))) (Cint.land 1 x))) (Cint.lsl 1 - (Int.(+) (1) (n)))) - -lemma lsl_extraction_sup : forall x:int, n:int, m:int [Cint.bit_test - (Cint.lsl x n) m]. (Int.(<=) (0) (n)) -> (Int.(<=) (0) (m)) -> - (Int.(>=) (m) (n)) -> Cint.bit_test (Cint.lsl x n) m <-> Cint.bit_test x - (Int.(-) (m) (n)) - -lemma lsl_extraction_inf : forall x:int, n:int, m:int [Cint.bit_test - (Cint.lsl x n) m]. (Int.(<=) (0) (n)) -> (Int.(<=) (0) (m)) -> - (Int.(<) (m) (n)) -> not Cint.bit_test (Cint.lsl x n) m - -lemma lsr_extractionl : forall x:int, n:int, m:int [Cint.bit_test (Cint.lsr x - n) m]. (Int.(<=) (0) (n)) -> (Int.(<=) (0) (m)) -> Cint.bit_test (Cint.lsr - x n) m <-> Cint.bit_test x (Int.(+) (m) (n)) - -lemma lsl1_extraction : forall i:int, j:int [Cint.bit_test (Cint.lsl 1 i) j]. - (Int.(<=) (0) (i)) -> (Int.(<=) (0) (j)) -> Cint.bit_test (Cint.lsl 1 i) - j <-> ((i) = (j)) - -lemma to_uint8_extraction_sup : forall x:int, i:int [Cint.is_uint8 x, - Cint.bit_test x i]. (Int.(<=) (8) (i)) -> Cint.is_uint8 x -> - not Cint.bit_test x i - -lemma to_uint8_extraction_inf : forall x:int, i:int [Cint.bit_test - (Cint.to_uint8 x) i]. (Int.(<=) (0) (i)) /\ (Int.(<) (i) (8)) -> - Cint.bit_test (Cint.to_uint8 x) i <-> Cint.bit_test x i - -lemma to_uint16_extraction_sup : forall x:int, i:int [Cint.is_uint16 x, - Cint.bit_test x i]. (Int.(<=) (16) (i)) -> Cint.is_uint16 x -> - not Cint.bit_test x i - -lemma to_uint16_extraction_inf : forall x:int, i:int [Cint.bit_test - (Cint.to_uint16 x) i]. (Int.(<=) (0) (i)) /\ (Int.(<) (i) (16)) -> - Cint.bit_test (Cint.to_uint16 x) i <-> Cint.bit_test x i - -lemma to_uint32_extraction_sup : forall x:int, i:int [Cint.is_uint32 x, - Cint.bit_test x i]. (Int.(<=) (32) (i)) -> Cint.is_uint32 x -> - not Cint.bit_test x i - -lemma to_uint32_extraction_inf : forall x:int, i:int [Cint.bit_test - (Cint.to_uint32 x) i]. (Int.(<=) (0) (i)) /\ (Int.(<) (i) (32)) -> - Cint.bit_test (Cint.to_uint32 x) i <-> Cint.bit_test x i - -lemma to_uint64_extraction_sup : forall x:int, i:int [Cint.is_uint64 x, - Cint.bit_test x i]. (Int.(<=) (64) (i)) -> Cint.is_uint64 x -> - not Cint.bit_test x i - -lemma to_uint64_extraction_inf : forall x:int, i:int [Cint.bit_test - (Cint.to_uint64 x) i]. (Int.(<=) (0) (i)) /\ (Int.(<) (i) (64)) -> - Cint.bit_test (Cint.to_uint64 x) i <-> Cint.bit_test x i - -lemma to_sint8_extraction_sup : forall x:int, i:int [Cint.is_sint8 x, - Cint.bit_test x i]. (Int.(<=) (7) (i)) -> Cint.is_sint8 x -> Cint.bit_test - x i <-> (Int.(<) (x) (0)) - -lemma to_sint8_extraction_inf : forall x:int, i:int [Cint.bit_test - (Cint.to_sint8 x) i]. (Int.(<=) (0) (i)) /\ (Int.(<) (i) (7)) -> - Cint.bit_test (Cint.to_sint8 x) i <-> Cint.bit_test x i - -lemma to_sint16_extraction_sup : forall x:int, i:int [Cint.is_sint16 x, - Cint.bit_test x i]. (Int.(<=) (15) (i)) -> Cint.is_sint16 x -> - Cint.bit_test x i <-> (Int.(<) (x) (0)) - -lemma to_sint16_extraction_inf : forall x:int, i:int [Cint.bit_test - (Cint.to_sint16 x) i]. (Int.(<=) (0) (i)) /\ (Int.(<) (i) (15)) -> - Cint.bit_test (Cint.to_sint16 x) i <-> Cint.bit_test x i - -lemma to_sint32_extraction_sup : forall x:int, i:int [Cint.is_sint32 x, - Cint.bit_test x i]. (Int.(<=) (31) (i)) -> Cint.is_sint32 x -> - Cint.bit_test x i <-> (Int.(<) (x) (0)) - -lemma to_sint32_extraction_inf : forall x:int, i:int [Cint.bit_test - (Cint.to_sint32 x) i]. (Int.(<=) (0) (i)) /\ (Int.(<) (i) (31)) -> - Cint.bit_test (Cint.to_sint32 x) i <-> Cint.bit_test x i - -lemma to_sint64_extraction_sup : forall x:int, i:int [Cint.is_sint64 x, - Cint.bit_test x i]. (Int.(<=) (63) (i)) -> Cint.is_sint64 x -> - Cint.bit_test x i <-> (Int.(<) (x) (0)) - -lemma to_sint64_extraction_inf : forall x:int, i:int [Cint.bit_test - (Cint.to_sint64 x) i]. (Int.(<=) (0) (i)) /\ (Int.(<) (i) (63)) -> - Cint.bit_test (Cint.to_sint64 x) i <-> Cint.bit_test x i - -lemma is_uint_lxor : forall n:int, x:int, y:int. Cint.is_uint n x -> - Cint.is_uint n y -> ((Cint.to_uint n (Cint.lxor x y)) = (Cint.lxor x y)) - -lemma is_uint8_lxor : forall x:int, y:int [Cint.to_uint8 (Cint.lxor x y)]. - Cint.is_uint8 x -> Cint.is_uint8 y -> ((Cint.to_uint8 (Cint.lxor x - y)) = (Cint.lxor x y)) - -lemma is_uint8_lor : forall x:int, y:int [Cint.to_uint8 (Cint.lor x y)]. - Cint.is_uint8 x -> Cint.is_uint8 y -> ((Cint.to_uint8 (Cint.lor x - y)) = (Cint.lor x y)) - -lemma is_uint8_land : forall x:int, y:int [Cint.to_uint8 (Cint.land x y)]. - Cint.is_uint8 x -> Cint.is_uint8 y -> ((Cint.to_uint8 (Cint.land x - y)) = (Cint.land x y)) - -lemma is_uint8_lsr : forall x:int, y:int [Cint.to_uint8 (Cint.lsr x y)]. - (Int.(<=) (0) (y)) -> Cint.is_uint8 x -> ((Cint.to_uint8 (Cint.lsr x - y)) = (Cint.lsr x y)) - -lemma is_uint8_lsl1_inf : forall y:int [Cint.to_uint8 (Cint.lsl 1 y)]. - (Int.(<=) (0) (y)) /\ (Int.(<) (y) (8)) -> ((Cint.to_uint8 (Cint.lsl 1 - y)) = (Cint.lsl 1 y)) - -lemma is_uint8_lsl1_sup : forall y:int [Cint.to_uint8 (Cint.lsl 1 y)]. - (Int.(<=) (8) (y)) -> ((Cint.to_uint8 (Cint.lsl 1 y)) = (0)) - -lemma is_uint16_lxor : forall x:int, y:int [Cint.to_uint16 (Cint.lxor x y)]. - Cint.is_uint16 x -> Cint.is_uint16 y -> ((Cint.to_uint16 (Cint.lxor x - y)) = (Cint.lxor x y)) - -lemma is_uint16_lor : forall x:int, y:int [Cint.to_uint16 (Cint.lor x y)]. - Cint.is_uint16 x -> Cint.is_uint16 y -> ((Cint.to_uint16 (Cint.lor x - y)) = (Cint.lor x y)) - -lemma is_uint16_land : forall x:int, y:int [Cint.to_uint16 (Cint.land x y)]. - Cint.is_uint16 x -> Cint.is_uint16 y -> ((Cint.to_uint16 (Cint.land x - y)) = (Cint.land x y)) - -lemma is_uint16_lsr : forall x:int, y:int [Cint.to_uint16 (Cint.lsr x y)]. - (Int.(<=) (0) (y)) -> Cint.is_uint16 x -> ((Cint.to_uint16 (Cint.lsr x - y)) = (Cint.lsr x y)) - -lemma is_uint16_lsl1_inf : forall y:int [Cint.to_uint16 (Cint.lsl 1 y)]. - (Int.(<=) (0) (y)) /\ (Int.(<) (y) (16)) -> ((Cint.to_uint16 (Cint.lsl 1 - y)) = (Cint.lsl 1 y)) - -lemma is_uint16_lsl1_sup : forall y:int [Cint.to_uint16 (Cint.lsl 1 y)]. - (Int.(<=) (16) (y)) -> ((Cint.to_uint16 (Cint.lsl 1 y)) = (0)) - -lemma is_uint32_lxor : forall x:int, y:int [Cint.to_uint32 (Cint.lxor x y)]. - Cint.is_uint32 x -> Cint.is_uint32 y -> ((Cint.to_uint32 (Cint.lxor x - y)) = (Cint.lxor x y)) - -lemma is_uint32_lor : forall x:int, y:int [Cint.to_uint32 (Cint.lor x y)]. - Cint.is_uint32 x -> Cint.is_uint32 y -> ((Cint.to_uint32 (Cint.lor x - y)) = (Cint.lor x y)) - -lemma is_uint32_land : forall x:int, y:int [Cint.to_uint32 (Cint.land x y)]. - Cint.is_uint32 x -> Cint.is_uint32 y -> ((Cint.to_uint32 (Cint.land x - y)) = (Cint.land x y)) - -lemma is_uint32_lsr : forall x:int, y:int [Cint.to_uint32 (Cint.lsr x y)]. - (Int.(<=) (0) (y)) -> Cint.is_uint32 x -> ((Cint.to_uint32 (Cint.lsr x - y)) = (Cint.lsr x y)) - -lemma is_uint32_lsl1_inf : forall y:int [Cint.to_uint32 (Cint.lsl 1 y)]. - (Int.(<=) (0) (y)) /\ (Int.(<) (y) (32)) -> ((Cint.to_uint32 (Cint.lsl 1 - y)) = (Cint.lsl 1 y)) - -lemma is_uint32_lsl1_sup : forall y:int [Cint.to_uint32 (Cint.lsl 1 y)]. - (Int.(<=) (32) (y)) -> ((Cint.to_uint32 (Cint.lsl 1 y)) = (0)) - -lemma is_uint64_lxor : forall x:int, y:int [Cint.to_uint64 (Cint.lxor x y)]. - Cint.is_uint64 x -> Cint.is_uint64 y -> ((Cint.to_uint64 (Cint.lxor x - y)) = (Cint.lxor x y)) - -lemma is_uint64_lor : forall x:int, y:int [Cint.to_uint64 (Cint.lor x y)]. - Cint.is_uint64 x -> Cint.is_uint64 y -> ((Cint.to_uint64 (Cint.lor x - y)) = (Cint.lor x y)) - -lemma is_uint64_land : forall x:int, y:int [Cint.to_uint64 (Cint.land x y)]. - Cint.is_uint64 x -> Cint.is_uint64 y -> ((Cint.to_uint64 (Cint.land x - y)) = (Cint.land x y)) - -lemma is_uint64_lsr : forall x:int, y:int [Cint.to_uint64 (Cint.lsr x y)]. - (Int.(<=) (0) (y)) -> Cint.is_uint64 x -> ((Cint.to_uint64 (Cint.lsr x - y)) = (Cint.lsr x y)) - -lemma is_uint64_lsl1_inf : forall y:int [Cint.to_uint64 (Cint.lsl 1 y)]. - (Int.(<=) (0) (y)) /\ (Int.(<) (y) (64)) -> ((Cint.to_uint64 (Cint.lsl 1 - y)) = (Cint.lsl 1 y)) - -lemma is_uint64_lsl1_sup : forall y:int [Cint.to_uint64 (Cint.lsl 1 y)]. - (Int.(<=) (64) (y)) -> ((Cint.to_uint64 (Cint.lsl 1 y)) = (0)) - -lemma is_sint8_lnot : forall x:int [Cint.to_sint8 (Cint.lnot x)]. - Cint.is_sint8 x -> ((Cint.to_sint8 (Cint.lnot x)) = (Cint.lnot x)) - -lemma is_sint8_lxor : forall x:int, y:int [Cint.to_sint8 (Cint.lxor x y)]. - Cint.is_sint8 x -> Cint.is_sint8 y -> ((Cint.to_sint8 (Cint.lxor x - y)) = (Cint.lxor x y)) - -lemma is_sint8_lor : forall x:int, y:int [Cint.to_sint8 (Cint.lor x y)]. - Cint.is_sint8 x -> Cint.is_sint8 y -> ((Cint.to_sint8 (Cint.lor x - y)) = (Cint.lor x y)) - -lemma is_sint8_land : forall x:int, y:int [Cint.to_sint8 (Cint.land x y)]. - Cint.is_sint8 x -> Cint.is_sint8 y -> ((Cint.to_sint8 (Cint.land x - y)) = (Cint.land x y)) - -lemma is_sint8_lsr : forall x:int, y:int [Cint.to_sint8 (Cint.lsr x y)]. - (Int.(<=) (0) (y)) -> Cint.is_sint8 x -> ((Cint.to_sint8 (Cint.lsr x - y)) = (Cint.lsr x y)) - -lemma is_sint8_lsl1 : ((Cint.lsl 1 7) = (Cint.max_sint8)) - -lemma is_sint8_lsl1_inf : forall y:int [Cint.to_sint8 (Cint.lsl 1 y)]. - (Int.(<=) (0) (y)) /\ (Int.(<) (y) (7)) -> ((Cint.to_sint8 (Cint.lsl 1 - y)) = (Cint.lsl 1 y)) - -lemma is_sint8_lsl1_sup : forall y:int [Cint.to_sint8 (Cint.lsl 1 y)]. - (Int.(<=) (8) (y)) -> ((Cint.to_sint8 (Cint.lsl 1 y)) = (0)) - -lemma is_sint16_lnot : forall x:int [Cint.to_sint16 (Cint.lnot x)]. - Cint.is_sint16 x -> ((Cint.to_sint16 (Cint.lnot x)) = (Cint.lnot x)) - -lemma is_sint16_lxor : forall x:int, y:int [Cint.to_sint16 (Cint.lxor x y)]. - Cint.is_sint16 x -> Cint.is_sint16 y -> ((Cint.to_sint16 (Cint.lxor x - y)) = (Cint.lxor x y)) - -lemma is_sint16_lor : forall x:int, y:int [Cint.to_sint16 (Cint.lor x y)]. - Cint.is_sint16 x -> Cint.is_sint16 y -> ((Cint.to_sint16 (Cint.lor x - y)) = (Cint.lor x y)) - -lemma is_sint16_land : forall x:int, y:int [Cint.to_sint16 (Cint.land x y)]. - Cint.is_sint16 x -> Cint.is_sint16 y -> ((Cint.to_sint16 (Cint.land x - y)) = (Cint.land x y)) - -lemma is_sint16_lsr : forall x:int, y:int [Cint.to_sint16 (Cint.lsr x y)]. - (Int.(<=) (0) (y)) -> Cint.is_sint16 x -> ((Cint.to_sint16 (Cint.lsr x - y)) = (Cint.lsr x y)) - -lemma is_sint16_lsl1 : ((Cint.lsl 1 15) = (Cint.max_sint16)) - -lemma is_sint16_lsl1_inf : forall y:int [Cint.to_sint16 (Cint.lsl 1 y)]. - (Int.(<=) (0) (y)) /\ (Int.(<) (y) (15)) -> ((Cint.to_sint16 (Cint.lsl 1 - y)) = (Cint.lsl 1 y)) - -lemma is_sint16_lsl1_sup : forall y:int [Cint.to_sint16 (Cint.lsl 1 y)]. - (Int.(<=) (16) (y)) -> ((Cint.to_sint16 (Cint.lsl 1 y)) = (0)) - -lemma is_sint32_lnot : forall x:int [Cint.to_sint32 (Cint.lnot x)]. - Cint.is_sint32 x -> ((Cint.to_sint32 (Cint.lnot x)) = (Cint.lnot x)) - -lemma is_sint32_lxor : forall x:int, y:int [Cint.to_sint32 (Cint.lxor x y)]. - Cint.is_sint32 x -> Cint.is_sint32 y -> ((Cint.to_sint32 (Cint.lxor x - y)) = (Cint.lxor x y)) - -lemma is_sint32_lor : forall x:int, y:int [Cint.to_sint32 (Cint.lor x y)]. - Cint.is_sint32 x -> Cint.is_sint32 y -> ((Cint.to_sint32 (Cint.lor x - y)) = (Cint.lor x y)) - -lemma is_sint32_land : forall x:int, y:int [Cint.to_sint32 (Cint.land x y)]. - Cint.is_sint32 x -> Cint.is_sint32 y -> ((Cint.to_sint32 (Cint.land x - y)) = (Cint.land x y)) - -lemma is_sint32_lsr : forall x:int, y:int [Cint.to_sint32 (Cint.lsr x y)]. - (Int.(<=) (0) (y)) -> Cint.is_sint32 x -> ((Cint.to_sint32 (Cint.lsr x - y)) = (Cint.lsr x y)) - -lemma is_sint32_lsl1 : ((Cint.lsl 1 31) = (Cint.max_sint32)) - -lemma is_sint32_lsl1_inf : forall y:int [Cint.to_sint32 (Cint.lsl 1 y)]. - (Int.(<=) (0) (y)) /\ (Int.(<) (y) (31)) -> ((Cint.to_sint32 (Cint.lsl 1 - y)) = (Cint.lsl 1 y)) - -lemma is_sint32_lsl1_sup : forall y:int [Cint.to_sint32 (Cint.lsl 1 y)]. - (Int.(<=) (32) (y)) -> ((Cint.to_sint32 (Cint.lsl 1 y)) = (0)) - -lemma is_sint64_lnot : forall x:int [Cint.to_sint64 (Cint.lnot x)]. - Cint.is_sint64 x -> ((Cint.to_sint64 (Cint.lnot x)) = (Cint.lnot x)) - -lemma is_sint64_lxor : forall x:int, y:int [Cint.to_sint64 (Cint.lxor x y)]. - Cint.is_sint64 x -> Cint.is_sint64 y -> ((Cint.to_sint64 (Cint.lxor x - y)) = (Cint.lxor x y)) - -lemma is_sint64_lor : forall x:int, y:int [Cint.to_sint64 (Cint.lor x y)]. - Cint.is_sint64 x -> Cint.is_sint64 y -> ((Cint.to_sint64 (Cint.lor x - y)) = (Cint.lor x y)) - -lemma is_sint64_land : forall x:int, y:int [Cint.to_sint64 (Cint.land x y)]. - Cint.is_sint64 x -> Cint.is_sint64 y -> ((Cint.to_sint64 (Cint.land x - y)) = (Cint.land x y)) - -lemma is_sint64_lsr : forall x:int, y:int [Cint.to_sint64 (Cint.lsr x y)]. - (Int.(<=) (0) (y)) -> Cint.is_sint64 x -> ((Cint.to_sint64 (Cint.lsr x - y)) = (Cint.lsr x y)) - -lemma is_sint64_lsl1 : ((Cint.lsl 1 63) = (Cint.max_sint64)) - -lemma is_sint64_lsl1_inf : forall y:int [Cint.to_sint64 (Cint.lsl 1 y)]. - (Int.(<=) (0) (y)) /\ (Int.(<) (y) (63)) -> ((Cint.to_sint64 (Cint.lsl 1 - y)) = (Cint.lsl 1 y)) - -lemma is_sint64_lsl1_sup : forall y:int [Cint.to_sint64 (Cint.lsl 1 y)]. - (Int.(<=) (64) (y)) -> ((Cint.to_sint64 (Cint.lsl 1 y)) = (0)) - -lemma lor_addition : forall x:int, y:int [Cint.land x y, Cint.lor x y]. - ((Cint.land x y) = (0)) -> (((Int.(+) (x) (y))) = (Cint.lor x y)) - -lemma lxor_addition : forall x:int, y:int [Cint.land x y, Cint.lxor x y]. - ((Cint.land x y) = (0)) -> (((Int.(+) (x) (y))) = (Cint.lxor x y)) - -end diff --git a/src/plugins/wp/share/why3/Cfloat.why b/src/plugins/wp/share/why3/Cfloat.why deleted file mode 100644 index 8d17a607ed538c9f71c5d55e4ee54368dc25eda7..0000000000000000000000000000000000000000 --- a/src/plugins/wp/share/why3/Cfloat.why +++ /dev/null @@ -1,262 +0,0 @@ -(**************************************************************************) -(* *) -(* This file is part of WP plug-in of Frama-C. *) -(* *) -(* Copyright (C) 2007-2019 *) -(* 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). *) -(* *) -(**************************************************************************) - -theory Cfloat -use bool.Bool as Bool -use int.Int as Int -use real.Real as Real -use real.Abs as Abs -use real.FromInt as FromInt -use real.Square as Square - -type f32 - -type f64 - -function to_f32 real : f32 - -function of_f32 f32 : real - -function to_f64 real : f64 - -function of_f64 f64 : real - -axiom to_f32_zero : ((of_f32 (to_f32 0.0)) = (0.0)) - -axiom to_f32_one : ((of_f32 (to_f32 1.0)) = (1.0)) - -axiom to_f64_zero : ((of_f64 (to_f64 0.0)) = (0.0)) - -axiom to_f64_one : ((of_f64 (to_f64 1.0)) = (1.0)) - -type rounding_mode = - | Up - | Down - | ToZero - | NearestTiesToAway - | NearestTiesToEven - -function round_float rounding_mode real : f32 - -function round_double rounding_mode real : f64 - -axiom float_32 : forall x:real [round_float NearestTiesToEven x]. ((to_f32 - x) = (round_float NearestTiesToEven x)) - -axiom float_64 : forall x:real [round_double NearestTiesToEven x]. ((to_f64 - x) = (round_double NearestTiesToEven x)) - -type float_kind = - | Finite - | NaN - | Inf_pos - | Inf_neg - -function classify_f32 f32 : float_kind - -function classify_f64 f64 : float_kind - -predicate is_finite_f32 (f:f32) = ((classify_f32 f) = (Finite)) - -predicate is_finite_f64 (d:f64) = ((classify_f64 d) = (Finite)) - -predicate is_NaN_f32 (f:f32) = ((classify_f32 f) = (NaN)) - -predicate is_NaN_f64 (d:f64) = ((classify_f64 d) = (NaN)) - -predicate is_infinite_f32 (f:f32) = ((classify_f32 f) = (Inf_pos)) || ((classify_f32 f) = (Inf_neg)) - -predicate is_infinite_f64 (d:f64) = ((classify_f64 d) = (Inf_pos)) || ((classify_f64 d) = (Inf_neg)) - -predicate is_positive_infinite_f32 (f:f32) = ((classify_f32 f) = (Inf_pos)) - -predicate is_positive_infinite_f64 (d:f64) = ((classify_f64 d) = (Inf_pos)) - -predicate is_negative_infinite_f32 (f:f32) = ((classify_f32 f) = (Inf_neg)) - -predicate is_negative_infinite_f64 (d:f64) = ((classify_f64 d) = (Inf_neg)) - -axiom is_finite_to_float_32 : forall x:real [is_finite_f32 (to_f32 x)]. - is_finite_f32 (to_f32 x) - -axiom is_finite_to_float_64 : forall x:real [is_finite_f64 (to_f64 x)]. - is_finite_f64 (to_f64 x) - -axiom to_float_is_finite_32 : forall f:f32 [to_f32 (of_f32 f)| is_finite_f32 - f]. is_finite_f32 f -> ((to_f32 (of_f32 f)) = (f)) - -axiom to_float_is_finite_64 : forall d:f64 [to_f64 (of_f64 d)| is_finite_f64 - d]. is_finite_f64 d -> ((to_f64 (of_f64 d)) = (d)) - -predicate finite (x:real) = is_finite_f32 (to_f32 x) /\ is_finite_f64 (to_f64 - x) - -function max_f32 : real = 340282346600000016151267322115014000640.0 - -function max_f64 : real = - 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0 - -axiom finite_small_f32 : forall x:real. - (Real.(<=) ((Real.(-_) (max_f64))) (x)) /\ (Real.(<=) (x) (max_f32)) -> - is_finite_f32 (to_f32 x) - -axiom finite_small_f64 : forall x:real. - (Real.(<=) ((Real.(-_) (max_f64))) (x)) /\ (Real.(<=) (x) (max_f64)) -> - is_finite_f64 (to_f64 x) - -axiom finite_range_f32 : forall f:f32. is_finite_f32 f <-> - (Real.(<=) ((Real.(-_) (max_f32))) (of_f32 f)) /\ (Real.(<=) (of_f32 - f) (max_f32)) - -axiom finite_range_f64 : forall d:f64. is_finite_f64 d <-> - (Real.(<=) ((Real.(-_) (max_f64))) (of_f64 d)) /\ (Real.(<=) (of_f64 - d) (max_f64)) - -function eq_f32b f32 f32 : Bool.bool - -function eq_f64b f64 f64 : Bool.bool - -predicate eq_f32 (x:f32) (y:f32) = ((eq_f32b x y) = (Bool.True)) - -predicate eq_f64 (x:f64) (y:f64) = ((eq_f64b x y) = (Bool.True)) - -axiom eq_finite_f32 : forall x:f32, y:f32 [eq_f32 x y]. is_finite_f32 x -> - is_finite_f32 y -> eq_f32 x y <-> ((of_f32 x) = (of_f32 y)) - -axiom eq_finite_f64 : forall x:f64, y:f64 [eq_f64 x y]. is_finite_f64 x -> - is_finite_f64 y -> eq_f64 x y <-> ((of_f64 x) = (of_f64 y)) - -function ne_f32b f32 f32 : Bool.bool - -function ne_f64b f64 f64 : Bool.bool - -predicate ne_f32 (x:f32) (y:f32) = ((ne_f32b x y) = (Bool.True)) - -predicate ne_f64 (x:f64) (y:f64) = ((ne_f64b x y) = (Bool.True)) - -axiom ne_finite_f32 : forall x:f32, y:f32 [ne_f32 x y]. is_finite_f32 x -> - is_finite_f32 y -> ne_f32 x y <-> not ((of_f32 x) = (of_f32 y)) - -axiom ne_finite_f64 : forall x:f64, y:f64 [ne_f64 x y]. is_finite_f64 x -> - is_finite_f64 y -> ne_f64 x y <-> not ((of_f64 x) = (of_f64 y)) - -function le_f32b f32 f32 : Bool.bool - -function le_f64b f64 f64 : Bool.bool - -predicate le_f32 (x:f32) (y:f32) = ((le_f32b x y) = (Bool.True)) - -predicate le_f64 (x:f64) (y:f64) = ((le_f64b x y) = (Bool.True)) - -axiom le_finite_f32 : forall x:f32, y:f32 [le_f32 x y]. is_finite_f32 x -> - is_finite_f32 y -> le_f32 x y <-> (Real.(<=) (of_f32 x) (of_f32 y)) - -axiom le_finite_f64 : forall x:f64, y:f64 [le_f64 x y]. is_finite_f64 x -> - is_finite_f64 y -> le_f64 x y <-> (Real.(<=) (of_f64 x) (of_f64 y)) - -function lt_f32b f32 f32 : Bool.bool - -function lt_f64b f64 f64 : Bool.bool - -predicate lt_f32 (x:f32) (y:f32) = ((lt_f32b x y) = (Bool.True)) - -predicate lt_f64 (x:f64) (y:f64) = ((lt_f64b x y) = (Bool.True)) - -axiom lt_finite_f32 : forall x:f32, y:f32 [lt_f32 x y]. is_finite_f32 x -> - is_finite_f32 y -> lt_f32 x y <-> (Real.(<) (of_f32 x) (of_f32 y)) - -axiom lt_finite_f64 : forall x:f64, y:f64 [lt_f64 x y]. is_finite_f64 x -> - is_finite_f64 y -> lt_f64 x y <-> (Real.(<) (of_f64 x) (of_f64 y)) - -function neg_f32 f32 : f32 - -function neg_f64 f64 : f64 - -axiom neg_finite_f32 : forall x:f32 [neg_f32 x]. is_finite_f32 x -> ((of_f32 - (neg_f32 x)) = ((Real.(-_) (of_f32 x)))) - -axiom neg_finite_f64 : forall x:f64 [neg_f64 x]. is_finite_f64 x -> ((of_f64 - (neg_f64 x)) = ((Real.(-_) (of_f64 x)))) - -function add_f32 f32 f32 : f32 - -function add_f64 f64 f64 : f64 - -axiom add_finite_f32 : forall x:f32, y:f32 [add_f32 x y]. is_finite_f32 x -> - is_finite_f32 y -> ((add_f32 x y) = (to_f32 (Real.(+) (of_f32 x) (of_f32 - y)))) - -axiom add_finite_f64 : forall x:f64, y:f64 [add_f64 x y]. is_finite_f64 x -> - is_finite_f64 y -> ((add_f64 x y) = (to_f64 (Real.(+) (of_f64 x) (of_f64 - y)))) - -function mul_f32 f32 f32 : f32 - -function mul_f64 f64 f64 : f64 - -axiom mul_finite_f32 : forall x:f32, y:f32 [mul_f32 x y]. is_finite_f32 x -> - is_finite_f32 y -> ((mul_f32 x y) = (to_f32 (Real.(*) (of_f32 x) (of_f32 - y)))) - -axiom mul_finite_f64 : forall x:f64, y:f64 [mul_f64 x y]. is_finite_f64 x -> - is_finite_f64 y -> ((mul_f64 x y) = (to_f64 (Real.(*) (of_f64 x) (of_f64 - y)))) - -function div_f32 f32 f32 : f32 - -function div_f64 f64 f64 : f64 - -axiom div_finite_f32 : forall x:f32, y:f32 [div_f32 x y]. is_finite_f32 x -> - is_finite_f32 y -> ((div_f32 x y) = (to_f32 (Real.(/) (of_f32 x) (of_f32 - y)))) - -axiom div_finite_f64 : forall x:f64, y:f64 [div_f64 x y]. is_finite_f64 x -> - is_finite_f64 y -> ((div_f64 x y) = (to_f64 (Real.(/) (of_f64 x) (of_f64 - y)))) - -function sqrt_f32 f32 : f32 - -function sqrt_f64 f64 : f64 - -axiom sqrt_finite_f32 : forall x:f32 [sqrt_f32 x]. is_finite_f32 x -> - ((sqrt_f32 x) = (to_f32 (Square.sqrt (of_f32 x)))) - -axiom sqrt_finite_f64 : forall x:f64 [sqrt_f64 x]. is_finite_f64 x -> - ((sqrt_f64 x) = (to_f64 (Square.sqrt (of_f64 x)))) - -function model_f32 f32 : real - -function delta_f32 (f:f32) : real = Abs.abs (Real.(-) (of_f32 f) (model_f32 - f)) - -function error_f32 (f:f32) : real = (Real.(/) (delta_f32 f) (Abs.abs - (model_f32 f))) - -function model_f64 f64 : real - -function delta_f64 (f:f64) : real = Abs.abs (Real.(-) (of_f64 f) (model_f64 - f)) - -function error_f64 (f:f64) : real = (Real.(/) (delta_f64 f) (Abs.abs - (model_f64 f))) - -end diff --git a/src/plugins/wp/share/why3/Cint.why b/src/plugins/wp/share/why3/Cint.why deleted file mode 100644 index 0522aebf1c30162f2143e7310c6e85b12b71ce10..0000000000000000000000000000000000000000 --- a/src/plugins/wp/share/why3/Cint.why +++ /dev/null @@ -1,197 +0,0 @@ -(**************************************************************************) -(* *) -(* This file is part of WP plug-in of Frama-C. *) -(* *) -(* Copyright (C) 2007-2019 *) -(* 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). *) -(* *) -(**************************************************************************) - -theory Cint -use bool.Bool as Bool -use int.Int as Int - -function max_uint8 : int = 256 - -function max_sint8 : int = 128 - -function max_uint16 : int = 65536 - -function max_sint16 : int = 32768 - -function max_uint32 : int = 4294967296 - -function max_sint32 : int = 2147483648 - -function max_uint64 : int = 18446744073709551616 - -function max_sint64 : int = 9223372036854775808 - -predicate is_bool (x:int) = ((x) = (0)) \/ ((x) = (1)) - -predicate is_uint8 int - -axiom is_uint8_def : forall x:int [is_uint8 x]. is_uint8 x <-> - (Int.(<=) (0) (x)) /\ (Int.(<) (x) (max_uint8)) - -predicate is_sint8 int - -axiom is_sint8_def : forall x:int [is_sint8 x]. is_sint8 x <-> - (Int.(<=) ((Int.(-_) (max_sint8))) (x)) /\ (Int.(<) (x) (max_sint8)) - -predicate is_uint16 int - -axiom is_uint16_def : forall x:int [is_uint16 x]. is_uint16 x <-> - (Int.(<=) (0) (x)) /\ (Int.(<) (x) (max_uint16)) - -predicate is_sint16 (x:int) = (Int.(<=) ((Int.(-_) (max_sint16))) (x)) /\ - (Int.(<) (x) (max_sint16)) - -predicate is_uint32 int - -axiom is_uint32_def : forall x:int [is_uint32 x]. is_uint32 x <-> - (Int.(<=) (0) (x)) /\ (Int.(<) (x) (max_uint32)) - -predicate is_sint32 int - -axiom is_sint32_def : forall x:int [is_sint32 x]. is_sint32 x <-> - (Int.(<=) ((Int.(-_) (max_sint32))) (x)) /\ (Int.(<) (x) (max_sint32)) - -predicate is_uint64 int - -axiom is_uint64_def : forall x:int [is_uint64 x]. is_uint64 x <-> - (Int.(<=) (0) (x)) /\ (Int.(<) (x) (max_uint64)) - -predicate is_sint64 int - -axiom is_sint64_def : forall x:int [is_sint64 x]. is_sint64 x <-> - (Int.(<=) ((Int.(-_) (max_sint64))) (x)) /\ (Int.(<) (x) (max_sint64)) - -lemma is_bool0 : is_bool 0 - -lemma is_bool1 : is_bool 1 - -function to_bool (x:int) : int = if ((x) = (0)) then 0 else 1 - -function to_uint8 int : int - -function to_sint8 int : int - -function to_uint16 int : int - -function to_sint16 int : int - -function to_uint32 int : int - -function to_sint32 int : int - -function to_uint64 int : int - -function to_sint64 int : int - -function two_power_abs int : int - -predicate is_uint (n:int) (x:int) = (Int.(<=) (0) (x)) /\ - (Int.(<) (x) (two_power_abs n)) - -predicate is_sint (n:int) (x:int) = (Int.(<=) ((Int.(-_) (two_power_abs - n))) (x)) /\ (Int.(<) (x) (two_power_abs n)) - -function to_uint int int : int - -function 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]. (Int.(<=) (0) (x)) /\ - (Int.(<) (x) (max_uint8)) -> ((to_uint8 x) = (x)) - -axiom id_sint8 : forall x:int [to_sint8 x]. - (Int.(<=) ((Int.(-_) (max_sint8))) (x)) /\ (Int.(<) (x) (max_sint8)) -> - ((to_sint8 x) = (x)) - -axiom id_uint16 : forall x:int [to_uint16 x]. (Int.(<=) (0) (x)) /\ - (Int.(<) (x) (max_uint16)) -> ((to_uint16 x) = (x)) - -axiom id_sint16 : forall x:int [to_sint16 x]. - (Int.(<=) ((Int.(-_) (max_sint16))) (x)) /\ (Int.(<) (x) (max_sint16)) -> - ((to_sint16 x) = (x)) - -axiom id_uint32 : forall x:int [to_uint32 x]. (Int.(<=) (0) (x)) /\ - (Int.(<) (x) (max_uint32)) -> ((to_uint32 x) = (x)) - -axiom id_sint32 : forall x:int [to_sint32 x]. - (Int.(<=) ((Int.(-_) (max_sint32))) (x)) /\ (Int.(<) (x) (max_sint32)) -> - ((to_sint32 x) = (x)) - -axiom id_uint64 : forall x:int [to_uint64 x]. (Int.(<=) (0) (x)) /\ - (Int.(<) (x) (max_uint64)) -> ((to_uint64 x) = (x)) - -axiom id_sint64 : forall x:int [to_sint64 x]. - (Int.(<=) ((Int.(-_) (max_sint64))) (x)) /\ (Int.(<) (x) (max_sint64)) -> - ((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)) - -function lnot int : int - -function land int int : int - -function lxor int int : int - -function lor int int : int - -function lsl int int : int - -function lsr int int : int - -function bit_testb int int : Bool.bool - -predicate bit_test int int - -end diff --git a/src/plugins/wp/share/why3/Memory.why b/src/plugins/wp/share/why3/Memory.why deleted file mode 100644 index 8496fc9cc19ebb20e7828dae1df523a33e4cbb1a..0000000000000000000000000000000000000000 --- a/src/plugins/wp/share/why3/Memory.why +++ /dev/null @@ -1,157 +0,0 @@ -(**************************************************************************) -(* *) -(* This file is part of WP plug-in of Frama-C. *) -(* *) -(* Copyright (C) 2007-2019 *) -(* 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). *) -(* *) -(**************************************************************************) - -theory Memory -use bool.Bool as Bool -use int.Int as Int -use map.Map as Map - -type addr = - | Mk_addr (base:int) (offset:int) - -predicate addr_le addr addr - -predicate addr_lt addr addr - -function addr_le_bool addr addr : Bool.bool - -function addr_lt_bool addr addr : Bool.bool - -axiom addr_le_def : forall p:addr, q:addr [addr_le p q]. ((base p) = (base - q)) -> addr_le p q <-> (Int.(<=) (offset p) (offset q)) - -axiom addr_lt_def : forall p:addr, q:addr [addr_lt p q]. ((base p) = (base - q)) -> addr_lt p q <-> (Int.(<) (offset p) (offset q)) - -axiom addr_le_bool_def : forall p:addr, q:addr [addr_le_bool p q]. addr_le p - q <-> ((addr_le_bool p q) = (Bool.True)) - -axiom addr_lt_bool_def : forall p:addr, q:addr [addr_lt_bool p q]. addr_lt p - q <-> ((addr_lt_bool p q) = (Bool.True)) - -function null : addr = Mk_addr 0 0 - -function global (b:int) : addr = Mk_addr b 0 - -function shift (p:addr) (k:int) : addr = Mk_addr (base p) (Int.(+) (offset - p) (k)) - -predicate included (p:addr) (a:int) (q:addr) (b:int) = (Int.(>) (a) (0)) -> - (Int.(>=) (b) (0)) /\ ((base p) = (base q)) /\ (Int.(<=) (offset q) (offset - p)) /\ (Int.(<=) ((Int.(+) (offset p) (a))) ((Int.(+) (offset q) (b)))) - -predicate separated (p:addr) (a:int) (q:addr) (b:int) = (Int.(<=) (a) (0)) \/ - (Int.(<=) (b) (0)) \/ not ((base p) = (base q)) \/ - (Int.(<=) ((Int.(+) (offset q) (b))) (offset p)) \/ - (Int.(<=) ((Int.(+) (offset p) (a))) (offset q)) - -predicate eqmem (m1:Map.map addr 'a) (m2:Map.map addr 'a) (p:addr) (a:int) = - forall q:addr [(Map.([]) (m1) (p))| (Map.([]) (m2) (q))]. included q 1 p - a -> (((Map.([]) (m1) (q))) = ((Map.([]) (m2) (q)))) - -function havoc (Map.map addr 'a) (Map.map addr 'a) addr int : Map.map addr 'a - -predicate valid_rw (m:Map.map int int) (p:addr) (n:int) = - (Int.(>) (n) (0)) -> (Int.(<) (0) (base p)) /\ (Int.(<=) (0) (offset p)) /\ - (Int.(<=) ((Int.(+) (offset p) (n))) ((Map.([]) (m) (base p)))) - -predicate valid_rd (m:Map.map int int) (p:addr) (n:int) = - (Int.(>) (n) (0)) -> not ((0) = (base p)) /\ (Int.(<=) (0) (offset p)) /\ - (Int.(<=) ((Int.(+) (offset p) (n))) ((Map.([]) (m) (base p)))) - -predicate invalid (m:Map.map int int) (p:addr) (n:int) = (Int.(>) (n) (0)) -> - (Int.(<=) ((Map.([]) (m) (base p))) (offset p)) \/ - (Int.(<=) ((Int.(+) (offset p) (n))) (0)) - -lemma valid_rw_rd : forall m:Map.map int int. forall p:addr. forall n:int. - valid_rw m p n -> valid_rd m p n - -lemma valid_string : forall m:Map.map int int. forall p:addr. (Int.(<) (base - p) (0)) -> (Int.(<=) (0) (offset p)) /\ (Int.(<) (offset - p) ((Map.([]) (m) (base p)))) -> valid_rd m p 1 /\ not valid_rw m p 1 - -lemma separated_1 : forall p:addr, q:addr. forall a:int, b:int, i:int, j:int - [separated p a q b, Mk_addr (base p) i, Mk_addr (base q) j]. separated p a - q b -> (Int.(<=) (offset p) (i)) /\ (Int.(<) (i) ((Int.(+) (offset - p) (a)))) -> (Int.(<=) (offset q) (j)) /\ (Int.(<) (j) ((Int.(+) (offset - q) (b)))) -> not ((Mk_addr (base p) i) = (Mk_addr (base q) j)) - -function region int : int - -predicate linked (Map.map int int) - -predicate sconst (Map.map addr int) - -predicate framed (m:Map.map addr addr) = forall p:addr [(Map.([]) (m) (p))]. - (Int.(<=) (region (base (Map.([]) (m) (p)))) (0)) - -lemma separated_included : forall p:addr, q:addr. forall a:int, b:int - [separated p a q b, included p a q b]. (Int.(>) (a) (0)) -> - (Int.(>) (b) (0)) -> separated p a q b -> included p a q b -> false - -lemma included_trans : forall p:addr, q:addr, r:addr. forall a:int, b:int, c: - int [included p a q b, included q b r c]. included p a q b -> included q b - r c -> included p a r c - -lemma separated_trans : forall p:addr, q:addr, r:addr. forall a:int, b:int, - c:int [included p a q b, separated q b r c]. included p a q b -> separated - q b r c -> separated p a r c - -lemma separated_sym : forall p:addr, q:addr. forall a:int, b:int [separated p - a q b]. separated p a q b <-> separated q b p a - -lemma eqmem_included : forall m1:Map.map addr 'a, m2:Map.map addr 'a. - forall p:addr, q:addr. forall a:int, b:int [eqmem m1 m2 p a, eqmem m1 m2 q - b]. included p a q b -> eqmem m1 m2 q b -> eqmem m1 m2 p a - -lemma eqmem_sym : forall m1:Map.map addr 'a, m2:Map.map addr 'a. forall p: - addr. forall a:int. eqmem m1 m2 p a -> eqmem m2 m1 p a - -lemma havoc_access : forall m0:Map.map addr 'a, m1:Map.map addr 'a. forall q: - addr, p:addr. forall a:int. (((Map.([]) (havoc m0 m1 p - a) (q))) = (if separated q 1 p a then (Map.([]) (m1) (q)) - else (Map.([]) (m0) (q)))) - -function int_of_addr addr : int - -function addr_of_int int : addr - -function base_offset int : int - -function base_index int : int - -lemma int_of_addr_bijection : forall a:int. ((int_of_addr (addr_of_int - a)) = (a)) - -lemma addr_of_int_bijection : forall p:addr. ((addr_of_int (int_of_addr - p)) = (p)) - -lemma addr_of_null : ((int_of_addr null) = (0)) - -lemma base_offset_zero : ((base_offset 0) = (0)) - -lemma base_offset_inj : forall i:int. ((base_index (base_offset i)) = (i)) - -lemma base_offset_monotonic : forall i:int, j:int. (Int.(<) (i) (j)) -> - (Int.(<) (base_offset i) (base_offset j)) - -end diff --git a/src/plugins/wp/share/why3/Qed.why b/src/plugins/wp/share/why3/Qed.why deleted file mode 100644 index 6e1692ec952d9c5dc9dd1b47d806098e66c136e1..0000000000000000000000000000000000000000 --- a/src/plugins/wp/share/why3/Qed.why +++ /dev/null @@ -1,107 +0,0 @@ -(**************************************************************************) -(* *) -(* This file is part of WP plug-in of Frama-C. *) -(* *) -(* Copyright (C) 2007-2019 *) -(* 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). *) -(* *) -(**************************************************************************) - -theory Qed -use bool.Bool as Bool -use int.Int as Int -use int.Abs as Abs -use int.ComputerDivision as ComputerDivision -use real.Real as Real -use real.FromInt as FromInt - -function match_bool Bool.bool 'a 'a : 'a - -function eqb 'a 'a : Bool.bool - -axiom eqb1 : forall x:'a, y:'a. ((eqb x y) = (Bool.True)) <-> ((x) = (y)) - -function neqb 'a 'a : Bool.bool - -axiom neqb1 : forall x:'a, y:'a. ((neqb x y) = (Bool.True)) <-> - not ((x) = (y)) - -function zlt int int : Bool.bool - -function zleq int int : Bool.bool - -axiom zlt1 : forall x:int, y:int. ((zlt x y) = (Bool.True)) <-> - (Int.(<) (x) (y)) - -axiom zleq1 : forall x:int, y:int. ((zleq x y) = (Bool.True)) <-> - (Int.(<=) (x) (y)) - -function rlt real real : Bool.bool - -function rleq real real : Bool.bool - -axiom rlt1 : forall x:real, y:real. ((rlt x y) = (Bool.True)) <-> - (Real.(<) (x) (y)) - -axiom rleq1 : forall x:real, y:real. ((rleq x y) = (Bool.True)) <-> - (Real.(<=) (x) (y)) - -function real_of_int (x:int) : real = FromInt.from_int x - -lemma c_euclidian : forall n:int, d:int [ComputerDivision.div n d, - ComputerDivision.mod n d]. not ((d) = (0)) -> - ((n) = ((Int.(+) ((Int.(*) (ComputerDivision.div n - d) (d))) (ComputerDivision.mod n d)))) - -lemma cdiv_cases : forall n:int, d:int [ComputerDivision.div n d]. - ((Int.(>=) (n) (0)) -> (Int.(>) (d) (0)) -> ((ComputerDivision.div n - d) = ((ComputerDivision.div n d)))) /\ ((Int.(<=) (n) (0)) -> - (Int.(>) (d) (0)) -> ((ComputerDivision.div n - d) = ((Int.(-_) ((ComputerDivision.div (Int.(-_) (n)) d)))))) /\ - ((Int.(>=) (n) (0)) -> (Int.(<) (d) (0)) -> ((ComputerDivision.div n - d) = ((Int.(-_) ((ComputerDivision.div n (Int.(-_) (d)))))))) /\ - ((Int.(<=) (n) (0)) -> (Int.(<) (d) (0)) -> ((ComputerDivision.div n - d) = ((ComputerDivision.div (Int.(-_) (n)) (Int.(-_) (d)))))) - -lemma cmod_cases : forall n:int, d:int [ComputerDivision.mod n d]. - ((Int.(>=) (n) (0)) -> (Int.(>) (d) (0)) -> ((ComputerDivision.mod n - d) = ((ComputerDivision.mod n d)))) /\ ((Int.(<=) (n) (0)) -> - (Int.(>) (d) (0)) -> ((ComputerDivision.mod n - d) = ((Int.(-_) ((ComputerDivision.mod (Int.(-_) (n)) d)))))) /\ - ((Int.(>=) (n) (0)) -> (Int.(<) (d) (0)) -> ((ComputerDivision.mod n - d) = ((ComputerDivision.mod n (Int.(-_) (d)))))) /\ ((Int.(<=) (n) (0)) -> - (Int.(<) (d) (0)) -> ((ComputerDivision.mod n - d) = ((Int.(-_) ((ComputerDivision.mod (Int.(-_) (n)) (Int.(-_) (d)))))))) - -lemma cmod_remainder : forall n:int, d:int [ComputerDivision.mod n d]. - ((Int.(>=) (n) (0)) -> (Int.(>) (d) (0)) -> - (Int.(<=) (0) (ComputerDivision.mod n d)) /\ (Int.(<) (ComputerDivision.mod - n d) (d))) /\ ((Int.(<=) (n) (0)) -> (Int.(>) (d) (0)) -> - (Int.(<) ((Int.(-_) (d))) (ComputerDivision.mod n d)) /\ - (Int.(<=) (ComputerDivision.mod n d) (0))) /\ ((Int.(>=) (n) (0)) -> - (Int.(<) (d) (0)) -> (Int.(<=) (0) (ComputerDivision.mod n d)) /\ - (Int.(<) (ComputerDivision.mod n d) ((Int.(-_) (d))))) /\ - ((Int.(<=) (n) (0)) -> (Int.(<) (d) (0)) -> - (Int.(<) (d) (ComputerDivision.mod n d)) /\ (Int.(<=) (ComputerDivision.mod - n d) (0))) - -lemma cdiv_neutral : forall a:int [ComputerDivision.div a 1]. - ((ComputerDivision.div a 1) = (a)) - -lemma cdiv_inv : forall a:int [ComputerDivision.div a a]. not ((a) = (0)) -> - ((ComputerDivision.div a a) = (1)) - -end diff --git a/src/plugins/wp/share/why3/Vlist.why b/src/plugins/wp/share/why3/Vlist.why deleted file mode 100644 index df55f756bbdc96150fdf5f54896ce5e0efc33a75..0000000000000000000000000000000000000000 --- a/src/plugins/wp/share/why3/Vlist.why +++ /dev/null @@ -1,105 +0,0 @@ -(**************************************************************************) -(* *) -(* This file is part of WP plug-in of Frama-C. *) -(* *) -(* Copyright (C) 2007-2019 *) -(* 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). *) -(* *) -(**************************************************************************) - -theory Vlist -use int.Int as Int -use int.Abs as Abs -use int.ComputerDivision as ComputerDivision - -type list 'a - -function nil : list 'a - -function cons 'a (list 'a) : list 'a - -function concat (list 'a) (list 'a) : list 'a - -function repeat (list 'a) int : list 'a - -function length (list 'a) : int - -function nth (list 'a) int : 'a - -axiom length_pos : forall w:list 'a. (Int.(<=) (0) (length w)) - -axiom length_nil : ((length (nil:list 'a)) = (0)) - -axiom length_nil_bis : forall w:list 'a. ((length w) = (0)) -> - ((w) = (nil:list 'a)) - -axiom length_cons : forall x:'a, w:list 'a [length (cons x w)]. ((length - (cons x w)) = ((Int.(+) (1) (length w)))) - -axiom length_concat : forall u:list 'a, v:list 'a [length (concat u v)]. - ((length (concat u v)) = ((Int.(+) (length u) (length v)))) - -axiom length_repeat : forall w:list 'a, n:int [length (repeat w n)]. - (Int.(<=) (0) (n)) -> ((length (repeat w n)) = ((Int.(*) (n) (length w)))) - -axiom nth_cons : forall k:int, x:'a, w:list 'a [nth (cons x w) k]. ((nth - (cons x w) k) = (if ((k) = (0)) then x else nth w (Int.(-) (k) (1)))) - -axiom nth_concat : forall u:list 'a, v:list 'a, k:int [nth (concat u v) k]. - ((nth (concat u v) k) = (if (Int.(<) (k) (length u)) then nth u k else nth - v (Int.(-) (k) (length u)))) - -axiom nth_repeat : forall n:int, k:int, w:list 'a [nth (repeat w n) k]. - (Int.(<=) (0) (k)) /\ (Int.(<) (k) ((Int.(*) (n) (length w)))) -> - (Int.(<) (0) (length w)) -> ((nth (repeat w n) k) = (nth w - (ComputerDivision.mod k (length w)))) - -predicate vlist_eq (u:list 'a) (v:list 'a) = ((length - u) = (length v)) && (forall i:int. (Int.(<=) (0) (i)) /\ - (Int.(<) (i) (length u)) -> ((nth u i) = (nth v i))) - -axiom extensionality : forall u:list 'a, v:list 'a. vlist_eq u v -> - ((u) = (v)) - -axiom rw_nil_concat_left : forall w:list 'a [concat (nil:list 'a) w]. - ((concat (nil:list 'a) w) = (w)) - -axiom rw_nil_concat_right : forall w:list 'a [concat w (nil:list 'a)]. - ((concat w (nil:list 'a)) = (w)) - -axiom rw_nil_repeat : forall n:int [repeat (nil:list 'a) n]. - (Int.(>=) (n) (0)) -> ((repeat (nil:list 'a) n) = (nil:list 'a)) - -axiom rw_repeat_zero : forall w:list 'a [repeat w 0]. ((repeat w - 0) = (nil:list 'a)) - -axiom rw_repeat_one : forall w:list 'a [repeat w 1]. ((repeat w 1) = (w)) - -function repeat_box (list 'a) int : list 'a - -axiom rw_repeat_box_unfold : forall w:list 'a, n:int [repeat_box w n]. - ((repeat_box w n) = (repeat w n)) - -axiom rw_repeat_plus_box_unfold : forall w:list 'a, a:int, b:int [repeat_box - w (Int.(+) (a) (b))]. (Int.(<=) (0) (a)) -> (Int.(<=) (0) (b)) -> - ((repeat_box w (Int.(+) (a) (b))) = (concat (repeat w a) (repeat w b))) - -axiom rw_repeat_plus_one_box_unfold : forall w:list 'a, n:int [repeat_box w - n]. (Int.(<) (0) (n)) -> ((repeat_box w n) = (concat (repeat - w (Int.(-) (n) (1))) w)) && ((repeat_box w (Int.(+) (n) (1))) = (concat - (repeat w n) w)) - -end diff --git a/src/plugins/wp/share/why3/Vset.why b/src/plugins/wp/share/why3/Vset.why deleted file mode 100644 index d0664f99585e45b7cbd6640c465bf25b120aabf4..0000000000000000000000000000000000000000 --- a/src/plugins/wp/share/why3/Vset.why +++ /dev/null @@ -1,94 +0,0 @@ -(**************************************************************************) -(* *) -(* This file is part of WP plug-in of Frama-C. *) -(* *) -(* Copyright (C) 2007-2019 *) -(* 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). *) -(* *) -(**************************************************************************) - -theory Vset -use bool.Bool as Bool -use int.Int as Int - -type set 'a - -function empty : set 'a - -function singleton 'a : set 'a - -function union (set 'a) (set 'a) : set 'a - -function inter (set 'a) (set 'a) : set 'a - -predicate member 'a (set 'a) - -function member_bool 'a (set 'a) : Bool.bool - -function range int int : set int - -function range_sup int : set int - -function range_inf int : set int - -function range_all : set int - -predicate eqset (a:set 'a) (b:set 'a) = forall x:'a. member x a <-> member x - b - -predicate subset (a:set 'a) (b:set 'a) = forall x:'a. member x a -> member x - b - -predicate disjoint (a:set 'a) (b:set 'a) = forall x:'a. member x a -> member - x b -> false - -axiom member_bool1 : forall x:'a. forall s:set 'a [member_bool x s]. - if member x s then ((member_bool x s) = (Bool.True)) else ((member_bool x - s) = (Bool.False)) - -axiom member_empty : forall x:'a [member x (empty:set 'a)]. not member x - (empty:set 'a) - -axiom member_singleton : forall x:'a, y:'a [member x (singleton y)]. member x - (singleton y) <-> ((x) = (y)) - -axiom member_union : forall x:'a. forall a:set 'a, b:set 'a [member x (union - a b)]. member x (union a b) <-> member x a \/ member x b - -axiom member_inter : forall x:'a. forall a:set 'a, b:set 'a [member x (inter - a b)]. member x (inter a b) <-> member x a /\ member x b - -axiom union_empty : forall a:set 'a [union a (empty:set 'a)| union (empty:set - 'a) a]. ((union a (empty:set 'a)) = (a)) /\ ((union (empty:set 'a) - a) = (a)) - -axiom inter_empty : forall a:set 'a [inter a (empty:set 'a)| inter (empty:set - 'a) a]. ((inter a (empty:set 'a)) = (empty:set 'a)) /\ ((inter (empty:set - 'a) a) = (empty:set 'a)) - -axiom member_range : forall x:int, a:int, b:int [member x (range a b)]. - member x (range a b) <-> (Int.(<=) (a) (x)) /\ (Int.(<=) (x) (b)) - -axiom member_range_sup : forall x:int, a:int [member x (range_sup a)]. member - x (range_sup a) <-> (Int.(<=) (a) (x)) - -axiom member_range_inf : forall x:int, b:int [member x (range_inf b)]. member - x (range_inf b) <-> (Int.(<=) (x) (b)) - -axiom member_range_all : forall x:int [member x range_all]. member x - range_all - -end