Update dependency: deps/k_release (#1995)

* deps/k_release: v5.0.0-e698f30 * deps/k_release: v5.0.0-cecacf8 * deps/k_release: v5.0.0-d10c70c * deps/k_release: v5.0.0-bbc70cb * test: make golden Co-authored-by: Thomas Tuegel <[email protected]>
runtimeverification · Jul 24, 2020 · 7c68064 · 7c68064
1 parent 9e9085c
commit 7c68064
Show file tree

Hide file tree

Showing 10 changed files with 41 additions and 35 deletions.
diff --git a/deps/k_release b/deps/k_release
@@ -1 +1 @@
-v5.0.0-e160771
+v5.0.0-bbc70cb
diff --git a/test/imp/1.merge.out.golden b/test/imp/1.merge.out.golden
@@ -15,7 +15,7 @@
                         /* Inj: */ inj{SortId{}, SortKItem{}}(
                             /* Fl Fn D Sfa */ VarX:SortId{}
                         ),
-                        /* Fl Fn D Sfa */ VarDotVar2:SortK{}
+                        /* Fl Fn D Sfa */ Var'Unds'DotVar2:SortK{}
                     )
                 ),
                 /* Fn Sfc */
@@ -31,11 +31,11 @@
                             /* Fl Fn D Sfa */ VarI:SortKItem{}
                         ),
                         /* opaque child: */ /* Fl Fn D Sfa */
-                        VarDotVar3:SortMap{}
+                        Var'Unds'DotVar3:SortMap{}
                     )
                 )
             ),
-            /* Fl Fn D Sfa */ VarDotVar0:SortGeneratedCounterCell{}
+            /* Fl Fn D Sfa */ Var'Unds'DotVar0:SortGeneratedCounterCell{}
         )
     ),
     /* Fn Spc */
@@ -47,7 +47,7 @@
                 /* Fl Fn D Spa */
                 kseq{}(
                     /* Fl Fn D Sfa */ VarI:SortKItem{},
-                    /* Fl Fn D Sfa */ VarDotVar2:SortK{}
+                    /* Fl Fn D Sfa */ Var'Unds'DotVar2:SortK{}
                 )
             ),
             /* Fn Sfc */
@@ -62,10 +62,11 @@
                         ),
                         /* Fl Fn D Sfa */ VarI:SortKItem{}
                     ),
-                    /* opaque child: */ /* Fl Fn D Sfa */ VarDotVar3:SortMap{}
+                    /* opaque child: */ /* Fl Fn D Sfa */
+                    Var'Unds'DotVar3:SortMap{}
                 )
             )
         ),
-        /* Fl Fn D Sfa */ VarDotVar0:SortGeneratedCounterCell{}
+        /* Fl Fn D Sfa */ Var'Unds'DotVar0:SortGeneratedCounterCell{}
     )
 )
diff --git a/test/imp/2.merge.out.golden b/test/imp/2.merge.out.golden
@@ -13,7 +13,7 @@
                     /* Inj: */ inj{SortId{}, SortKItem{}}(
                         /* Fl Fn D Sfa */ VarX:SortId{}
                     ),
-                    /* Fl Fn D Sfa */ VarDotVar3:SortMap{}
+                    /* Fl Fn D Sfa */ Var'Unds'DotVar3:SortMap{}
                 ),
                 /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("false")
             ),
@@ -32,7 +32,8 @@
                             /* Fl Fn D Sfa */ VarI:SortInt{}
                         )
                     ),
-                    /* opaque child: */ /* Fl Fn D Sfa */ VarDotVar3:SortMap{}
+                    /* opaque child: */ /* Fl Fn D Sfa */
+                    Var'Unds'DotVar3:SortMap{}
                 ),
                 /* Fn Sfc */
                 /* builtin: */
@@ -44,7 +45,8 @@
                         ),
                         /* Fl Fn D Sfa */ VarI0:SortKItem{}
                     ),
-                    /* opaque child: */ /* Fl Fn D Sfa */ VarDotVar6:SortMap{}
+                    /* opaque child: */ /* Fl Fn D Sfa */
+                    Var'Unds'DotVar6:SortMap{}
                 )
             )
         ),
@@ -73,7 +75,7 @@
                             /* Inj: */ inj{SortId{}, SortKItem{}}(
                                 /* Fl Fn D Sfa */ VarX0:SortId{}
                             ),
-                            /* Fl Fn D Sfa */ VarDotVar5:SortK{}
+                            /* Fl Fn D Sfa */ Var'Unds'DotVar5:SortK{}
                         )
                     )
                 ),
@@ -90,11 +92,11 @@
                             /* Fl Fn D Sfa */ Var'Unds'0:SortKItem{}
                         ),
                         /* opaque child: */ /* Fl Fn D Sfa */
-                        VarDotVar3:SortMap{}
+                        Var'Unds'DotVar3:SortMap{}
                     )
                 )
             ),
-            /* Fl Fn D Sfa */ VarDotVar4:SortGeneratedCounterCell{}
+            /* Fl Fn D Sfa */ Var'Unds'DotVar4:SortGeneratedCounterCell{}
         )
     ),
     /* Fn Spa */
@@ -106,7 +108,7 @@
                 /* Fl Fn D Spa */
                 kseq{}(
                     /* Fl Fn D Sfa */ VarI0:SortKItem{},
-                    /* Fl Fn D Sfa */ VarDotVar5:SortK{}
+                    /* Fl Fn D Sfa */ Var'Unds'DotVar5:SortK{}
                 )
             ),
             /* Fn Spa */
@@ -121,10 +123,11 @@
                         ),
                         /* Fl Fn D Sfa */ VarI0:SortKItem{}
                     ),
-                    /* opaque child: */ /* Fl Fn D Sfa */ VarDotVar6:SortMap{}
+                    /* opaque child: */ /* Fl Fn D Sfa */
+                    Var'Unds'DotVar6:SortMap{}
                 )
             )
         ),
-        /* Fl Fn D Sfa */ VarDotVar4:SortGeneratedCounterCell{}
+        /* Fl Fn D Sfa */ Var'Unds'DotVar4:SortGeneratedCounterCell{}
     )
 )
diff --git a/test/imp/sum-save-proofs-spec.k.save-proofs.kore.golden b/test/imp/sum-save-proofs-spec.k.save-proofs.kore.golden
@@ -104,7 +104,7 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d
                                     )
                                 )
                             ),
-                            /* Fl Fn D Sfa */ VarDotVar2:SortK{}
+                            /* Fl Fn D Sfa */ Var'Unds'DotVar2:SortK{}
                         )
                     ),
                     /* Fl Fn D Spa */
@@ -139,7 +139,7 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d
                 ),
                 /* Fl Fn D Spa */
                 Lbl'-LT-'generatedCounter'-GT-'{}(
-                    /* Fl Fn D Sfa */ VarDotVar3:SortInt{}
+                    /* Fl Fn D Sfa */ Var'Unds'DotVar3:SortInt{}
                 )
             )
         ),
@@ -150,7 +150,9 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d
                 /* Fn Spa */
                 Lbl'-LT-'T'-GT-'{}(
                     /* Fl Fn D Spa */
-                    Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa */ VarDotVar2:SortK{}),
+                    Lbl'-LT-'k'-GT-'{}(
+                        /* Fl Fn D Sfa */ Var'Unds'DotVar2:SortK{}
+                    ),
                     /* Fn Spa */
                     Lbl'-LT-'state'-GT-'{}(
                         /* Fn Spa */
@@ -200,7 +202,7 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d
                 ),
                 /* Fl Fn D Spa */
                 Lbl'-LT-'generatedCounter'-GT-'{}(
-                    /* Fl Fn D Sfa */ VarDotVar3:SortInt{}
+                    /* Fl Fn D Sfa */ Var'Unds'DotVar3:SortInt{}
                 )
             )
         )

diff --git a/test/overloads/simple-lists/broken-spec.k.out.golden b/test/overloads/simple-lists/broken-spec.k.out.golden
@@ -1,3 +1,3 @@
 <k>
-  i1  i2  .EmptyStmts ~> DotVar1 ~> .
+  i1  i2  .EmptyStmts ~> _DotVar1 ~> .
 </k>
diff --git a/test/priority/1.merge.out.golden b/test/priority/1.merge.out.golden
@@ -62,10 +62,10 @@
                                 /* Fl Fn D Sfa */ VarX0:SortInt{}
                             )
                         ),
-                        /* Fl Fn D Sfa */ VarDotVar3:SortK{}
+                        /* Fl Fn D Sfa */ Var'Unds'DotVar3:SortK{}
                     )
                 ),
-                /* Fl Fn D Sfa */ VarDotVar2:SortGeneratedCounterCell{}
+                /* Fl Fn D Sfa */ Var'Unds'DotVar2:SortGeneratedCounterCell{}
             )
         )
     ),
@@ -79,9 +79,9 @@
                 /* Inj: */ inj{SortS{}, SortKItem{}}(
                     /* Fl Fn D Sfa Cl */ Lbltwo'Unds'PRIORITY'Unds'S{}()
                 ),
-                /* Fl Fn D Sfa */ VarDotVar3:SortK{}
+                /* Fl Fn D Sfa */ Var'Unds'DotVar3:SortK{}
             )
         ),
-        /* Fl Fn D Sfa */ VarDotVar2:SortGeneratedCounterCell{}
+        /* Fl Fn D Sfa */ Var'Unds'DotVar2:SortGeneratedCounterCell{}
     )
 )
diff --git a/test/priority/2.merge.out.golden b/test/priority/2.merge.out.golden
@@ -65,10 +65,10 @@
                                 /* Fl Fn D Sfa */ VarX0:SortInt{}
                             )
                         ),
-                        /* Fl Fn D Sfa */ VarDotVar3:SortK{}
+                        /* Fl Fn D Sfa */ Var'Unds'DotVar3:SortK{}
                     )
                 ),
-                /* Fl Fn D Sfa */ VarDotVar2:SortGeneratedCounterCell{}
+                /* Fl Fn D Sfa */ Var'Unds'DotVar2:SortGeneratedCounterCell{}
             )
         )
     ),
@@ -82,9 +82,9 @@
                 /* Inj: */ inj{SortS{}, SortKItem{}}(
                     /* Fl Fn D Sfa Cl */ Lblone'Unds'PRIORITY'Unds'S{}()
                 ),
-                /* Fl Fn D Sfa */ VarDotVar3:SortK{}
+                /* Fl Fn D Sfa */ Var'Unds'DotVar3:SortK{}
             )
         ),
-        /* Fl Fn D Sfa */ VarDotVar2:SortGeneratedCounterCell{}
+        /* Fl Fn D Sfa */ Var'Unds'DotVar2:SortGeneratedCounterCell{}
     )
 )
diff --git a/test/remove-destination/test-1-spec.k.out.golden b/test/remove-destination/test-1-spec.k.out.golden
@@ -36,7 +36,7 @@
 #And
   <k>
     a ( K:Int |-> V:Int
-    M ) ~> DotVar1 ~> .
+    M ) ~> _DotVar1 ~> .
   </k>
 #And
   {

diff --git a/test/save-proofs/test-1-spec.k.out.golden b/test/save-proofs/test-1-spec.k.out.golden
@@ -1,3 +1,3 @@
 <k>
-  AA ( X ) ~> DotVar1 ~> .
+  AA ( X ) ~> _DotVar1 ~> .
 </k>
diff --git a/test/save-proofs/test-1-spec.k.save-proofs.kore.golden b/test/save-proofs/test-1-spec.k.save-proofs.kore.golden
@@ -17,12 +17,12 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d
                         LblBB'LParUndsRParUnds'SAVE-PROOFS'Unds'KItem'Unds'Int{}(
                             /* Fl Fn D Sfa */ VarX:SortInt{}
                         ),
-                        /* Fl Fn D Sfa */ VarDotVar1:SortK{}
+                        /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortK{}
                     )
                 ),
                 /* Fl Fn D Spa */
                 Lbl'-LT-'generatedCounter'-GT-'{}(
-                    /* Fl Fn D Sfa */ VarDotVar2:SortInt{}
+                    /* Fl Fn D Sfa */ Var'Unds'DotVar2:SortInt{}
                 )
             )
         ),
@@ -38,12 +38,12 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d
                         LblCC'LParUndsRParUnds'SAVE-PROOFS'Unds'KItem'Unds'Int{}(
                             /* Fl Fn D Sfa */ VarX:SortInt{}
                         ),
-                        /* Fl Fn D Sfa */ VarDotVar1:SortK{}
+                        /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortK{}
                     )
                 ),
                 /* Fl Fn D Spa */
                 Lbl'-LT-'generatedCounter'-GT-'{}(
-                    /* Fl Fn D Sfa */ VarDotVar2:SortInt{}
+                    /* Fl Fn D Sfa */ Var'Unds'DotVar2:SortInt{}
                 )
             )
         )
-Original file line number
+Diff line change
@@ Expand Up / @@ -36,7 +36,7 @@ @@
     #And
       <k>
         a ( K:Int |-> V:Int
-        M ) ~> DotVar1 ~> .
+        M ) ~> _DotVar1 ~> .
       </k>
     #And
       {
@@ Expand Down @@