From 0afb3b0a96df987c3e4cfa4ea354392bcd9d78e3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 13 Sep 2019 14:39:00 +0200
Subject: [PATCH] [wp] fix division driver for native alt-ergo
---
src/plugins/qed/export_altergo.ml | 4 ++--
src/plugins/wp/share/ergo/int.EuclideanDivision.mlw | 5 -----
src/plugins/wp/share/wp.driver | 1 -
3 files changed, 2 insertions(+), 8 deletions(-)
delete mode 100644 src/plugins/wp/share/ergo/int.EuclideanDivision.mlw
diff --git a/src/plugins/qed/export_altergo.ml b/src/plugins/qed/export_altergo.ml
index 52864b8b166..70087ff2d4c 100644
--- a/src/plugins/qed/export_altergo.ml
+++ b/src/plugins/qed/export_altergo.ml
@@ -114,8 +114,8 @@ struct
method op_add (_:amode) = Assoc "+"
method op_sub (_:amode) = Assoc "-"
method op_mul (_:amode) = Assoc "*"
- method op_div = function Aint -> Call "comp_div" | Areal -> Op "/"
- method op_mod = function Aint -> Call "comp_mod" | Areal -> Call "rmod"
+ method op_div = function Aint -> Call "div" | Areal -> Op "/"
+ method op_mod = function Aint -> Call "mod" | Areal -> Call "rmod"
method op_eq cmode _amode =
match cmode with
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