From 21cfcf582f5db64d254adfbe6a2fe3af95f3613e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Wed, 18 Sep 2019 11:44:29 +0200 Subject: [PATCH] [wp/alt-ergo] fix resources for div & bits --- src/plugins/wp/share/ergo/Cbits.mlw | 8 +------- src/plugins/wp/share/ergo/Qed.mlw | 2 -- .../wp/share/ergo/int.ComputerOfEuclideanDivision.mlw | 3 +-- src/plugins/wp/share/ergo/int.EuclideanDivision.mlw | 5 ----- src/plugins/wp/share/wp.driver | 1 - 5 files changed, 2 insertions(+), 17 deletions(-) delete mode 100644 src/plugins/wp/share/ergo/int.EuclideanDivision.mlw diff --git a/src/plugins/wp/share/ergo/Cbits.mlw b/src/plugins/wp/share/ergo/Cbits.mlw index 1bf6749cffe..4b2b2d6ed43 100644 --- a/src/plugins/wp/share/ergo/Cbits.mlw +++ b/src/plugins/wp/share/ergo/Cbits.mlw @@ -27,14 +27,12 @@ (** 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_EuclideanDivision_ 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 for_drivers_ComputerOfEuclideanDivision_ must be appended to this file*) (** The theory Cint_ must be appended to this file*) -<<<<<<< HEAD + logic bit_testb : int, int -> bool logic bit_test : int, int -> prop @@ -51,8 +49,6 @@ logic lsl : int, int -> int logic lsr : int, int -> int -||||||| merged common ancestors -======= axiom lnot_bool : (lnot(0) = (-1)) axiom lnot_bool1 : (lnot((-1)) = 0) @@ -87,7 +83,6 @@ 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)) ->>>>>>> origin/master axiom bit_test_def : (forall x:int. forall k:int [bit_testb(x, k)]. ((bit_testb(x, k) = true) -> bit_test(x, k))) @@ -536,4 +531,3 @@ axiom lor_addition : 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/Qed.mlw b/src/plugins/wp/share/ergo/Qed.mlw index 0537e4c35cb..eeb3d92f882 100644 --- a/src/plugins/wp/share/ergo/Qed.mlw +++ b/src/plugins/wp/share/ergo/Qed.mlw @@ -26,12 +26,10 @@ (** 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_EuclideanDivision_ 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 for_drivers_ComputerOfEuclideanDivision_ must be appended to this file*) logic match_bool : bool, 'a, 'a -> 'a axiom match_bool1 : diff --git a/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw b/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw index ab250caabbf..4fca9c6c375 100644 --- a/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw +++ b/src/plugins/wp/share/ergo/int.ComputerOfEuclideanDivision.mlw @@ -17,8 +17,8 @@ (** 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_EuclideanDivision_ 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))))) @@ -50,4 +50,3 @@ axiom cmod_cases2 : 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.EuclideanDivision.mlw b/src/plugins/wp/share/ergo/int.EuclideanDivision.mlw deleted file mode 100644 index 7390354ffaa..00000000000 --- a/src/plugins/wp/share/ergo/int.EuclideanDivision.mlw +++ /dev/null @@ -1,5 +0,0 @@ -(* 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*) diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver index 271c470da94..84cccb44f4c 100644 --- a/src/plugins/wp/share/wp.driver +++ b/src/plugins/wp/share/wp.driver @@ -41,7 +41,6 @@ why3.import += "frama_c_wp.qed.Qed"; altergo.file += "ergo/int.Int.mlw"; altergo.file += "ergo/int.Abs.mlw"; altergo.file += "ergo/int.ComputerDivision.mlw"; -altergo.file += "ergo/int.EuclideanDivision.mlw"; altergo.file += "ergo/int.ComputerOfEuclideanDivision.mlw"; altergo.file += "ergo/real.Real.mlw"; altergo.file += "ergo/real.RealInfix.mlw"; -- GitLab