From ce9becf01ce4a5a34e1bf143d6fc4a068ff9cdd5 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 7 Jan 2022 14:06:21 +0100
Subject: [PATCH] [wp] Removed alt-ergo libs
---
headers/header_spec.txt | 31 -
src/plugins/wp/share/ergo/ArcTrigo.mlw | 40 --
src/plugins/wp/share/ergo/Cbits.mlw | 553 ------------------
src/plugins/wp/share/ergo/Cfloat.mlw | 360 ------------
src/plugins/wp/share/ergo/Cint.mlw | 224 -------
src/plugins/wp/share/ergo/Cmath.mlw | 34 --
src/plugins/wp/share/ergo/ExpLog.mlw | 30 -
src/plugins/wp/share/ergo/Memory.mlw | 212 -------
src/plugins/wp/share/ergo/Qed.mlw | 158 -----
src/plugins/wp/share/ergo/Square.mlw | 37 --
src/plugins/wp/share/ergo/Vlist.mlw | 126 ----
src/plugins/wp/share/ergo/Vset.mlw | 152 -----
src/plugins/wp/share/ergo/bool.Bool.mlw | 27 -
src/plugins/wp/share/ergo/int.Abs.mlw | 35 --
.../wp/share/ergo/int.ComputerDivision.mlw | 49 --
.../ergo/int.ComputerOfEuclideanDivision.mlw | 52 --
src/plugins/wp/share/ergo/int.Int.mlw | 18 -
src/plugins/wp/share/ergo/int.MinMax.mlw | 52 --
src/plugins/wp/share/ergo/map.Const.mlw | 23 -
src/plugins/wp/share/ergo/map.Map.mlw | 17 -
src/plugins/wp/share/ergo/real.Abs.mlw | 48 --
src/plugins/wp/share/ergo/real.ExpLog.mlw | 41 --
src/plugins/wp/share/ergo/real.FromInt.mlw | 45 --
src/plugins/wp/share/ergo/real.Hyperbolic.mlw | 40 --
src/plugins/wp/share/ergo/real.MinMax.mlw | 54 --
src/plugins/wp/share/ergo/real.Polar.mlw | 31 -
src/plugins/wp/share/ergo/real.PowerReal.mlw | 50 --
src/plugins/wp/share/ergo/real.Real.mlw | 42 --
src/plugins/wp/share/ergo/real.RealInfix.mlw | 18 -
src/plugins/wp/share/ergo/real.Square.mlw | 36 --
.../wp/share/ergo/real.Trigonometry.mlw | 75 ---
src/plugins/wp/share/ergo/real.Truncate.mlw | 73 ---
32 files changed, 2783 deletions(-)
delete mode 100644 src/plugins/wp/share/ergo/ArcTrigo.mlw
delete mode 100644 src/plugins/wp/share/ergo/Cbits.mlw
delete mode 100644 src/plugins/wp/share/ergo/Cfloat.mlw
delete mode 100644 src/plugins/wp/share/ergo/Cint.mlw
delete mode 100644 src/plugins/wp/share/ergo/Cmath.mlw
delete mode 100644 src/plugins/wp/share/ergo/ExpLog.mlw
delete mode 100644 src/plugins/wp/share/ergo/Memory.mlw
delete mode 100644 src/plugins/wp/share/ergo/Qed.mlw
delete mode 100644 src/plugins/wp/share/ergo/Square.mlw
delete mode 100644 src/plugins/wp/share/ergo/Vlist.mlw
delete mode 100644 src/plugins/wp/share/ergo/Vset.mlw
delete mode 100644 src/plugins/wp/share/ergo/bool.Bool.mlw
delete mode 100644 src/plugins/wp/share/ergo/int.Abs.mlw
delete mode 100644 src/plugins/wp/share/ergo/int.ComputerDivision.mlw
delete mode 100644 src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw
delete mode 100644 src/plugins/wp/share/ergo/int.Int.mlw
delete mode 100644 src/plugins/wp/share/ergo/int.MinMax.mlw
delete mode 100644 src/plugins/wp/share/ergo/map.Const.mlw
delete mode 100644 src/plugins/wp/share/ergo/map.Map.mlw
delete mode 100644 src/plugins/wp/share/ergo/real.Abs.mlw
delete mode 100644 src/plugins/wp/share/ergo/real.ExpLog.mlw
delete mode 100644 src/plugins/wp/share/ergo/real.FromInt.mlw
delete mode 100644 src/plugins/wp/share/ergo/real.Hyperbolic.mlw
delete mode 100644 src/plugins/wp/share/ergo/real.MinMax.mlw
delete mode 100644 src/plugins/wp/share/ergo/real.Polar.mlw
delete mode 100644 src/plugins/wp/share/ergo/real.PowerReal.mlw
delete mode 100644 src/plugins/wp/share/ergo/real.Real.mlw
delete mode 100644 src/plugins/wp/share/ergo/real.RealInfix.mlw
delete mode 100644 src/plugins/wp/share/ergo/real.Square.mlw
delete mode 100644 src/plugins/wp/share/ergo/real.Trigonometry.mlw
delete mode 100644 src/plugins/wp/share/ergo/real.Truncate.mlw
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index f4889824536..a283b5ab581 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1898,37 +1898,6 @@ src/plugins/wp/share/coqwp/real/Real.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/real/RealInfix.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/real/Square.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/real/Trigonometry.v: UNMODIFIED_WHY3
-src/plugins/wp/share/ergo/ArcTrigo.mlw: CEA_WP
-src/plugins/wp/share/ergo/Cbits.mlw: CEA_WP
-src/plugins/wp/share/ergo/Cfloat.mlw: CEA_WP
-src/plugins/wp/share/ergo/Cint.mlw: CEA_WP
-src/plugins/wp/share/ergo/Cmath.mlw: CEA_WP
-src/plugins/wp/share/ergo/ExpLog.mlw: CEA_WP
-src/plugins/wp/share/ergo/Memory.mlw: CEA_WP
-src/plugins/wp/share/ergo/Qed.mlw: CEA_WP
-src/plugins/wp/share/ergo/Square.mlw: CEA_WP
-src/plugins/wp/share/ergo/Vlist.mlw: CEA_WP
-src/plugins/wp/share/ergo/Vset.mlw: CEA_WP
-src/plugins/wp/share/ergo/bool.Bool.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/int.Abs.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/int.ComputerDivision.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/int.Int.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/int.MinMax.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/map.Map.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/map.Const.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/real.Abs.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/real.ExpLog.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/real.Hyperbolic.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/real.FromInt.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/real.MinMax.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/real.Polar.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/real.PowerReal.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/real.Real.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/real.RealInfix.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/real.Square.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/real.Trigonometry.mlw: MODIFIED_WHY3
-src/plugins/wp/share/ergo/real.Truncate.mlw: MODIFIED_WHY3
src/plugins/wp/share/install.ml: CEA_WP
src/plugins/wp/share/why3/frama_c_wp/cbits.mlw: CEA_WP
src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw: CEA_WP
diff --git a/src/plugins/wp/share/ergo/ArcTrigo.mlw b/src/plugins/wp/share/ergo/ArcTrigo.mlw
deleted file mode 100644
index e2640273c38..00000000000
--- a/src/plugins/wp/share/ergo/ArcTrigo.mlw
+++ /dev/null
@@ -1,40 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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 theory real_RealInfix_ must be appended to this file*)
-(** The theory real_Abs_ must be appended to this file*)
-(** The theory real_Square_ must be appended to this file*)
-(** The theory real_Trigonometry_ must be appended to this file*)
-logic asin : real -> real
-
-logic acos : real -> real
-
-axiom Sin_asin :
- (forall x:real. ((((-1.0) <= x) and (x <= 1.0)) -> (sin(asin(x)) = x)))
-
-axiom Cos_acos :
- (forall x:real. ((((-1.0) <= x) and (x <= 1.0)) -> (cos(acos(x)) = x)))
-
diff --git a/src/plugins/wp/share/ergo/Cbits.mlw b/src/plugins/wp/share/ergo/Cbits.mlw
deleted file mode 100644
index fc3e1ca738f..00000000000
--- a/src/plugins/wp/share/ergo/Cbits.mlw
+++ /dev/null
@@ -1,553 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** The theory BuiltIn_ must be appended to this file*)
-(** The theory Bool_ must be appended to this file*)
-(** The theory Qed_ 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*)
-(** The theory Cint_ must be appended to this file*)
-
-logic bit_testb : int, int -> bool
-
-logic bit_test : int, int -> prop
-
-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
-
-axiom lnot_bool : (lnot(0) = (-1))
-
-axiom lnot_bool1 : (lnot((-1)) = 0)
-
-axiom land_idemp : (forall x:int [land(x, x)]. (land(x, x) = x))
-
-axiom land_0 : (forall x:int [land(0, x)]. (land(0, x) = 0))
-
-axiom land_0bis : (forall x:int [land(x, 0)]. (land(x, 0) = 0))
-
-axiom land_1 : (forall x:int [land((-1), x)]. (land((-1), x) = x))
-
-axiom land_1bis : (forall x:int [land(x, (-1))]. (land(x, (-1)) = x))
-
-axiom lor_idemp : (forall x:int [lor(x, x)]. (lor(x, x) = x))
-
-axiom lor_1 : (forall x:int [lor((-1), x)]. (lor((-1), x) = (-1)))
-
-axiom lor_1bis : (forall x:int [lor(x, (-1))]. (lor(x, (-1)) = (-1)))
-
-axiom lor_0 : (forall x:int [lor(0, x)]. (lor(0, x) = x))
-
-axiom lor_0bis : (forall x:int [lor(x, 0)]. (lor(x, 0) = x))
-
-axiom lxor_nilpotent : (forall x:int [lxor(x, x)]. (lxor(x, x) = 0))
-
-axiom lxor_1 : (forall x:int [lxor((-1), x)]. (lxor((-1), x) = lnot(x)))
-
-axiom lxor_1bis : (forall x:int [lxor(x, (-1))]. (lxor(x, (-1)) = lnot(x)))
-
-axiom lxor_0 : (forall x:int [lxor(0, x)]. (lxor(0, x) = x))
-
-axiom lxor_0bis : (forall x:int [lxor(x, 0)]. (lxor(x, 0) = x))
-
-axiom lsl_0 : (forall x:int. (lsl(x, 0) = x))
-
-axiom lsl_1 : (forall x:int. (lsl(x, 1) = (2 * x)))
-
-axiom lsl_add :
- (forall x:int. forall p:int. forall q:int. ((0 <= p) -> ((0 <= q) ->
- (lsl(lsl(x, p), q) = lsl(x, (p + q))))))
-
-axiom lsr_0 : (forall x:int. (lsr(x, 0) = x))
-
-axiom lsr_1 : (forall x:int. ((0 <= x) -> (lsr(x, 1) = div(x,2))))
-
-axiom lsr_add :
- (forall x:int. forall p:int. forall q:int. ((0 <= p) -> ((0 <= q) ->
- (lsr(lsr(x, p), q) = lsr(x, (p + q))))))
-
-axiom lsl_lsr_add :
- (forall x:int. forall p:int. forall q:int. (((0 <= q) and (q <= p)) ->
- (lsr(lsl(x, p), q) = lsl(x, (p - q)))))
-
-axiom bit_test_def :
- (forall x:int. forall k:int [bit_testb(x, k)]. ((bit_testb(x, k) = true) ->
- bit_test(x, k)))
-
-axiom bit_test_def1 :
- (forall x:int. forall k:int [bit_testb(x, k)]. (bit_test(x, k) ->
- (bit_testb(x, k) = true)))
-
-axiom bit_test_extraction :
- (forall x:int. forall k:int [land(x, lsl(1, k))| land(lsl(1, k), x)].
- ((0 <= k) -> ((not (land(x, lsl(1, k)) = 0)) -> bit_test(x, k))))
-
-axiom bit_test_extraction1 :
- (forall x:int. forall k:int [land(x, lsl(1, k))| land(lsl(1, k), x)].
- ((0 <= k) -> (bit_test(x, k) -> (not (land(x, lsl(1, k)) = 0)))))
-
-axiom lsl_1_0 : (lsl(1, 0) = 1)
-
-axiom bit_test_extraction_bis :
- (forall x:int [land(x, 1)| land(1, x)]. ((not (land(1, x) = 0)) ->
- bit_test(x, 0)))
-
-axiom bit_test_extraction_bis_eq :
- (forall x:int [land(x, 1)| land(1, x)]. (bit_test(x, 0) -> (land(1,
- x) = 1)))
-
-axiom lnot_extraction :
- (forall x:int. forall i:int [bit_test(lnot(x), i)]. ((0 <= i) ->
- (bit_test(lnot(x), i) -> (not bit_test(x, i)))))
-
-axiom lnot_extraction1 :
- (forall x:int. forall i:int [bit_test(lnot(x), i)]. ((0 <= i) ->
- ((not bit_test(x, i)) -> bit_test(lnot(x), i))))
-
-axiom land_extraction :
- (forall x:int. forall y:int. forall i:int [bit_test(land(x, y), i)].
- ((0 <= i) -> (bit_test(land(x, y), i) -> bit_test(x, i))))
-
-axiom land_extraction1 :
- (forall x:int. forall y:int. forall i:int [bit_test(land(x, y), i)].
- ((0 <= i) -> (bit_test(land(x, y), i) -> bit_test(y, i))))
-
-axiom land_extraction2 :
- (forall x:int. forall y:int. forall i:int [bit_test(land(x, y), i)].
- ((0 <= i) -> ((bit_test(x, i) and bit_test(y, i)) -> bit_test(land(x, y),
- i))))
-
-axiom lor_extraction :
- (forall x:int. forall y:int. forall i:int [bit_test(lor(x, y), i)].
- ((0 <= i) -> (bit_test(lor(x, y), i) -> (bit_test(x, i) or bit_test(y,
- i)))))
-
-axiom lor_extraction1 :
- (forall x:int. forall y:int. forall i:int [bit_test(lor(x, y), i)].
- ((0 <= i) -> ((bit_test(x, i) or bit_test(y, i)) -> bit_test(lor(x, y),
- i))))
-
-axiom lxor_extraction :
- (forall x:int. forall y:int. forall i:int [bit_test(lxor(x, y), i)].
- ((0 <= i) -> (bit_test(lxor(x, y), i) -> (bit_test(x, i) ->
- (not bit_test(y, i))))))
-
-axiom lxor_extraction1 :
- (forall x:int. forall y:int. forall i:int [bit_test(lxor(x, y), i)].
- ((0 <= i) -> (bit_test(lxor(x, y), i) -> ((not bit_test(y, i)) ->
- bit_test(x, i)))))
-
-axiom lxor_extraction2 :
- (forall x:int. forall y:int. forall i:int [bit_test(lxor(x, y), i)].
- ((0 <= i) -> ((bit_test(x, i) <-> (not bit_test(y, i))) -> bit_test(lxor(x,
- y), i))))
-
-axiom land_1_lsl_1 :
- (forall a:int. forall x:int. forall n:int [lsl(1, (1 + n)), lsl(1, n),
- ((2 * a) + land(1, x))]. ((0 <= n) -> ((a < lsl(1, n)) ->
- (((2 * a) + land(1, x)) < lsl(1, (1 + n))))))
-
-axiom lsl_extraction_sup :
- (forall x:int. forall n:int. forall m:int [bit_test(lsl(x, n), m)].
- ((0 <= n) -> ((0 <= m) -> ((n <= m) -> (bit_test(lsl(x, n), m) ->
- bit_test(x, (m - n)))))))
-
-axiom lsl_extraction_sup1 :
- (forall x:int. forall n:int. forall m:int [bit_test(lsl(x, n), m)].
- ((0 <= n) -> ((0 <= m) -> ((n <= m) -> (bit_test(x, (m - n)) ->
- bit_test(lsl(x, n), m))))))
-
-axiom lsl_extraction_inf :
- (forall x:int. forall n:int. forall m:int [bit_test(lsl(x, n), m)].
- ((0 <= n) -> ((0 <= m) -> ((m < n) -> (not bit_test(lsl(x, n), m))))))
-
-axiom lsr_extractionl :
- (forall x:int. forall n:int. forall m:int [bit_test(lsr(x, n), m)].
- ((0 <= n) -> ((0 <= m) -> (bit_test(lsr(x, n), m) -> bit_test(x,
- (m + n))))))
-
-axiom lsr_extractionl1 :
- (forall x:int. forall n:int. forall m:int [bit_test(lsr(x, n), m)].
- ((0 <= n) -> ((0 <= m) -> (bit_test(x, (m + n)) -> bit_test(lsr(x, n),
- m)))))
-
-axiom lsl1_extraction :
- (forall i:int. forall j:int [bit_test(lsl(1, i), j)]. ((0 <= i) ->
- ((0 <= j) -> (bit_test(lsl(1, i), j) -> (i = j)))))
-
-axiom lsl1_extraction1 :
- (forall i:int. forall j:int [bit_test(lsl(1, i), j)]. ((0 <= i) ->
- ((0 <= j) -> ((i = j) -> bit_test(lsl(1, i), j)))))
-
-axiom to_uint8_extraction_sup :
- (forall x:int. forall i:int [is_uint8(x), bit_test(x, i)]. ((8 <= i) ->
- (is_uint8(x) -> (not bit_test(x, i)))))
-
-axiom to_uint8_extraction_inf :
- (forall x:int. forall i:int [bit_test(to_uint8(x), i)]. (((0 <= i) and
- (i < 8)) -> (bit_test(to_uint8(x), i) -> bit_test(x, i))))
-
-axiom to_uint8_extraction_inf1 :
- (forall x:int. forall i:int [bit_test(to_uint8(x), i)]. (((0 <= i) and
- (i < 8)) -> (bit_test(x, i) -> bit_test(to_uint8(x), i))))
-
-axiom to_uint16_extraction_sup :
- (forall x:int. forall i:int [is_uint16(x), bit_test(x, i)]. ((16 <= i) ->
- (is_uint16(x) -> (not bit_test(x, i)))))
-
-axiom to_uint16_extraction_inf :
- (forall x:int. forall i:int [bit_test(to_uint16(x), i)]. (((0 <= i) and
- (i < 16)) -> (bit_test(to_uint16(x), i) -> bit_test(x, i))))
-
-axiom to_uint16_extraction_inf1 :
- (forall x:int. forall i:int [bit_test(to_uint16(x), i)]. (((0 <= i) and
- (i < 16)) -> (bit_test(x, i) -> bit_test(to_uint16(x), i))))
-
-axiom to_uint32_extraction_sup :
- (forall x:int. forall i:int [is_uint32(x), bit_test(x, i)]. ((32 <= i) ->
- (is_uint32(x) -> (not bit_test(x, i)))))
-
-axiom to_uint32_extraction_inf :
- (forall x:int. forall i:int [bit_test(to_uint32(x), i)]. (((0 <= i) and
- (i < 32)) -> (bit_test(to_uint32(x), i) -> bit_test(x, i))))
-
-axiom to_uint32_extraction_inf1 :
- (forall x:int. forall i:int [bit_test(to_uint32(x), i)]. (((0 <= i) and
- (i < 32)) -> (bit_test(x, i) -> bit_test(to_uint32(x), i))))
-
-axiom to_uint64_extraction_sup :
- (forall x:int. forall i:int [is_uint64(x), bit_test(x, i)]. ((64 <= i) ->
- (is_uint64(x) -> (not bit_test(x, i)))))
-
-axiom to_uint64_extraction_inf :
- (forall x:int. forall i:int [bit_test(to_uint64(x), i)]. (((0 <= i) and
- (i < 64)) -> (bit_test(to_uint64(x), i) -> bit_test(x, i))))
-
-axiom to_uint64_extraction_inf1 :
- (forall x:int. forall i:int [bit_test(to_uint64(x), i)]. (((0 <= i) and
- (i < 64)) -> (bit_test(x, i) -> bit_test(to_uint64(x), i))))
-
-axiom to_sint8_extraction_sup :
- (forall x:int. forall i:int [is_sint8(x), bit_test(x, i)]. ((7 <= i) ->
- (is_sint8(x) -> (bit_test(x, i) -> (x < 0)))))
-
-axiom to_sint8_extraction_sup1 :
- (forall x:int. forall i:int [is_sint8(x), bit_test(x, i)]. ((7 <= i) ->
- (is_sint8(x) -> ((x < 0) -> bit_test(x, i)))))
-
-axiom to_sint8_extraction_inf :
- (forall x:int. forall i:int [bit_test(to_sint8(x), i)]. (((0 <= i) and
- (i < 7)) -> (bit_test(to_sint8(x), i) -> bit_test(x, i))))
-
-axiom to_sint8_extraction_inf1 :
- (forall x:int. forall i:int [bit_test(to_sint8(x), i)]. (((0 <= i) and
- (i < 7)) -> (bit_test(x, i) -> bit_test(to_sint8(x), i))))
-
-axiom to_sint16_extraction_sup :
- (forall x:int. forall i:int [is_sint16(x), bit_test(x, i)]. ((15 <= i) ->
- (is_sint16(x) -> (bit_test(x, i) -> (x < 0)))))
-
-axiom to_sint16_extraction_sup1 :
- (forall x:int. forall i:int [is_sint16(x), bit_test(x, i)]. ((15 <= i) ->
- (is_sint16(x) -> ((x < 0) -> bit_test(x, i)))))
-
-axiom to_sint16_extraction_inf :
- (forall x:int. forall i:int [bit_test(to_sint16(x), i)]. (((0 <= i) and
- (i < 15)) -> (bit_test(to_sint16(x), i) -> bit_test(x, i))))
-
-axiom to_sint16_extraction_inf1 :
- (forall x:int. forall i:int [bit_test(to_sint16(x), i)]. (((0 <= i) and
- (i < 15)) -> (bit_test(x, i) -> bit_test(to_sint16(x), i))))
-
-axiom to_sint32_extraction_sup :
- (forall x:int. forall i:int [is_sint32(x), bit_test(x, i)]. ((31 <= i) ->
- (is_sint32(x) -> (bit_test(x, i) -> (x < 0)))))
-
-axiom to_sint32_extraction_sup1 :
- (forall x:int. forall i:int [is_sint32(x), bit_test(x, i)]. ((31 <= i) ->
- (is_sint32(x) -> ((x < 0) -> bit_test(x, i)))))
-
-axiom to_sint32_extraction_inf :
- (forall x:int. forall i:int [bit_test(to_sint32(x), i)]. (((0 <= i) and
- (i < 31)) -> (bit_test(to_sint32(x), i) -> bit_test(x, i))))
-
-axiom to_sint32_extraction_inf1 :
- (forall x:int. forall i:int [bit_test(to_sint32(x), i)]. (((0 <= i) and
- (i < 31)) -> (bit_test(x, i) -> bit_test(to_sint32(x), i))))
-
-axiom to_sint64_extraction_sup :
- (forall x:int. forall i:int [is_sint64(x), bit_test(x, i)]. ((63 <= i) ->
- (is_sint64(x) -> (bit_test(x, i) -> (x < 0)))))
-
-axiom to_sint64_extraction_sup1 :
- (forall x:int. forall i:int [is_sint64(x), bit_test(x, i)]. ((63 <= i) ->
- (is_sint64(x) -> ((x < 0) -> bit_test(x, i)))))
-
-axiom to_sint64_extraction_inf :
- (forall x:int. forall i:int [bit_test(to_sint64(x), i)]. (((0 <= i) and
- (i < 63)) -> (bit_test(to_sint64(x), i) -> bit_test(x, i))))
-
-axiom to_sint64_extraction_inf1 :
- (forall x:int. forall i:int [bit_test(to_sint64(x), i)]. (((0 <= i) and
- (i < 63)) -> (bit_test(x, i) -> bit_test(to_sint64(x), i))))
-
-axiom is_uint_lxor :
- (forall n:int. forall x:int. forall y:int. (is_uint(n, x) -> (is_uint(n,
- y) -> (to_uint(n, lxor(x, y)) = lxor(x, y)))))
-
-axiom is_uint8_lxor :
- (forall x:int. forall y:int [to_uint8(lxor(x, y))]. (is_uint8(x) ->
- (is_uint8(y) -> (to_uint8(lxor(x, y)) = lxor(x, y)))))
-
-axiom is_uint8_lor :
- (forall x:int. forall y:int [to_uint8(lor(x, y))]. (is_uint8(x) ->
- (is_uint8(y) -> (to_uint8(lor(x, y)) = lor(x, y)))))
-
-axiom is_uint8_land :
- (forall x:int. forall y:int [to_uint8(land(x, y))]. (is_uint8(x) ->
- (is_uint8(y) -> (to_uint8(land(x, y)) = land(x, y)))))
-
-axiom is_uint8_lsr :
- (forall x:int. forall y:int [to_uint8(lsr(x, y))]. ((0 <= y) ->
- (is_uint8(x) -> (to_uint8(lsr(x, y)) = lsr(x, y)))))
-
-axiom is_uint8_lsl1_inf :
- (forall y:int [to_uint8(lsl(1, y))]. (((0 <= y) and (y < 8)) ->
- (to_uint8(lsl(1, y)) = lsl(1, y))))
-
-axiom is_uint8_lsl1_sup :
- (forall y:int [to_uint8(lsl(1, y))]. ((8 <= y) -> (to_uint8(lsl(1,
- y)) = 0)))
-
-axiom is_uint16_lxor :
- (forall x:int. forall y:int [to_uint16(lxor(x, y))]. (is_uint16(x) ->
- (is_uint16(y) -> (to_uint16(lxor(x, y)) = lxor(x, y)))))
-
-axiom is_uint16_lor :
- (forall x:int. forall y:int [to_uint16(lor(x, y))]. (is_uint16(x) ->
- (is_uint16(y) -> (to_uint16(lor(x, y)) = lor(x, y)))))
-
-axiom is_uint16_land :
- (forall x:int. forall y:int [to_uint16(land(x, y))]. (is_uint16(x) ->
- (is_uint16(y) -> (to_uint16(land(x, y)) = land(x, y)))))
-
-axiom is_uint16_lsr :
- (forall x:int. forall y:int [to_uint16(lsr(x, y))]. ((0 <= y) ->
- (is_uint16(x) -> (to_uint16(lsr(x, y)) = lsr(x, y)))))
-
-axiom is_uint16_lsl1_inf :
- (forall y:int [to_uint16(lsl(1, y))]. (((0 <= y) and (y < 16)) ->
- (to_uint16(lsl(1, y)) = lsl(1, y))))
-
-axiom is_uint16_lsl1_sup :
- (forall y:int [to_uint16(lsl(1, y))]. ((16 <= y) -> (to_uint16(lsl(1,
- y)) = 0)))
-
-axiom is_uint32_lxor :
- (forall x:int. forall y:int [to_uint32(lxor(x, y))]. (is_uint32(x) ->
- (is_uint32(y) -> (to_uint32(lxor(x, y)) = lxor(x, y)))))
-
-axiom is_uint32_lor :
- (forall x:int. forall y:int [to_uint32(lor(x, y))]. (is_uint32(x) ->
- (is_uint32(y) -> (to_uint32(lor(x, y)) = lor(x, y)))))
-
-axiom is_uint32_land :
- (forall x:int. forall y:int [to_uint32(land(x, y))]. (is_uint32(x) ->
- (is_uint32(y) -> (to_uint32(land(x, y)) = land(x, y)))))
-
-axiom is_uint32_lsr :
- (forall x:int. forall y:int [to_uint32(lsr(x, y))]. ((0 <= y) ->
- (is_uint32(x) -> (to_uint32(lsr(x, y)) = lsr(x, y)))))
-
-axiom is_uint32_lsl1_inf :
- (forall y:int [to_uint32(lsl(1, y))]. (((0 <= y) and (y < 32)) ->
- (to_uint32(lsl(1, y)) = lsl(1, y))))
-
-axiom is_uint32_lsl1_sup :
- (forall y:int [to_uint32(lsl(1, y))]. ((32 <= y) -> (to_uint32(lsl(1,
- y)) = 0)))
-
-axiom is_uint64_lxor :
- (forall x:int. forall y:int [to_uint64(lxor(x, y))]. (is_uint64(x) ->
- (is_uint64(y) -> (to_uint64(lxor(x, y)) = lxor(x, y)))))
-
-axiom is_uint64_lor :
- (forall x:int. forall y:int [to_uint64(lor(x, y))]. (is_uint64(x) ->
- (is_uint64(y) -> (to_uint64(lor(x, y)) = lor(x, y)))))
-
-axiom is_uint64_land :
- (forall x:int. forall y:int [to_uint64(land(x, y))]. (is_uint64(x) ->
- (is_uint64(y) -> (to_uint64(land(x, y)) = land(x, y)))))
-
-axiom is_uint64_lsr :
- (forall x:int. forall y:int [to_uint64(lsr(x, y))]. ((0 <= y) ->
- (is_uint64(x) -> (to_uint64(lsr(x, y)) = lsr(x, y)))))
-
-axiom is_uint64_lsl1_inf :
- (forall y:int [to_uint64(lsl(1, y))]. (((0 <= y) and (y < 64)) ->
- (to_uint64(lsl(1, y)) = lsl(1, y))))
-
-axiom is_uint64_lsl1_sup :
- (forall y:int [to_uint64(lsl(1, y))]. ((64 <= y) -> (to_uint64(lsl(1,
- y)) = 0)))
-
-axiom is_sint8_lnot :
- (forall x:int [to_sint8(lnot(x))]. (is_sint8(x) ->
- (to_sint8(lnot(x)) = lnot(x))))
-
-axiom is_sint8_lxor :
- (forall x:int. forall y:int [to_sint8(lxor(x, y))]. (is_sint8(x) ->
- (is_sint8(y) -> (to_sint8(lxor(x, y)) = lxor(x, y)))))
-
-axiom is_sint8_lor :
- (forall x:int. forall y:int [to_sint8(lor(x, y))]. (is_sint8(x) ->
- (is_sint8(y) -> (to_sint8(lor(x, y)) = lor(x, y)))))
-
-axiom is_sint8_land :
- (forall x:int. forall y:int [to_sint8(land(x, y))]. (is_sint8(x) ->
- (is_sint8(y) -> (to_sint8(land(x, y)) = land(x, y)))))
-
-axiom is_sint8_lsr :
- (forall x:int. forall y:int [to_sint8(lsr(x, y))]. ((0 <= y) ->
- (is_sint8(x) -> (to_sint8(lsr(x, y)) = lsr(x, y)))))
-
-axiom is_sint8_lsl1 : (lsl(1, 7) = 128)
-
-axiom is_sint8_lsl1_inf :
- (forall y:int [to_sint8(lsl(1, y))]. (((0 <= y) and (y < 7)) ->
- (to_sint8(lsl(1, y)) = lsl(1, y))))
-
-axiom is_sint8_lsl1_sup :
- (forall y:int [to_sint8(lsl(1, y))]. ((8 <= y) -> (to_sint8(lsl(1,
- y)) = 0)))
-
-axiom is_sint16_lnot :
- (forall x:int [to_sint16(lnot(x))]. (is_sint16(x) ->
- (to_sint16(lnot(x)) = lnot(x))))
-
-axiom is_sint16_lxor :
- (forall x:int. forall y:int [to_sint16(lxor(x, y))]. (is_sint16(x) ->
- (is_sint16(y) -> (to_sint16(lxor(x, y)) = lxor(x, y)))))
-
-axiom is_sint16_lor :
- (forall x:int. forall y:int [to_sint16(lor(x, y))]. (is_sint16(x) ->
- (is_sint16(y) -> (to_sint16(lor(x, y)) = lor(x, y)))))
-
-axiom is_sint16_land :
- (forall x:int. forall y:int [to_sint16(land(x, y))]. (is_sint16(x) ->
- (is_sint16(y) -> (to_sint16(land(x, y)) = land(x, y)))))
-
-axiom is_sint16_lsr :
- (forall x:int. forall y:int [to_sint16(lsr(x, y))]. ((0 <= y) ->
- (is_sint16(x) -> (to_sint16(lsr(x, y)) = lsr(x, y)))))
-
-axiom is_sint16_lsl1 : (lsl(1, 15) = 32768)
-
-axiom is_sint16_lsl1_inf :
- (forall y:int [to_sint16(lsl(1, y))]. (((0 <= y) and (y < 15)) ->
- (to_sint16(lsl(1, y)) = lsl(1, y))))
-
-axiom is_sint16_lsl1_sup :
- (forall y:int [to_sint16(lsl(1, y))]. ((16 <= y) -> (to_sint16(lsl(1,
- y)) = 0)))
-
-axiom is_sint32_lnot :
- (forall x:int [to_sint32(lnot(x))]. (is_sint32(x) ->
- (to_sint32(lnot(x)) = lnot(x))))
-
-axiom is_sint32_lxor :
- (forall x:int. forall y:int [to_sint32(lxor(x, y))]. (is_sint32(x) ->
- (is_sint32(y) -> (to_sint32(lxor(x, y)) = lxor(x, y)))))
-
-axiom is_sint32_lor :
- (forall x:int. forall y:int [to_sint32(lor(x, y))]. (is_sint32(x) ->
- (is_sint32(y) -> (to_sint32(lor(x, y)) = lor(x, y)))))
-
-axiom is_sint32_land :
- (forall x:int. forall y:int [to_sint32(land(x, y))]. (is_sint32(x) ->
- (is_sint32(y) -> (to_sint32(land(x, y)) = land(x, y)))))
-
-axiom is_sint32_lsr :
- (forall x:int. forall y:int [to_sint32(lsr(x, y))]. ((0 <= y) ->
- (is_sint32(x) -> (to_sint32(lsr(x, y)) = lsr(x, y)))))
-
-axiom is_sint32_lsl1 : (lsl(1, 31) = 2147483648)
-
-axiom is_sint32_lsl1_inf :
- (forall y:int [to_sint32(lsl(1, y))]. (((0 <= y) and (y < 31)) ->
- (to_sint32(lsl(1, y)) = lsl(1, y))))
-
-axiom is_sint32_lsl1_sup :
- (forall y:int [to_sint32(lsl(1, y))]. ((32 <= y) -> (to_sint32(lsl(1,
- y)) = 0)))
-
-axiom is_sint64_lnot :
- (forall x:int [to_sint64(lnot(x))]. (is_sint64(x) ->
- (to_sint64(lnot(x)) = lnot(x))))
-
-axiom is_sint64_lxor :
- (forall x:int. forall y:int [to_sint64(lxor(x, y))]. (is_sint64(x) ->
- (is_sint64(y) -> (to_sint64(lxor(x, y)) = lxor(x, y)))))
-
-axiom is_sint64_lor :
- (forall x:int. forall y:int [to_sint64(lor(x, y))]. (is_sint64(x) ->
- (is_sint64(y) -> (to_sint64(lor(x, y)) = lor(x, y)))))
-
-axiom is_sint64_land :
- (forall x:int. forall y:int [to_sint64(land(x, y))]. (is_sint64(x) ->
- (is_sint64(y) -> (to_sint64(land(x, y)) = land(x, y)))))
-
-axiom is_sint64_lsr :
- (forall x:int. forall y:int [to_sint64(lsr(x, y))]. ((0 <= y) ->
- (is_sint64(x) -> (to_sint64(lsr(x, y)) = lsr(x, y)))))
-
-axiom is_sint64_lsl1 : (lsl(1, 63) = 9223372036854775808)
-
-axiom is_sint64_lsl1_inf :
- (forall y:int [to_sint64(lsl(1, y))]. (((0 <= y) and (y < 63)) ->
- (to_sint64(lsl(1, y)) = lsl(1, y))))
-
-axiom is_sint64_lsl1_sup :
- (forall y:int [to_sint64(lsl(1, y))]. ((64 <= y) -> (to_sint64(lsl(1,
- y)) = 0)))
-
-axiom lor_addition :
- (forall x:int. forall y:int [land(x, y), lor(x, y)]. ((land(x, y) = 0) ->
- ((x + y) = lor(x, y))))
-
-axiom lxor_addition :
- (forall x:int. forall y:int [land(x, y), lxor(x, y)]. ((land(x, y) = 0) ->
- ((x + y) = lxor(x, y))))
diff --git a/src/plugins/wp/share/ergo/Cfloat.mlw b/src/plugins/wp/share/ergo/Cfloat.mlw
deleted file mode 100644
index 8767b09720c..00000000000
--- a/src/plugins/wp/share/ergo/Cfloat.mlw
+++ /dev/null
@@ -1,360 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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 real_Real_ must be appended to this file*)
-(** The theory real_RealInfix_ must be appended to this file*)
-(** The theory real_Abs_ must be appended to this file*)
-(** The theory real_FromInt_ must be appended to this file*)
-(** The theory real_Square_ must be appended to this file*)
-type f32
-
-type f64
-
-logic to_f32 : real -> f32
-
-logic of_f32 : f32 -> real
-
-logic to_f64 : real -> f64
-
-logic 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
-
-logic match_rounding_mode : rounding_mode, 'a, 'a, 'a, 'a, 'a -> 'a
-
-axiom match_rounding_mode_Up :
- (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
- (match_rounding_mode(Up, z, z1, z2, z3, z4) = z))
-
-axiom match_rounding_mode_Down :
- (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
- (match_rounding_mode(Down, z, z1, z2, z3, z4) = z1))
-
-axiom match_rounding_mode_ToZero :
- (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
- (match_rounding_mode(ToZero, z, z1, z2, z3, z4) = z2))
-
-axiom match_rounding_mode_NearestTiesToAway :
- (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
- (match_rounding_mode(NearestTiesToAway, z, z1, z2, z3, z4) = z3))
-
-axiom match_rounding_mode_NearestTiesToEven :
- (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
- (match_rounding_mode(NearestTiesToEven, z, z1, z2, z3, z4) = z4))
-
-logic round_float : rounding_mode, real -> f32
-
-logic 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
-
-logic match_float_kind : float_kind, 'a, 'a, 'a, 'a -> 'a
-
-axiom match_float_kind_Finite :
- (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a.
- (match_float_kind(Finite, z, z1, z2, z3) = z))
-
-axiom match_float_kind_NaN :
- (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a.
- (match_float_kind(NaN, z, z1, z2, z3) = z1))
-
-axiom match_float_kind_Inf_pos :
- (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a.
- (match_float_kind(Inf_pos, z, z1, z2, z3) = z2))
-
-axiom match_float_kind_Inf_neg :
- (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a.
- (match_float_kind(Inf_neg, z, z1, z2, z3) = z3))
-
-logic classify_f32 : f32 -> float_kind
-
-logic 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) or
- (classify_f32(f) = Inf_neg))
-
-predicate is_infinite_f64(d: f64) = ((classify_f64(d) = Inf_pos) or
- (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)) and
- is_finite_f64(to_f64(x)))
-
-axiom finite_small_f32 :
- (forall x:real.
- ((((-179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0) <= x) and
- (x <= 340282346600000016151267322115014000640.0)) ->
- is_finite_f32(to_f32(x))))
-
-axiom finite_small_f64 :
- (forall x:real.
- ((((-179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0) <= x) and
- (x <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0)) ->
- is_finite_f64(to_f64(x))))
-
-axiom finite_range_f32 :
- (forall f:f32. (is_finite_f32(f) ->
- ((-340282346600000016151267322115014000640.0) <= of_f32(f))))
-
-axiom finite_range_f321 :
- (forall f:f32. (is_finite_f32(f) ->
- (of_f32(f) <= 340282346600000016151267322115014000640.0)))
-
-axiom finite_range_f322 :
- (forall f:f32.
- ((((-340282346600000016151267322115014000640.0) <= of_f32(f)) and
- (of_f32(f) <= 340282346600000016151267322115014000640.0)) ->
- is_finite_f32(f)))
-
-axiom finite_range_f64 :
- (forall d:f64. (is_finite_f64(d) ->
- ((-179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0) <= of_f64(d))))
-
-axiom finite_range_f641 :
- (forall d:f64. (is_finite_f64(d) ->
- (of_f64(d) <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0)))
-
-axiom finite_range_f642 :
- (forall d:f64.
- ((((-179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0) <= of_f64(d)) and
- (of_f64(d) <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0)) ->
- is_finite_f64(d)))
-
-logic eq_f32b : f32, f32 -> bool
-
-logic eq_f64b : f64, f64 -> bool
-
-predicate eq_f32(x: f32, y: f32) = (eq_f32b(x, y) = true)
-
-predicate eq_f64(x: f64, y: f64) = (eq_f64b(x, y) = true)
-
-axiom eq_finite_f32 :
- (forall x:f32. forall 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_f321 :
- (forall x:f32. forall y:f32 [eq_f32(x, y)]. (is_finite_f32(x) ->
- (is_finite_f32(y) -> ((of_f32(x) = of_f32(y)) -> eq_f32(x, y)))))
-
-axiom eq_finite_f64 :
- (forall x:f64. forall y:f64 [eq_f64(x, y)]. (is_finite_f64(x) ->
- (is_finite_f64(y) -> (eq_f64(x, y) -> (of_f64(x) = of_f64(y))))))
-
-axiom eq_finite_f641 :
- (forall x:f64. forall y:f64 [eq_f64(x, y)]. (is_finite_f64(x) ->
- (is_finite_f64(y) -> ((of_f64(x) = of_f64(y)) -> eq_f64(x, y)))))
-
-logic ne_f32b : f32, f32 -> bool
-
-logic ne_f64b : f64, f64 -> bool
-
-predicate ne_f32(x: f32, y: f32) = (ne_f32b(x, y) = true)
-
-predicate ne_f64(x: f64, y: f64) = (ne_f64b(x, y) = true)
-
-axiom ne_finite_f32 :
- (forall x:f32. forall 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_f321 :
- (forall x:f32. forall y:f32 [ne_f32(x, y)]. (is_finite_f32(x) ->
- (is_finite_f32(y) -> ((not (of_f32(x) = of_f32(y))) -> ne_f32(x, y)))))
-
-axiom ne_finite_f64 :
- (forall x:f64. forall 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)))))))
-
-axiom ne_finite_f641 :
- (forall x:f64. forall y:f64 [ne_f64(x, y)]. (is_finite_f64(x) ->
- (is_finite_f64(y) -> ((not (of_f64(x) = of_f64(y))) -> ne_f64(x, y)))))
-
-logic le_f32b : f32, f32 -> bool
-
-logic le_f64b : f64, f64 -> bool
-
-predicate le_f32(x: f32, y: f32) = (le_f32b(x, y) = true)
-
-predicate le_f64(x: f64, y: f64) = (le_f64b(x, y) = true)
-
-axiom le_finite_f32 :
- (forall x:f32. forall y:f32 [le_f32(x, y)]. (is_finite_f32(x) ->
- (is_finite_f32(y) -> (le_f32(x, y) -> (of_f32(x) <= of_f32(y))))))
-
-axiom le_finite_f321 :
- (forall x:f32. forall y:f32 [le_f32(x, y)]. (is_finite_f32(x) ->
- (is_finite_f32(y) -> ((of_f32(x) <= of_f32(y)) -> le_f32(x, y)))))
-
-axiom le_finite_f64 :
- (forall x:f64. forall y:f64 [le_f64(x, y)]. (is_finite_f64(x) ->
- (is_finite_f64(y) -> (le_f64(x, y) -> (of_f64(x) <= of_f64(y))))))
-
-axiom le_finite_f641 :
- (forall x:f64. forall y:f64 [le_f64(x, y)]. (is_finite_f64(x) ->
- (is_finite_f64(y) -> ((of_f64(x) <= of_f64(y)) -> le_f64(x, y)))))
-
-logic lt_f32b : f32, f32 -> bool
-
-logic lt_f64b : f64, f64 -> bool
-
-predicate lt_f32(x: f32, y: f32) = (lt_f32b(x, y) = true)
-
-predicate lt_f64(x: f64, y: f64) = (lt_f64b(x, y) = true)
-
-axiom lt_finite_f32 :
- (forall x:f32. forall y:f32 [lt_f32(x, y)]. (is_finite_f32(x) ->
- (is_finite_f32(y) -> (lt_f32(x, y) -> (of_f32(x) < of_f32(y))))))
-
-axiom lt_finite_f321 :
- (forall x:f32. forall y:f32 [lt_f32(x, y)]. (is_finite_f32(x) ->
- (is_finite_f32(y) -> ((of_f32(x) < of_f32(y)) -> lt_f32(x, y)))))
-
-axiom lt_finite_f64 :
- (forall x:f64. forall y:f64 [lt_f64(x, y)]. (is_finite_f64(x) ->
- (is_finite_f64(y) -> (lt_f64(x, y) -> (of_f64(x) < of_f64(y))))))
-
-axiom lt_finite_f641 :
- (forall x:f64. forall y:f64 [lt_f64(x, y)]. (is_finite_f64(x) ->
- (is_finite_f64(y) -> ((of_f64(x) < of_f64(y)) -> lt_f64(x, y)))))
-
-logic neg_f32 : f32 -> f32
-
-logic neg_f64 : f64 -> f64
-
-axiom neg_finite_f32 :
- (forall x:f32 [neg_f32(x)]. (is_finite_f32(x) ->
- (of_f32(neg_f32(x)) = (-of_f32(x)))))
-
-axiom neg_finite_f64 :
- (forall x:f64 [neg_f64(x)]. (is_finite_f64(x) ->
- (of_f64(neg_f64(x)) = (-of_f64(x)))))
-
-logic add_f32 : f32, f32 -> f32
-
-logic add_f64 : f64, f64 -> f64
-
-axiom add_finite_f32 :
- (forall x:f32. forall y:f32 [add_f32(x, y)]. (is_finite_f32(x) ->
- (is_finite_f32(y) -> (add_f32(x, y) = to_f32((of_f32(x) + of_f32(y)))))))
-
-axiom add_finite_f64 :
- (forall x:f64. forall y:f64 [add_f64(x, y)]. (is_finite_f64(x) ->
- (is_finite_f64(y) -> (add_f64(x, y) = to_f64((of_f64(x) + of_f64(y)))))))
-
-logic mul_f32 : f32, f32 -> f32
-
-logic mul_f64 : f64, f64 -> f64
-
-axiom mul_finite_f32 :
- (forall x:f32. forall y:f32 [mul_f32(x, y)]. (is_finite_f32(x) ->
- (is_finite_f32(y) -> (mul_f32(x, y) = to_f32((of_f32(x) * of_f32(y)))))))
-
-axiom mul_finite_f64 :
- (forall x:f64. forall y:f64 [mul_f64(x, y)]. (is_finite_f64(x) ->
- (is_finite_f64(y) -> (mul_f64(x, y) = to_f64((of_f64(x) * of_f64(y)))))))
-
-logic div_f32 : f32, f32 -> f32
-
-logic div_f64 : f64, f64 -> f64
-
-axiom div_finite_f32 :
- (forall x:f32. forall y:f32 [div_f32(x, y)]. (is_finite_f32(x) ->
- (is_finite_f32(y) -> (div_f32(x, y) = to_f32((of_f32(x) / of_f32(y)))))))
-
-axiom div_finite_f64 :
- (forall x:f64. forall y:f64 [div_f64(x, y)]. (is_finite_f64(x) ->
- (is_finite_f64(y) -> (div_f64(x, y) = to_f64((of_f64(x) / of_f64(y)))))))
-
-logic sqrt_f32 : f32 -> f32
-
-logic sqrt_f64 : f64 -> f64
-
-axiom sqrt_finite_f32 :
- (forall x:f32 [sqrt_f32(x)]. (is_finite_f32(x) ->
- (sqrt_f32(x) = to_f32(sqrt(of_f32(x))))))
-
-axiom sqrt_finite_f64 :
- (forall x:f64 [sqrt_f64(x)]. (is_finite_f64(x) ->
- (sqrt_f64(x) = to_f64(sqrt(of_f64(x))))))
-
-logic model_f32 : f32 -> real
-
-function delta_f32(f: f32) : real = abs_real((of_f32(f) - model_f32(f)))
-
-function error_f32(f: f32) : real = (delta_f32(f) / abs_real(model_f32(f)))
-
-logic model_f64 : f64 -> real
-
-function delta_f64(f: f64) : real = abs_real((of_f64(f) - model_f64(f)))
-
-function error_f64(f: f64) : real = (delta_f64(f) / abs_real(model_f64(f)))
-
diff --git a/src/plugins/wp/share/ergo/Cint.mlw b/src/plugins/wp/share/ergo/Cint.mlw
deleted file mode 100644
index 7dab2653490..00000000000
--- a/src/plugins/wp/share/ergo/Cint.mlw
+++ /dev/null
@@ -1,224 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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*)
-predicate is_bool(x: int) = ((x = 0) or (x = 1))
-
-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)))
-
-axiom is_bool0 : is_bool(0)
-
-axiom is_bool1 : is_bool(1)
-
-logic to_bool : int -> int
-
-axiom to_bool_def : (forall x:int. ((x = 0) -> (to_bool(x) = 0)))
-
-axiom to_bool_def1 : (forall x:int. ((not (x = 0)) -> (to_bool(x) = 1)))
-
-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)))
-
diff --git a/src/plugins/wp/share/ergo/Cmath.mlw b/src/plugins/wp/share/ergo/Cmath.mlw
deleted file mode 100644
index 137cf15a396..00000000000
--- a/src/plugins/wp/share/ergo/Cmath.mlw
+++ /dev/null
@@ -1,34 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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*)
-(** The theory real_Real_ must be appended to this file*)
-(** The theory real_RealInfix_ must be appended to this file*)
-axiom abs_def : (forall x:int [abs_int(x)]. ((0 <= x) -> (abs_int(x) = x)))
-
-axiom abs_def1 :
- (forall x:int [abs_int(x)]. ((not (0 <= x)) -> (abs_int(x) = (-x))))
-
diff --git a/src/plugins/wp/share/ergo/ExpLog.mlw b/src/plugins/wp/share/ergo/ExpLog.mlw
deleted file mode 100644
index c71d17e18b0..00000000000
--- a/src/plugins/wp/share/ergo/ExpLog.mlw
+++ /dev/null
@@ -1,30 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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 theory real_RealInfix_ must be appended to this file*)
-(** The theory real_ExpLog_ must be appended to this file*)
-axiom exp_pos : (forall x:real. (0.0 < exp(x)))
-
diff --git a/src/plugins/wp/share/ergo/Memory.mlw b/src/plugins/wp/share/ergo/Memory.mlw
deleted file mode 100644
index 32ac4406cf9..00000000000
--- a/src/plugins/wp/share/ergo/Memory.mlw
+++ /dev/null
@@ -1,212 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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 map_Map_ must be appended to this file*)
-type addr = { base : int; offset : int
-}
-
-logic addr_le : addr, addr -> prop
-
-logic addr_lt : addr, addr -> prop
-
-logic addr_le_bool : addr, addr -> bool
-
-logic addr_lt_bool : addr, addr -> bool
-
-axiom addr_le_def :
- (forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
- (addr_le(p, q) -> ((p).offset <= (q).offset))))
-
-axiom addr_le_def1 :
- (forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
- (((p).offset <= (q).offset) -> addr_le(p, q))))
-
-axiom addr_lt_def :
- (forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) ->
- (addr_lt(p, q) -> ((p).offset < (q).offset))))
-
-axiom addr_lt_def1 :
- (forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) ->
- (((p).offset < (q).offset) -> addr_lt(p, q))))
-
-axiom addr_le_bool_def :
- (forall p:addr. forall q:addr [addr_le_bool(p, q)]. (addr_le(p, q) ->
- (addr_le_bool(p, q) = true)))
-
-axiom addr_le_bool_def1 :
- (forall p:addr. forall q:addr [addr_le_bool(p, q)]. ((addr_le_bool(p,
- q) = true) -> addr_le(p, q)))
-
-axiom addr_lt_bool_def :
- (forall p:addr. forall q:addr [addr_lt_bool(p, q)]. (addr_lt(p, q) ->
- (addr_lt_bool(p, q) = true)))
-
-axiom addr_lt_bool_def1 :
- (forall p:addr. forall q:addr [addr_lt_bool(p, q)]. ((addr_lt_bool(p,
- q) = true) -> addr_lt(p, q)))
-
-function null() : addr = { base = 0; offset = 0 }
-
-function global(b: int) : addr = { base = b; offset = 0 }
-
-function shift(p: addr, k: int) : addr = { base = (p).base; offset =
- ((p).offset + k) }
-
-predicate included(p: addr, a: int, q: addr, b: int) = ((0 < a) ->
- ((0 <= b) and (((p).base = (q).base) and (((q).offset <= (p).offset) and
- (((p).offset + a) <= ((q).offset + b))))))
-
-predicate separated(p: addr, a: int, q: addr, b: int) = ((a <= 0) or
- ((b <= 0) or ((not ((p).base = (q).base)) or
- ((((q).offset + b) <= (p).offset) or (((p).offset + a) <= (q).offset)))))
-
-predicate eqmem(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr,
- a1: int) =
- (forall q:addr [(m1[p])| (m2[q])]. (included(q, 1, p, a1) ->
- ((m1[q]) = (m2[q]))))
-
-logic havoc : (addr,'a) farray, (addr,'a) farray, addr,
- int -> (addr,'a) farray
-
-predicate valid_rw(m: (int,int) farray, p: addr, n: int) = ((0 < n) ->
- ((0 < (p).base) and ((0 <= (p).offset) and
- (((p).offset + n) <= (m[(p).base])))))
-
-predicate valid_rd(m: (int,int) farray, p: addr, n: int) = ((0 < n) ->
- ((not (0 = (p).base)) and ((0 <= (p).offset) and
- (((p).offset + n) <= (m[(p).base])))))
-
-predicate invalid(m: (int,int) farray, p: addr, n: int) = ((0 < n) ->
- (((m[(p).base]) <= (p).offset) or (((p).offset + n) <= 0)))
-
-axiom valid_rw_rd :
- (forall m:(int,int) farray.
- (forall p:addr. (forall n:int. (valid_rw(m, p, n) -> valid_rd(m, p, n)))))
-
-axiom valid_string :
- (forall m:(int,int) farray.
- (forall p:addr. (((p).base < 0) -> (((0 <= (p).offset) and
- ((p).offset < (m[(p).base]))) -> valid_rd(m, p, 1)))))
-
-axiom valid_string1 :
- (forall m:(int,int) farray.
- (forall p:addr. (((p).base < 0) -> (((0 <= (p).offset) and
- ((p).offset < (m[(p).base]))) -> (not valid_rw(m, p, 1))))))
-
-axiom separated_1 :
- (forall p:addr. forall q:addr.
- (forall a:int. forall b:int. forall i:int. forall j:int [separated(p, a, q,
- b), { base = (p).base; offset = i }, { base = (q).base; offset = j }].
- (separated(p, a, q, b) -> ((((p).offset <= i) and
- (i < ((p).offset + a))) -> ((((q).offset <= j) and
- (j < ((q).offset + b))) -> (not ({ base = (p).base; offset = i } = {
- base = (q).base; offset = j })))))))
-
-logic region : int -> int
-
-logic linked : (int,int) farray -> prop
-
-logic sconst : (addr,int) farray -> prop
-
-predicate framed(m: (addr,addr) farray) =
- (forall p:addr [(m[p])]. (region(((m[p])).base) <= 0))
-
-axiom separated_included :
- (forall p:addr. forall q:addr.
- (forall a:int. forall b:int [separated(p, a, q, b), included(p, a, q, b)].
- ((0 < a) -> ((0 < b) -> (separated(p, a, q, b) -> (not included(p, a, q,
- b)))))))
-
-axiom included_trans :
- (forall p:addr. forall q:addr. forall r:addr.
- (forall a:int. forall b:int. forall 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)))))
-
-axiom separated_trans :
- (forall p:addr. forall q:addr. forall r:addr.
- (forall a:int. forall b:int. forall 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)))))
-
-axiom separated_sym :
- (forall p:addr. forall q:addr.
- (forall a:int. forall b:int [separated(p, a, q, b)]. (separated(p, a, q,
- b) -> separated(q, b, p, a))))
-
-axiom separated_sym1 :
- (forall p:addr. forall q:addr.
- (forall a:int. forall b:int [separated(p, a, q, b)]. (separated(q, b, p,
- a) -> separated(p, a, q, b))))
-
-axiom eqmem_included :
- (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
- (forall p:addr. forall q:addr.
- (forall a1:int. forall b:int [eqmem(m1, m2, p, a1), eqmem(m1, m2, q, b)].
- (included(p, a1, q, b) -> (eqmem(m1, m2, q, b) -> eqmem(m1, m2, p, a1))))))
-
-axiom eqmem_sym :
- (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray.
- (forall p:addr.
- (forall a1:int. (eqmem(m1, m2, p, a1) -> eqmem(m2, m1, p, a1)))))
-
-axiom havoc_access :
- (forall m0:(addr,'a) farray. forall m1:(addr,'a) farray.
- (forall q:addr. forall p:addr.
- (forall a1:int. (separated(q, 1, p, a1) -> ((havoc(m0, m1, p,
- a1)[q]) = (m1[q]))))))
-
-axiom havoc_access1 :
- (forall m0:(addr,'a) farray. forall m1:(addr,'a) farray.
- (forall q:addr. forall p:addr.
- (forall a1:int. ((not separated(q, 1, p, a1)) -> ((havoc(m0, m1, p,
- a1)[q]) = (m0[q]))))))
-
-logic int_of_addr : addr -> int
-
-logic addr_of_int : int -> addr
-
-logic base_offset : int -> int
-
-logic base_index : int -> int
-
-axiom int_of_addr_bijection :
- (forall a:int. (int_of_addr(addr_of_int(a)) = a))
-
-axiom addr_of_int_bijection :
- (forall p:addr. (addr_of_int(int_of_addr(p)) = p))
-
-axiom addr_of_null : (int_of_addr(null) = 0)
-
-axiom base_offset_zero : (base_offset(0) = 0)
-
-axiom base_offset_inj : (forall i:int. (base_index(base_offset(i)) = i))
-
-axiom base_offset_monotonic :
- (forall i:int. forall j:int. ((i < j) ->
- (base_offset(i) < base_offset(j))))
-
diff --git a/src/plugins/wp/share/ergo/Qed.mlw b/src/plugins/wp/share/ergo/Qed.mlw
deleted file mode 100644
index 08a3998f07c..00000000000
--- a/src/plugins/wp/share/ergo/Qed.mlw
+++ /dev/null
@@ -1,158 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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 match_bool : bool, 'a, 'a -> 'a
-
-axiom match_bool1 :
- (forall p:bool. forall x:'a. forall y:'a [match_bool(p, x, y)].
- (((p = true) and (match_bool(p, x, y) = x)) or ((p = false) and
- (match_bool(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)))
-
-function real_of_int(x: int) : real = from_int(x)
-
-axiom cdiv_cases :
- (forall n:int. forall d:int [div(n, d)]. ((0 <= n) -> ((0 < d) -> (div(n,
- d) = (n / d)))))
-
-axiom cdiv_cases1 :
- (forall n:int. forall d:int [div(n, d)]. ((n <= 0) -> ((0 < d) -> (div(n,
- d) = (-((-n) / d))))))
-
-axiom cdiv_cases2 :
- (forall n:int. forall d:int [div(n, d)]. ((0 <= n) -> ((d < 0) -> (div(n,
- d) = (-(n / (-d)))))))
-
-axiom cdiv_cases3 :
- (forall n:int. forall d:int [div(n, d)]. ((n <= 0) -> ((d < 0) -> (div(n,
- d) = ((-n) / (-d))))))
-
-axiom cmod_cases :
- (forall n:int. forall d:int [mod(n, d)]. ((0 <= n) -> ((0 < d) -> (mod(n,
- d) = (n % d)))))
-
-axiom cmod_cases1 :
- (forall n:int. forall d:int [mod(n, d)]. ((n <= 0) -> ((0 < d) -> (mod(n,
- d) = (-((-n) % d))))))
-
-axiom cmod_cases2 :
- (forall n:int. forall d:int [mod(n, d)]. ((0 <= n) -> ((d < 0) -> (mod(n,
- d) = (n % (-d))))))
-
-axiom cmod_cases3 :
- (forall n:int. forall d:int [mod(n, d)]. ((n <= 0) -> ((d < 0) -> (mod(n,
- d) = (-((-n) % (-d)))))))
-
-axiom c_euclidian :
- (forall n:int. forall d:int [div(n, d), mod(n, d)]. ((not (d = 0)) ->
- (n = ((div(n, d) * d) + mod(n, d)))))
-
-axiom cmod_remainder :
- (forall n:int. forall d:int [mod(n, d)]. ((0 <= n) -> ((0 < d) ->
- (0 <= mod(n, d)))))
-
-axiom cmod_remainder1 :
- (forall n:int. forall d:int [mod(n, d)]. ((0 <= n) -> ((0 < d) -> (mod(n,
- d) < d))))
-
-axiom cmod_remainder2 :
- (forall n:int. forall d:int [mod(n, d)]. ((n <= 0) -> ((0 < d) ->
- ((-d) < mod(n, d)))))
-
-axiom cmod_remainder3 :
- (forall n:int. forall d:int [mod(n, d)]. ((n <= 0) -> ((0 < d) -> (mod(n,
- d) <= 0))))
-
-axiom cmod_remainder4 :
- (forall n:int. forall d:int [mod(n, d)]. ((0 <= n) -> ((d < 0) ->
- (0 <= mod(n, d)))))
-
-axiom cmod_remainder5 :
- (forall n:int. forall d:int [mod(n, d)]. ((0 <= n) -> ((d < 0) -> (mod(n,
- d) < (-d)))))
-
-axiom cmod_remainder6 :
- (forall n:int. forall d:int [mod(n, d)]. ((n <= 0) -> ((d < 0) ->
- (d < mod(n, d)))))
-
-axiom cmod_remainder7 :
- (forall n:int. forall d:int [mod(n, d)]. ((n <= 0) -> ((d < 0) -> (mod(n,
- d) <= 0))))
-
-axiom cdiv_neutral : (forall a:int [div(a, 1)]. (div(a, 1) = a))
-
-axiom cdiv_inv :
- (forall a:int [div(a, a)]. ((not (a = 0)) -> (div(a, a) = 1)))
-
-axiom cdiv_closed_remainder :
- (forall a:int. forall b:int. forall n:int. ((0 <= a) -> ((0 <= b) ->
- (((0 <= (b - a)) and ((b - a) < n)) -> ((mod(a,n) = mod(b,n)) ->
- (a = b))))))
diff --git a/src/plugins/wp/share/ergo/Square.mlw b/src/plugins/wp/share/ergo/Square.mlw
deleted file mode 100644
index 3a1f199e50e..00000000000
--- a/src/plugins/wp/share/ergo/Square.mlw
+++ /dev/null
@@ -1,37 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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 theory real_RealInfix_ must be appended to this file*)
-(** The theory real_Square_ must be appended to this file*)
-axiom sqrt_lin1 : (forall x:real [sqrt(x)]. ((1.0 < x) -> (sqrt(x) < x)))
-
-axiom sqrt_lin0 :
- (forall x:real [sqrt(x)]. (((0.0 < x) and (x < 1.0)) -> (x < sqrt(x))))
-
-axiom sqrt_0 : (sqrt(0.0) = 0.0)
-
-axiom sqrt_1 : (sqrt(1.0) = 1.0)
-
diff --git a/src/plugins/wp/share/ergo/Vlist.mlw b/src/plugins/wp/share/ergo/Vlist.mlw
deleted file mode 100644
index c10ced2bdb5..00000000000
--- a/src/plugins/wp/share/ergo/Vlist.mlw
+++ /dev/null
@@ -1,126 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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*)
-(** The theory int_ComputerDivision_ must be appended to this file*)
-type 'a list
-
-logic nil : 'a list
-
-logic cons : 'a, 'a list -> 'a list
-
-logic concat : 'a list, 'a list -> 'a list
-
-logic repeat : 'a list, int -> 'a list
-
-logic length : 'a list -> int
-
-logic nth : 'a list, int -> 'a
-
-axiom length_pos : (forall w:'a list. (0 <= length(w)))
-
-axiom length_nil : (length((nil : 'a list)) = 0)
-
-axiom length_nil_bis :
- (forall w:'a list. ((length(w) = 0) -> (w = (nil : 'a list))))
-
-axiom length_cons :
- (forall x:'a. forall w:'a list [length(cons(x, w))]. (length(cons(x,
- w)) = (1 + length(w))))
-
-axiom length_concat :
- (forall u:'a list. forall v:'a list [length(concat(u, v))].
- (length(concat(u, v)) = (length(u) + length(v))))
-
-axiom length_repeat :
- (forall w:'a list. forall n:int [length(repeat(w, n))]. ((0 <= n) ->
- (length(repeat(w, n)) = (n * length(w)))))
-
-axiom nth_cons :
- (forall k:int. forall x:'a. forall w:'a list [nth(cons(x, w), k)].
- ((k = 0) -> (nth(cons(x, w), k) = x)))
-
-axiom nth_cons1 :
- (forall k:int. forall x:'a. forall w:'a list [nth(cons(x, w), k)].
- ((not (k = 0)) -> (nth(cons(x, w), k) = nth(w, (k - 1)))))
-
-axiom nth_concat :
- (forall u:'a list. forall v:'a list. forall k:int [nth(concat(u, v), k)].
- ((k < length(u)) -> (nth(concat(u, v), k) = nth(u, k))))
-
-axiom nth_concat1 :
- (forall u:'a list. forall v:'a list. forall k:int [nth(concat(u, v), k)].
- ((not (k < length(u))) -> (nth(concat(u, v), k) = nth(v,
- (k - length(u))))))
-
-axiom nth_repeat :
- (forall n:int. forall k:int. forall w:'a list [nth(repeat(w, n), k)].
- (((0 <= k) and (k < (n * length(w)))) -> ((0 < length(w)) ->
- (nth(repeat(w, n), k) = nth(w, mod(k, length(w)))))))
-
-predicate vlist_eq(u: 'a list, v: 'a list) = ((length(u) = length(v)) and
- (forall i:int. (((0 <= i) and (i < length(u))) -> (nth(u, i) = nth(v,
- i)))))
-
-axiom extensionality :
- (forall u:'a list. forall v:'a list. (vlist_eq(u, v) -> (u = v)))
-
-axiom rw_nil_concat_left :
- (forall w:'a list [concat((nil : 'a list), w)]. (concat((nil : 'a list),
- w) = w))
-
-axiom rw_nil_concat_right :
- (forall w:'a list [concat(w, (nil : 'a list))]. (concat(w,
- (nil : 'a list)) = w))
-
-axiom rw_nil_repeat :
- (forall n:int [repeat((nil : 'a list), n)]. ((0 <= n) ->
- (repeat((nil : 'a list), n) = (nil : 'a list))))
-
-axiom rw_repeat_zero :
- (forall w:'a list [repeat(w, 0)]. (repeat(w, 0) = (nil : 'a list)))
-
-axiom rw_repeat_one : (forall w:'a list [repeat(w, 1)]. (repeat(w, 1) = w))
-
-logic repeat_box : 'a list, int -> 'a list
-
-axiom rw_repeat_box_unfold :
- (forall w:'a list. forall n:int [repeat_box(w, n)]. (repeat_box(w,
- n) = repeat(w, n)))
-
-axiom rw_repeat_plus_box_unfold :
- (forall w:'a list. forall a1:int. forall b:int [repeat_box(w, (a1 + b))].
- ((0 <= a1) -> ((0 <= b) -> (repeat_box(w, (a1 + b)) = concat(repeat(w, a1),
- repeat(w, b))))))
-
-axiom rw_repeat_plus_one_box_unfold :
- (forall w:'a list. forall n:int [repeat_box(w, n)]. ((0 < n) ->
- (repeat_box(w, n) = concat(repeat(w, (n - 1)), w))))
-
-axiom rw_repeat_plus_one_box_unfold1 :
- (forall w:'a list. forall n:int [repeat_box(w, n)]. ((0 < n) ->
- (repeat_box(w, (n + 1)) = concat(repeat(w, n), w))))
-
diff --git a/src/plugins/wp/share/ergo/Vset.mlw b/src/plugins/wp/share/ergo/Vset.mlw
deleted file mode 100644
index 250caa04958..00000000000
--- a/src/plugins/wp/share/ergo/Vset.mlw
+++ /dev/null
@@ -1,152 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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*)
-type 'a set
-
-logic empty : 'a set
-
-logic singleton : 'a -> 'a set
-
-logic ac union : 'a set, 'a set -> 'a set
-
-logic ac inter : 'a set, 'a set -> 'a set
-
-logic member : 'a, 'a set -> prop
-
-logic member_bool : 'a, 'a set -> bool
-
-logic range : int, int -> int set
-
-logic range_sup : int -> int set
-
-logic range_inf : int -> int set
-
-logic range_all : int set
-
-predicate eqset(a: 'a1 set, b: 'a1 set) =
- (forall x:'a1. (member(x, a) <-> member(x, b)))
-
-predicate subset(a: 'a1 set, b: 'a1 set) =
- (forall x:'a1. (member(x, a) -> member(x, b)))
-
-predicate disjoint(a: 'a1 set, b: 'a1 set) =
- (forall x:'a1. (member(x, a) -> (not member(x, b))))
-
-axiom member_bool1 :
- (forall x:'a.
- (forall s:'a set [member_bool(x, s)]. (member(x, s) -> (member_bool(x,
- s) = true))))
-
-axiom member_bool2 :
- (forall x:'a.
- (forall s:'a set [member_bool(x, s)]. ((not member(x, s)) ->
- (member_bool(x, s) = false))))
-
-axiom member_empty :
- (forall x:'a [member(x, (empty : 'a set))]. (not member(x,
- (empty : 'a set))))
-
-axiom member_singleton :
- (forall x:'a. forall y:'a [member(x, singleton(y))]. (member(x,
- singleton(y)) -> (x = y)))
-
-axiom member_singleton1 :
- (forall x:'a. forall y:'a [member(x, singleton(y))]. ((x = y) -> member(x,
- singleton(y))))
-
-axiom member_union :
- (forall x:'a.
- (forall a1:'a set. forall b:'a set [member(x, union(a1, b))]. (member(x,
- union(a1, b)) -> (member(x, a1) or member(x, b)))))
-
-axiom member_union1 :
- (forall x:'a.
- (forall a1:'a set. forall b:'a set [member(x, union(a1, b))]. ((member(x,
- a1) or member(x, b)) -> member(x, union(a1, b)))))
-
-axiom member_inter :
- (forall x:'a.
- (forall a1:'a set. forall b:'a set [member(x, inter(a1, b))]. (member(x,
- inter(a1, b)) -> member(x, a1))))
-
-axiom member_inter1 :
- (forall x:'a.
- (forall a1:'a set. forall b:'a set [member(x, inter(a1, b))]. (member(x,
- inter(a1, b)) -> member(x, b))))
-
-axiom member_inter2 :
- (forall x:'a.
- (forall a1:'a set. forall b:'a set [member(x, inter(a1, b))]. ((member(x,
- a1) and member(x, b)) -> member(x, inter(a1, b)))))
-
-axiom union_empty :
- (forall a:'a1 set [union(a, (empty : 'a1 set))| union((empty : 'a1 set),
- a)]. (union(a, (empty : 'a1 set)) = a))
-
-axiom union_empty1 :
- (forall a:'a1 set [union(a, (empty : 'a1 set))| union((empty : 'a1 set),
- a)]. (union((empty : 'a1 set), a) = a))
-
-axiom inter_empty :
- (forall a:'a1 set [inter(a, (empty : 'a1 set))| inter((empty : 'a1 set),
- a)]. (inter(a, (empty : 'a1 set)) = (empty : 'a1 set)))
-
-axiom inter_empty1 :
- (forall a:'a1 set [inter(a, (empty : 'a1 set))| inter((empty : 'a1 set),
- a)]. (inter((empty : 'a1 set), a) = (empty : 'a1 set)))
-
-axiom member_range :
- (forall x:int. forall a:int. forall b:int [member(x, range(a, b))].
- (member(x, range(a, b)) -> (a <= x)))
-
-axiom member_range1 :
- (forall x:int. forall a:int. forall b:int [member(x, range(a, b))].
- (member(x, range(a, b)) -> (x <= b)))
-
-axiom member_range2 :
- (forall x:int. forall a:int. forall b:int [member(x, range(a, b))].
- (((a <= x) and (x <= b)) -> member(x, range(a, b))))
-
-axiom member_range_sup :
- (forall x:int. forall a:int [member(x, range_sup(a))]. (member(x,
- range_sup(a)) -> (a <= x)))
-
-axiom member_range_sup1 :
- (forall x:int. forall a:int [member(x, range_sup(a))]. ((a <= x) ->
- member(x, range_sup(a))))
-
-axiom member_range_inf :
- (forall x:int. forall b:int [member(x, range_inf(b))]. (member(x,
- range_inf(b)) -> (x <= b)))
-
-axiom member_range_inf1 :
- (forall x:int. forall b:int [member(x, range_inf(b))]. ((x <= b) ->
- member(x, range_inf(b))))
-
-axiom member_range_all :
- (forall x:int [member(x, range_all)]. member(x, range_all))
-
diff --git a/src/plugins/wp/share/ergo/bool.Bool.mlw b/src/plugins/wp/share/ergo/bool.Bool.mlw
deleted file mode 100644
index e31c6ffa0dc..00000000000
--- a/src/plugins/wp/share/ergo/bool.Bool.mlw
+++ /dev/null
@@ -1,27 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** The theory BuiltIn_ must be appended to this file*)
-(** The theory Bool_ must be appended to this file*)
-function andb(x: bool, y: bool) : bool = match_bool(x, y, false)
-
-function orb(x: bool, y: bool) : bool = match_bool(x, true, y)
-
-function notb(x: bool) : bool = match_bool(x, false, true)
-
-function xorb(x: bool, y: bool) : bool = match_bool(x, notb(y), y)
-
-function implb(x: bool, y: bool) : bool = match_bool(x, y, true)
-
diff --git a/src/plugins/wp/share/ergo/int.Abs.mlw b/src/plugins/wp/share/ergo/int.Abs.mlw
deleted file mode 100644
index e03de293a71..00000000000
--- a/src/plugins/wp/share/ergo/int.Abs.mlw
+++ /dev/null
@@ -1,35 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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)))
-
diff --git a/src/plugins/wp/share/ergo/int.ComputerDivision.mlw b/src/plugins/wp/share/ergo/int.ComputerDivision.mlw
deleted file mode 100644
index cc9054d9d97..00000000000
--- a/src/plugins/wp/share/ergo/int.ComputerDivision.mlw
+++ /dev/null
@@ -1,49 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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*)
-logic div : int, int -> int
-
-logic mod : int, int -> int
-
-axiom Div_bound :
- (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (0 <= div(x, y))))
-
-axiom Div_bound1 :
- (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (div(x, y) <= x)))
-
-axiom Div_1 : (forall x:int. (div(x, 1) = x))
-
-axiom Mod_1 : (forall x:int. (mod(x, 1) = 0))
-
-axiom Div_inf :
- (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> (div(x, y) = 0)))
-
-axiom Mod_inf :
- (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> (mod(x, y) = x)))
-
-axiom Div_mult :
- (forall x:int. forall y:int. forall z:int [div(((x * y) + z), x)].
- (((0 < x) and ((0 <= y) and (0 <= z))) -> (div(((x * y) + z),
- x) = (y + div(z, x)))))
-
-axiom Mod_mult :
- (forall x:int. forall y:int. forall z:int [mod(((x * y) + z), x)].
- (((0 < x) and ((0 <= y) and (0 <= z))) -> (mod(((x * y) + z), x) = mod(z,
- x))))
-
diff --git a/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw b/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw
deleted file mode 100644
index 4fca9c6c375..00000000000
--- a/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw
+++ /dev/null
@@ -1,52 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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*)
-(** The theory int_ComputerDivision_ must be appended to this file*)
-
-axiom cdiv_cases :
- (forall n:int. forall d:int [div(n, d)]. ((0 <= n) -> ((0 < d) -> (div(n,
- d) = (n / d)))))
-
-axiom cdiv_cases1 :
- (forall n:int. forall d:int [div(n, d)]. ((n <= 0) -> ((0 < d) -> (div(n,
- d) = (-((-n) / d))))))
-
-axiom cdiv_cases2 :
- (forall n:int. forall d:int [div(n, d)]. ((0 <= n) -> ((d < 0) -> (div(n,
- d) = (-(n / (-d)))))))
-
-axiom cdiv_cases3 :
- (forall n:int. forall d:int [div(n, d)]. ((n <= 0) -> ((d < 0) -> (div(n,
- d) = ((-n) / (-d))))))
-
-axiom cmod_cases :
- (forall n:int. forall d:int [mod(n, d)]. ((0 <= n) -> ((0 < d) -> (mod(n,
- d) = (n % d)))))
-
-axiom cmod_cases1 :
- (forall n:int. forall d:int [mod(n, d)]. ((n <= 0) -> ((0 < d) -> (mod(n,
- d) = (-((-n) % d))))))
-
-axiom cmod_cases2 :
- (forall n:int. forall d:int [mod(n, d)]. ((0 <= n) -> ((d < 0) -> (mod(n,
- d) = (n % (-d))))))
-
-axiom cmod_cases3 :
- (forall n:int. forall d:int [mod(n, d)]. ((n <= 0) -> ((d < 0) -> (mod(n,
- d) = (-((-n) % (-d)))))))
diff --git a/src/plugins/wp/share/ergo/int.Int.mlw b/src/plugins/wp/share/ergo/int.Int.mlw
deleted file mode 100644
index 703c83034f6..00000000000
--- a/src/plugins/wp/share/ergo/int.Int.mlw
+++ /dev/null
@@ -1,18 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(* 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*)
diff --git a/src/plugins/wp/share/ergo/int.MinMax.mlw b/src/plugins/wp/share/ergo/int.MinMax.mlw
deleted file mode 100644
index 5bbc63f7812..00000000000
--- a/src/plugins/wp/share/ergo/int.MinMax.mlw
+++ /dev/null
@@ -1,52 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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 min_int : int, int -> int
-
-axiom min_def :
- (forall x:int. forall y:int. ((x <= y) -> (min_int(x, y) = x)))
-
-axiom min_def1 :
- (forall x:int. forall y:int. ((not (x <= y)) -> (min_int(x, y) = y)))
-
-logic max_int : int, int -> int
-
-axiom max_def :
- (forall x:int. forall y:int. ((x <= y) -> (max_int(x, y) = y)))
-
-axiom max_def1 :
- (forall x:int. forall y:int. ((not (x <= y)) -> (max_int(x, y) = x)))
-
-axiom Min_r : (forall x:int. forall y:int. ((y <= x) -> (min_int(x, y) = y)))
-
-axiom Max_l : (forall x:int. forall y:int. ((y <= x) -> (max_int(x, y) = x)))
-
-axiom Min_comm :
- (forall x:int. forall y:int. (min_int(x, y) = min_int(y, x)))
-
-axiom Max_comm :
- (forall x:int. forall y:int. (max_int(x, y) = max_int(y, x)))
-
-axiom Min_assoc :
- (forall x:int. forall y:int. forall z:int. (min_int(min_int(x, y),
- z) = min_int(x, min_int(y, z))))
-
-axiom Max_assoc :
- (forall x:int. forall y:int. forall z:int. (max_int(max_int(x, y),
- z) = max_int(x, max_int(y, z))))
-
diff --git a/src/plugins/wp/share/ergo/map.Const.mlw b/src/plugins/wp/share/ergo/map.Const.mlw
deleted file mode 100644
index d93ab7e6468..00000000000
--- a/src/plugins/wp/share/ergo/map.Const.mlw
+++ /dev/null
@@ -1,23 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** The theory BuiltIn_ must be appended to this file*)
-(** The theory Bool_ must be appended to this file*)
-(** The theory map_Map_ must be appended to this file*)
-logic const : 'b -> ('a,'b) farray
-
-axiom const_def :
- (forall v:'b. forall us:'a. (((const(v) : ('a,'b) farray)[us]) = v))
-
diff --git a/src/plugins/wp/share/ergo/map.Map.mlw b/src/plugins/wp/share/ergo/map.Map.mlw
deleted file mode 100644
index ddb3b00ec7e..00000000000
--- a/src/plugins/wp/share/ergo/map.Map.mlw
+++ /dev/null
@@ -1,17 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** The theory BuiltIn_ must be appended to this file*)
-(** The theory Bool_ must be appended to this file*)
diff --git a/src/plugins/wp/share/ergo/real.Abs.mlw b/src/plugins/wp/share/ergo/real.Abs.mlw
deleted file mode 100644
index 1340bfad895..00000000000
--- a/src/plugins/wp/share/ergo/real.Abs.mlw
+++ /dev/null
@@ -1,48 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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*)
-logic abs_real : real -> real
-
-axiom abs_def : (forall x:real. ((0.0 <= x) -> (abs_real(x) = x)))
-
-axiom abs_def1 : (forall x:real. ((not (0.0 <= x)) -> (abs_real(x) = (-x))))
-
-axiom Abs_le :
- (forall x:real. forall y:real. ((abs_real(x) <= y) -> ((-y) <= x)))
-
-axiom Abs_le1 :
- (forall x:real. forall y:real. ((abs_real(x) <= y) -> (x <= y)))
-
-axiom Abs_le2 :
- (forall x:real. forall y:real. ((((-y) <= x) and (x <= y)) ->
- (abs_real(x) <= y)))
-
-axiom Abs_pos : (forall x:real. (0.0 <= abs_real(x)))
-
-axiom Abs_sum :
- (forall x:real. forall y:real.
- (abs_real((x + y)) <= (abs_real(x) + abs_real(y))))
-
-axiom Abs_prod :
- (forall x:real. forall y:real.
- (abs_real((x * y)) = (abs_real(x) * abs_real(y))))
-
-axiom triangular_inequality :
- (forall x:real. forall y:real. forall z:real.
- (abs_real((x - z)) <= (abs_real((x - y)) + abs_real((y - z)))))
-
diff --git a/src/plugins/wp/share/ergo/real.ExpLog.mlw b/src/plugins/wp/share/ergo/real.ExpLog.mlw
deleted file mode 100644
index a600122dfd8..00000000000
--- a/src/plugins/wp/share/ergo/real.ExpLog.mlw
+++ /dev/null
@@ -1,41 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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*)
-logic exp : real -> real
-
-axiom Exp_zero : (exp(0.0) = 1.0)
-
-axiom Exp_sum :
- (forall x:real. forall y:real. (exp((x + y)) = (exp(x) * exp(y))))
-
-logic log : real -> real
-
-axiom Log_one : (log(1.0) = 0.0)
-
-axiom Log_mul :
- (forall x:real. forall y:real. (((0.0 < x) and (0.0 < y)) ->
- (log((x * y)) = (log(x) + log(y)))))
-
-axiom Log_exp : (forall x:real. (log(exp(x)) = x))
-
-axiom Exp_log : (forall x:real. ((0.0 < x) -> (exp(log(x)) = x)))
-
-function log2(x: real) : real = (log(x) / log(2.0))
-
-function log10(x: real) : real = (log(x) / log(10.0))
-
diff --git a/src/plugins/wp/share/ergo/real.FromInt.mlw b/src/plugins/wp/share/ergo/real.FromInt.mlw
deleted file mode 100644
index a1f51341456..00000000000
--- a/src/plugins/wp/share/ergo/real.FromInt.mlw
+++ /dev/null
@@ -1,45 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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))))
-
-axiom Injective :
- (forall x:int. forall y:int. ((from_int(x) = from_int(y)) -> (x = y)))
-
-axiom Monotonic :
- (forall x:int. forall y:int. ((x <= y) -> (from_int(x) <= from_int(y))))
-
diff --git a/src/plugins/wp/share/ergo/real.Hyperbolic.mlw b/src/plugins/wp/share/ergo/real.Hyperbolic.mlw
deleted file mode 100644
index 14a08dae73f..00000000000
--- a/src/plugins/wp/share/ergo/real.Hyperbolic.mlw
+++ /dev/null
@@ -1,40 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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 theory real_Square_ must be appended to this file*)
-(** The theory real_ExpLog_ must be appended to this file*)
-function sinh(x: real) : real = (0.5 * (exp(x) - exp((-x))))
-
-function cosh(x: real) : real = (0.5 * (exp(x) + exp((-x))))
-
-function tanh(x: real) : real = (sinh(x) / cosh(x))
-
-function asinh(x: real) : real = log((x + sqrt((sqr(x) + 1.0))))
-
-logic acosh : real -> real
-
-axiom Acosh_def :
- (forall x:real. ((1.0 <= x) ->
- (acosh(x) = log((x + sqrt((sqr(x) - 1.0)))))))
-
-logic atanh : real -> real
-
-axiom Atanh_def :
- (forall x:real. ((((- 1.0) < x) and (x < 1.0)) ->
- (atanh(x) = (0.5 * log(((1.0 + x) / (1.0 - x)))))))
-
diff --git a/src/plugins/wp/share/ergo/real.MinMax.mlw b/src/plugins/wp/share/ergo/real.MinMax.mlw
deleted file mode 100644
index d1438d67fd2..00000000000
--- a/src/plugins/wp/share/ergo/real.MinMax.mlw
+++ /dev/null
@@ -1,54 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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*)
-logic min_real : real, real -> real
-
-axiom min_def :
- (forall x:real. forall y:real. ((x <= y) -> (min_real(x, y) = x)))
-
-axiom min_def1 :
- (forall x:real. forall y:real. ((not (x <= y)) -> (min_real(x, y) = y)))
-
-logic max_real : real, real -> real
-
-axiom max_def :
- (forall x:real. forall y:real. ((x <= y) -> (max_real(x, y) = y)))
-
-axiom max_def1 :
- (forall x:real. forall y:real. ((not (x <= y)) -> (max_real(x, y) = x)))
-
-axiom Min_r :
- (forall x:real. forall y:real. ((y <= x) -> (min_real(x, y) = y)))
-
-axiom Max_l :
- (forall x:real. forall y:real. ((y <= x) -> (max_real(x, y) = x)))
-
-axiom Min_comm :
- (forall x:real. forall y:real. (min_real(x, y) = min_real(y, x)))
-
-axiom Max_comm :
- (forall x:real. forall y:real. (max_real(x, y) = max_real(y, x)))
-
-axiom Min_assoc :
- (forall x:real. forall y:real. forall z:real. (min_real(min_real(x, y),
- z) = min_real(x, min_real(y, z))))
-
-axiom Max_assoc :
- (forall x:real. forall y:real. forall z:real. (max_real(max_real(x, y),
- z) = max_real(x, max_real(y, z))))
-
diff --git a/src/plugins/wp/share/ergo/real.Polar.mlw b/src/plugins/wp/share/ergo/real.Polar.mlw
deleted file mode 100644
index 4c953665ad7..00000000000
--- a/src/plugins/wp/share/ergo/real.Polar.mlw
+++ /dev/null
@@ -1,31 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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 theory real_Abs_ must be appended to this file*)
-(** The theory real_Square_ must be appended to this file*)
-(** The theory real_Trigonometry_ must be appended to this file*)
-function hypot(x: real, y: real) : real = sqrt((sqr(x) + sqr(y)))
-
-logic atan2 : real, real -> real
-
-axiom X_from_polar :
- (forall x:real. forall y:real. (x = (hypot(x, y) * cos(atan2(y, x)))))
-
-axiom Y_from_polar :
- (forall x:real. forall y:real. (y = (hypot(x, y) * sin(atan2(y, x)))))
-
diff --git a/src/plugins/wp/share/ergo/real.PowerReal.mlw b/src/plugins/wp/share/ergo/real.PowerReal.mlw
deleted file mode 100644
index 140f336820e..00000000000
--- a/src/plugins/wp/share/ergo/real.PowerReal.mlw
+++ /dev/null
@@ -1,50 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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_Exponentiation_ must be appended to this file*)
-(** The theory int_Power_ must be appended to this file*)
-(** The theory real_Real_ must be appended to this file*)
-(** The theory real_FromInt_ must be appended to this file*)
-(** The theory real_Square_ must be appended to this file*)
-(** The theory real_ExpLog_ must be appended to this file*)
-logic pow : real, real -> real
-
-axiom Pow_def :
- (forall x:real. forall y:real. ((0.0 < x) -> (pow(x,
- y) = exp((y * log(x))))))
-
-axiom Pow_pos :
- (forall x:real. forall y:real. ((0.0 < x) -> (0.0 < pow(x, y))))
-
-axiom Pow_plus :
- (forall x:real. forall y:real. forall z:real. ((0.0 < z) -> (pow(z,
- (x + y)) = (pow(z, x) * pow(z, y)))))
-
-axiom Pow_mult :
- (forall x:real. forall y:real. forall z:real. ((0.0 < x) -> (pow(pow(x,
- y), z) = pow(x, (y * z)))))
-
-axiom Pow_x_zero : (forall x:real. ((0.0 < x) -> (pow(x, 0.0) = 1.0)))
-
-axiom Pow_x_one : (forall x:real. ((0.0 < x) -> (pow(x, 1.0) = x)))
-
-axiom Pow_one_y : (forall y:real. (pow(1.0, y) = 1.0))
-
-axiom Pow_x_two : (forall x:real. ((0.0 < x) -> (pow(x, 2.0) = sqr(x))))
-
-axiom Pow_half : (forall x:real. ((0.0 < x) -> (pow(x, 0.5) = sqrt(x))))
diff --git a/src/plugins/wp/share/ergo/real.Real.mlw b/src/plugins/wp/share/ergo/real.Real.mlw
deleted file mode 100644
index db80917b1b0..00000000000
--- a/src/plugins/wp/share/ergo/real.Real.mlw
+++ /dev/null
@@ -1,42 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(* 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))))
-
diff --git a/src/plugins/wp/share/ergo/real.RealInfix.mlw b/src/plugins/wp/share/ergo/real.RealInfix.mlw
deleted file mode 100644
index 5134839728a..00000000000
--- a/src/plugins/wp/share/ergo/real.RealInfix.mlw
+++ /dev/null
@@ -1,18 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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*)
diff --git a/src/plugins/wp/share/ergo/real.Square.mlw b/src/plugins/wp/share/ergo/real.Square.mlw
deleted file mode 100644
index 4eaec010938..00000000000
--- a/src/plugins/wp/share/ergo/real.Square.mlw
+++ /dev/null
@@ -1,36 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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*)
-function sqr(x: real) : real = (x * x)
-
-logic sqrt : real -> real
-
-axiom Sqrt_positive : (forall x:real. ((0.0 <= x) -> (0.0 <= sqrt(x))))
-
-axiom Sqrt_square : (forall x:real. ((0.0 <= x) -> (sqr(sqrt(x)) = x)))
-
-axiom Square_sqrt : (forall x:real. ((0.0 <= x) -> (sqrt((x * x)) = x)))
-
-axiom Sqrt_mul :
- (forall x:real. forall y:real. (((0.0 <= x) and (0.0 <= y)) ->
- (sqrt((x * y)) = (sqrt(x) * sqrt(y)))))
-
-axiom Sqrt_le :
- (forall x:real. forall y:real. (((0.0 <= x) and (x <= y)) ->
- (sqrt(x) <= sqrt(y))))
-
diff --git a/src/plugins/wp/share/ergo/real.Trigonometry.mlw b/src/plugins/wp/share/ergo/real.Trigonometry.mlw
deleted file mode 100644
index 93f357ea6d8..00000000000
--- a/src/plugins/wp/share/ergo/real.Trigonometry.mlw
+++ /dev/null
@@ -1,75 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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 theory real_Abs_ must be appended to this file*)
-(** The theory real_Square_ must be appended to this file*)
-logic cos : real -> real
-
-logic sin : real -> real
-
-axiom Pythagorean_identity :
- (forall x:real. ((sqr(cos(x)) + sqr(sin(x))) = 1.0))
-
-axiom Cos_le_one : (forall x:real. (abs_real(cos(x)) <= 1.0))
-
-axiom Sin_le_one : (forall x:real. (abs_real(sin(x)) <= 1.0))
-
-axiom Cos_0 : (cos(0.0) = 1.0)
-
-axiom Sin_0 : (sin(0.0) = 0.0)
-
-logic pi : real
-
-axiom Pi_double_precision_bounds : (0x1.921fb54442d18p1 < pi)
-
-axiom Pi_double_precision_bounds1 : (pi < 0x1.921fb54442d19p1)
-
-axiom Cos_pi : (cos(pi) = (- 1.0))
-
-axiom Sin_pi : (sin(pi) = 0.0)
-
-axiom Cos_pi2 : (cos((0.5 * pi)) = 0.0)
-
-axiom Sin_pi2 : (sin((0.5 * pi)) = 1.0)
-
-axiom Cos_plus_pi : (forall x:real. (cos((x + pi)) = (-cos(x))))
-
-axiom Sin_plus_pi : (forall x:real. (sin((x + pi)) = (-sin(x))))
-
-axiom Cos_plus_pi2 : (forall x:real. (cos((x + (0.5 * pi))) = (-sin(x))))
-
-axiom Sin_plus_pi2 : (forall x:real. (sin((x + (0.5 * pi))) = cos(x)))
-
-axiom Cos_neg : (forall x:real. (cos((-x)) = cos(x)))
-
-axiom Sin_neg : (forall x:real. (sin((-x)) = (-sin(x))))
-
-axiom Cos_sum :
- (forall x:real. forall y:real.
- (cos((x + y)) = ((cos(x) * cos(y)) - (sin(x) * sin(y)))))
-
-axiom Sin_sum :
- (forall x:real. forall y:real.
- (sin((x + y)) = ((sin(x) * cos(y)) + (cos(x) * sin(y)))))
-
-function tan(x: real) : real = (sin(x) / cos(x))
-
-logic atan : real -> real
-
-axiom Tan_atan : (forall x:real. (tan(atan(x)) = x))
-
diff --git a/src/plugins/wp/share/ergo/real.Truncate.mlw b/src/plugins/wp/share/ergo/real.Truncate.mlw
deleted file mode 100644
index f86ba0df6fb..00000000000
--- a/src/plugins/wp/share/ergo/real.Truncate.mlw
+++ /dev/null
@@ -1,73 +0,0 @@
-(**************************************************************************)
-(* *)
-(* The Why3 Verification Platform / The Why3 Development Team *)
-(* Copyright 2010-2019 -- 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 the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** 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*)
-(** The theory real_FromInt_ must be appended to this file*)
-logic truncate : real -> int
-
-axiom Truncate_int : (forall i:int. (truncate(from_int(i)) = i))
-
-axiom Truncate_down_pos :
- (forall x:real. ((0.0 <= x) -> (from_int(truncate(x)) <= x)))
-
-axiom Truncate_down_pos1 :
- (forall x:real. ((0.0 <= x) -> (x < from_int((truncate(x) + 1)))))
-
-axiom Truncate_up_neg :
- (forall x:real. ((x <= 0.0) -> (from_int((truncate(x) - 1)) < x)))
-
-axiom Truncate_up_neg1 :
- (forall x:real. ((x <= 0.0) -> (x <= from_int(truncate(x)))))
-
-axiom Real_of_truncate :
- (forall x:real. ((x - 1.0) <= from_int(truncate(x))))
-
-axiom Real_of_truncate1 :
- (forall x:real. (from_int(truncate(x)) <= (x + 1.0)))
-
-axiom Truncate_monotonic :
- (forall x:real. forall y:real. ((x <= y) -> (truncate(x) <= truncate(y))))
-
-axiom Truncate_monotonic_int1 :
- (forall x:real. forall i:int. ((x <= from_int(i)) -> (truncate(x) <= i)))
-
-axiom Truncate_monotonic_int2 :
- (forall x:real. forall i:int. ((from_int(i) <= x) -> (i <= truncate(x))))
-
-logic floor : real -> int
-
-logic ceil : real -> int
-
-axiom Floor_int : (forall i:int. (floor(from_int(i)) = i))
-
-axiom Ceil_int : (forall i:int. (ceil(from_int(i)) = i))
-
-axiom Floor_down : (forall x:real. (from_int(floor(x)) <= x))
-
-axiom Floor_down1 : (forall x:real. (x < from_int((floor(x) + 1))))
-
-axiom Ceil_up : (forall x:real. (from_int((ceil(x) - 1)) < x))
-
-axiom Ceil_up1 : (forall x:real. (x <= from_int(ceil(x))))
-
-axiom Floor_monotonic :
- (forall x:real. forall y:real. ((x <= y) -> (floor(x) <= floor(y))))
-
-axiom Ceil_monotonic :
- (forall x:real. forall y:real. ((x <= y) -> (ceil(x) <= ceil(y))))
-
--
GitLab