From de7994155042c24d4dc4f0108d7232f9ee2753e4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 15 Jan 2020 11:28:46 +0100
Subject: [PATCH] [WP] Removes an unused parameter from the LogicAssigns.Make
functor.
---
src/plugins/wp/Factory.ml | 2 +-
src/plugins/wp/LogicAssigns.ml | 1 -
src/plugins/wp/LogicAssigns.mli | 1 -
3 files changed, 1 insertion(+), 3 deletions(-)
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 5b9e54a4366..3fde0d76ebc 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -242,7 +242,7 @@ module MakeCompiler(M:Sigs.Model) = struct
module M = M
module C = CodeSemantics.Make(M)
module L = LogicSemantics.Make(M)
- module A = LogicAssigns.Make(M)(C)(L)
+ module A = LogicAssigns.Make(M)(L)
end
module Comp_Region = MakeCompiler(Register(Static)(MemRegion))
diff --git a/src/plugins/wp/LogicAssigns.ml b/src/plugins/wp/LogicAssigns.ml
index 8da52bbfe32..fe9eab80a7c 100644
--- a/src/plugins/wp/LogicAssigns.ml
+++ b/src/plugins/wp/LogicAssigns.ml
@@ -24,7 +24,6 @@ open Sigs
module Make
( M : Sigs.Model )
- ( C : Sigs.CodeSemantics with module M = M )
( L : Sigs.LogicSemantics with module M = M ) =
struct
diff --git a/src/plugins/wp/LogicAssigns.mli b/src/plugins/wp/LogicAssigns.mli
index 92cd1d2006b..4ff9a6fb815 100644
--- a/src/plugins/wp/LogicAssigns.mli
+++ b/src/plugins/wp/LogicAssigns.mli
@@ -22,6 +22,5 @@
module Make
( M : Sigs.Model )
- ( C : Sigs.CodeSemantics with module M = M )
( L : Sigs.LogicSemantics with module M = M ) :
Sigs.LogicAssigns with module M = M and module L = L
--
GitLab