From ac7dcba6f14281ed5de2b98314abd606fb9c9493 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 21 Aug 2019 12:05:33 +0200
Subject: [PATCH] [wp/region] move frame conditions to sigs
---
src/plugins/wp/MemLoader.ml | 2 --
src/plugins/wp/MemLoader.mli | 10 ----------
src/plugins/wp/Sigs.ml | 10 ++++++++++
3 files changed, 10 insertions(+), 12 deletions(-)
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index bfe4d75df24..2fb65326e84 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -39,8 +39,6 @@ open Sigs
let cluster () =
Definitions.cluster ~id:"Compound" ~title:"Memory Compound Loader" ()
-type frame = string * Definitions.trigger list * pred list * term * term
-
module type Model =
sig
diff --git a/src/plugins/wp/MemLoader.mli b/src/plugins/wp/MemLoader.mli
index 6f94c256955..ddc2677cbc0 100644
--- a/src/plugins/wp/MemLoader.mli
+++ b/src/plugins/wp/MemLoader.mli
@@ -32,16 +32,6 @@ open Sigs
val cluster : unit -> cluster
-(** Frame Conditions.
- Consider a function [phi(m)] over memory [m],
- we want memories [m1,m2] and condition [p] such that
- [p(m1,m2) -> phi(m1) = phi(m2)].
- - [name] used for generating lemma
- - [triggers] for the lemma
- - [conditions] for the frame lemma to hold
- - [mem1,mem2] to two memories for which the lemma holds *)
-type frame = string * Definitions.trigger list * pred list * term * term
-
(** Loader Model for Atomic Values *)
module type Model =
sig
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 6fc72a241aa..a91e7770466 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -85,6 +85,16 @@ type 'a result =
(** Polarity of predicate compilation *)
type polarity = [ `Positive | `Negative | `NoPolarity ]
+(** Frame Conditions.
+ Consider a function [phi(m)] over memory [m],
+ we want memories [m1,m2] and condition [p] such that
+ [p(m1,m2) -> phi(m1) = phi(m2)].
+ - [name] used for generating lemma
+ - [triggers] for the lemma
+ - [conditions] for the frame lemma to hold
+ - [mem1,mem2] to two memories for which the lemma holds *)
+type frame = string * Definitions.trigger list * pred list * term * term
+
(* -------------------------------------------------------------------------- *)
(** {1 Reversing Models}
--
GitLab