From 3e483d2bad133e2c69848125cb7db2b1a3dcfe90 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 27 Aug 2019 14:04:11 +0200
Subject: [PATCH] [wp] fix equality clusters
---
src/plugins/wp/Cvalues.ml | 13 ++++++++-----
src/plugins/wp/Definitions.ml | 2 ++
src/plugins/wp/Definitions.mli | 1 +
src/plugins/wp/MemTyped.ml | 6 ++----
4 files changed, 13 insertions(+), 9 deletions(-)
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index 79ef3606a8d..f2adbc17b9b 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -252,7 +252,6 @@ module EQARRAYDEF = WpContext.StaticGenerator(Matrix.NATURAL)
let lfun = Lang.generated_f ~sort:Logic.Sprop "EqArray%s_%s"
(Matrix.id ds) (Matrix.natural_id te)
in
- let cluster = Definitions.matrix te in
let denv = Matrix.denv ds in
let tau = Matrix.tau te ds in
let xa = Lang.freshvar ~basename:"T" tau in
@@ -269,7 +268,7 @@ module EQARRAYDEF = WpContext.StaticGenerator(Matrix.NATURAL)
d_lfun = lfun ; d_types = 0 ;
d_params = denv.size_var @ [xa ; xb ] ;
d_definition = Predicate(Def,definition) ;
- d_cluster = cluster ;
+ d_cluster = Definitions.dummy () ;
}
end)
@@ -281,7 +280,9 @@ module EQARRAY = WpContext.Generator(Matrix.NATURAL)
type data = Lang.lfun
let compile mtx =
let def = EQARRAYDEF.get mtx in
- Definitions.define_symbol def ; def.d_lfun
+ let d_cluster = Definitions.matrix (fst mtx) in
+ Definitions.define_symbol { def with d_cluster } ;
+ def.d_lfun
end)
(* -------------------------------------------------------------------------- *)
@@ -310,7 +311,7 @@ module EQCOMPDEF = WpContext.StaticGenerator(Cil_datatype.Compinfo)
Lang.F.set_builtin lfun reduce_eqcomp ;
{
d_lfun = lfun ; d_types = 0 ; d_params = [xa;xb] ;
- d_cluster = Definitions.compinfo c ;
+ d_cluster = Definitions.dummy () ;
d_definition = Predicate(Def,def) ;
}
end)
@@ -322,7 +323,9 @@ module EQCOMP = WpContext.Generator(Cil_datatype.Compinfo)
type data = Lang.lfun
let compile ci =
let def = EQCOMPDEF.get ci in
- Definitions.define_symbol def ; def.d_lfun
+ let d_cluster = Definitions.compinfo ci in
+ Definitions.define_symbol { def with d_cluster } ;
+ def.d_lfun
end)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index 21bb43939f9..30f0dbaf27f 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -212,6 +212,8 @@ let newcluster ~id ?title ?position () =
let cluster ~id ?title ?position () =
Cluster.memoize (fun id -> newcluster ~id ?title ?position ()) id
+let dummy () = cluster ~id:"dummy" ()
+
let axiomatic ax =
Cluster.memoize
(fun id ->
diff --git a/src/plugins/wp/Definitions.mli b/src/plugins/wp/Definitions.mli
index 5814a70c952..cd93d34343d 100644
--- a/src/plugins/wp/Definitions.mli
+++ b/src/plugins/wp/Definitions.mli
@@ -28,6 +28,7 @@ open Lang.F
type cluster
+val dummy : unit -> cluster
val cluster : id:string -> ?title:string -> ?position:Filepath.position -> unit -> cluster
val axiomatic : axiomatic -> cluster
val section : logic_section -> cluster
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 7fdb796cf1c..f088afb4eb9 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -540,8 +540,6 @@ let cluster_globals () =
let cluster_memory () =
Definitions.cluster ~id:"Compound" ~title:"Memory Compound Updates" ()
-let cluster_dummy () = Definitions.cluster ~id:"dummy" ()
-
module ShiftFieldDef = WpContext.StaticGenerator(Cil_datatype.Fieldinfo)
(struct
let name = "MemTyped.ShiftFieldDef"
@@ -563,7 +561,7 @@ module ShiftFieldDef = WpContext.StaticGenerator(Cil_datatype.Fieldinfo)
d_lfun = lfun ; d_types = 0 ;
d_params = [xloc] ;
d_definition = dfun ;
- d_cluster = cluster_dummy () ;
+ d_cluster = Definitions.dummy () ;
}
let compile = Lang.local generate
@@ -627,7 +625,7 @@ module ShiftGen = WpContext.StaticGenerator(Cobj)
d_lfun = shift ; d_types = 0 ;
d_params = [xloc;xk] ;
d_definition = dfun ;
- d_cluster = cluster_dummy () ;
+ d_cluster = Definitions.dummy () ;
}
let compile = Lang.local generate
--
GitLab