[wp] fix equality clusters

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)
 
 (* -------------------------------------------------------------------------- *)

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 ->

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

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