From 73113843b69378d14de3285e23a1e9bd5f88534c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 22 Jan 2021 13:01:24 +0100
Subject: [PATCH] [wp] fix legacy generator selection
---
src/plugins/wp/Generator.ml | 2 +-
src/plugins/wp/Generator.mli | 3 ---
2 files changed, 1 insertion(+), 4 deletions(-)
diff --git a/src/plugins/wp/Generator.ml b/src/plugins/wp/Generator.ml
index 2af03b61f95..28ffe5d6212 100644
--- a/src/plugins/wp/Generator.ml
+++ b/src/plugins/wp/Generator.ml
@@ -64,7 +64,7 @@ let create
() : Wpo.generator =
let default f = function Some v -> v | None -> f () in
let dump = default Wp_parameters.Dump.get dump in
- let legacy = default Wp_parameters.Dump.get legacy in
+ let legacy = default Wp_parameters.Legacy.get legacy in
let driver = default Driver.load_driver driver in
let setup = default user_setup setup in
if legacy then
diff --git a/src/plugins/wp/Generator.mli b/src/plugins/wp/Generator.mli
index fc70c5d2fed..ef3b2b2dcee 100644
--- a/src/plugins/wp/Generator.mli
+++ b/src/plugins/wp/Generator.mli
@@ -20,9 +20,6 @@
(* *)
(*****************************************t*********************************)
-open Cil_types
-open Wp_parameters
-
(* -------------------------------------------------------------------------- *)
(* --- WP Computer (main entry points) --- *)
(* -------------------------------------------------------------------------- *)
--
GitLab