From a00483fe5f78bed0029c5827cc748ace5dee85ab Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 12 Apr 2017 23:21:52 +0200
Subject: [PATCH] [WP] Relocatable sig
---
src/plugins/wp/StmtCompiler.ml | 28 +++++++++++++--------------
src/plugins/wp/StmtCompiler.mli | 34 +++++++++++++++++++--------------
2 files changed, 33 insertions(+), 29 deletions(-)
diff --git a/src/plugins/wp/StmtCompiler.ml b/src/plugins/wp/StmtCompiler.ml
index 7d07d794a34..53534a42a13 100644
--- a/src/plugins/wp/StmtCompiler.ml
+++ b/src/plugins/wp/StmtCompiler.ml
@@ -29,7 +29,6 @@ sig
module M : Model
-
module Node : sig
type t
module Map : Qed.Idxmap.S with type key = t
@@ -43,29 +42,28 @@ sig
module E : sig
type t
val create : M.sigma sequence -> F.pred -> t
- (** Bundle an equation with the sigma sequence that created it *)
+ val get : t -> F.pred
+ val reads : t -> M.domain
+ val writes : t -> M.domain
val relocate : M.sigma sequence -> t -> t
- val get: t -> F.pred
end
- (** Relocatable predicate *)
- module P :
- sig
- type t
- val create : M.sigma Node.Map.t -> F.pred -> t
- (** Bundle an equation with the sigma sequence that created it. *)
- val relocate : M.sigma Node.Map.t -> t -> t
- val get: t -> F.pred
- end
-
- (** Relocatable condition *)
module C :
sig
type t
val create : M.sigma -> F.pred -> t
- (** Bundle an equation with the sigma sequence that created it. *)
+ val get : t -> F.pred
+ val reads : t -> M.domain
val relocate : M.sigma -> t -> t
+ end
+
+ module P :
+ sig
+ type t
+ val create : M.sigma Node.Map.t -> F.pred -> t
val get: t -> F.pred
+ val reads : t -> M.domain Node.Map.t
+ val relocate : M.sigma Node.Map.t -> t -> t
end
type cfg
diff --git a/src/plugins/wp/StmtCompiler.mli b/src/plugins/wp/StmtCompiler.mli
index 973b33d11d8..2dddde5ca98 100644
--- a/src/plugins/wp/StmtCompiler.mli
+++ b/src/plugins/wp/StmtCompiler.mli
@@ -73,9 +73,9 @@ sig
end
type node = Node.t
-
- val node : unit -> node
+
(** fresh node *)
+ val node : unit -> node
(** {2 Relocatable Formulae}
Can be created once with fresh environment, and used several
@@ -84,31 +84,37 @@ sig
(** Relocatable set of equations *)
module E : sig
type t
- val create : M.sigma sequence -> F.pred -> t
+
(** Bundle an equation with the sigma sequence that created it *)
+ val create : M.sigma sequence -> F.pred -> t
+ val get : t -> F.pred
+ val reads : t -> M.domain
+ val writes : t -> M.domain
val relocate : M.sigma sequence -> t -> t
- val get: t -> F.pred
end
- (** Relocatable predicate *)
- module P :
+ (** Relocatable condition *)
+ module C :
sig
type t
- val create : M.sigma Node.Map.t -> F.pred -> t
+
(** Bundle an equation with the sigma sequence that created it. *)
- val relocate : M.sigma Node.Map.t -> t -> t
- val get: t -> F.pred
+ val create : M.sigma -> F.pred -> t
+ val get : t -> F.pred
+ val reads : t -> M.domain
+ val relocate : M.sigma -> t -> t
end
-
- (** Relocatable condition *)
- module C :
+ (** Relocatable predicate *)
+ module P :
sig
type t
- val create : M.sigma -> F.pred -> t
+
(** Bundle an equation with the sigma sequence that created it. *)
- val relocate : M.sigma -> t -> t
+ val create : M.sigma Node.Map.t -> F.pred -> t
val get: t -> F.pred
+ val reads : t -> M.domain Node.Map.t
+ val relocate : M.sigma Node.Map.t -> t -> t
end
type cfg (** Structured collection of traces. *)
--
GitLab