Update dependency: deps/k_release (#3636)

runtimeverification · Sep 8, 2023 · 4f219fd · 4f219fd
1 parent 0d98bc9
commit 4f219fd
Show file tree

Hide file tree

Showing 5 changed files with 17 additions and 17 deletions.
diff --git a/deps/k_release b/deps/k_release
@@ -1 +1 @@
-6.0.36
+6.0.87
diff --git a/test/imp/imp.k b/test/imp/imp.k
@@ -151,8 +151,8 @@ considering their erasure as computational steps in the resulting transition
 systems.  You can make these rules computational (dropping the attribute
 \texttt{structural}) if you do want these to count as computational steps. */
 
-  rule {} => .   [structural]
-  rule {S} => S  [structural]
+  rule {} => .
+  rule {S} => S
 
 /*@ \subsubsection{Assignment}
 The assigned variable is updated in the state.  The variable is expected
@@ -172,7 +172,7 @@ and counting only the steps corresponding to computational rules as
 transitions (i.e., hiding the structural rules as unobservable, or
 internal steps). */
 
-  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+  rule S1:Stmt S2:Stmt => S1 ~> S2
 
 /*@ \subsubsection{Conditional}
 The conditional statement has two semantic cases, corresponding to
@@ -188,7 +188,7 @@ argument is allowed to be evaluated. */
 We give the semantics of the \texttt{while} loop by unrolling.
 Note that we preferred to make the rule below structural. */
 
-  rule while (B) S => if (B) {S while (B) S} else {}  [structural]
+  rule while (B) S => if (B) {S while (B) S} else {}
 
 /*@ \subsection{Programs}
 The semantics of an IMP program is that its body statement is executed
@@ -205,7 +205,7 @@ a computational step. */
 
   rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->0) </state>
     requires notBool (X in keys(Rho))
-  rule int .Ids; S => S  [structural]
+  rule int .Ids; S => S
 
   // for add-spec, double-sum-spec, run-stepf-repl-scrip-spec, sum-div-spec
   // , sum-save-proofs-spec

diff --git a/test/kprove/imp.k b/test/kprove/imp.k
@@ -151,8 +151,8 @@ considering their erasure as computational steps in the resulting transition
 systems.  You can make these rules computational (dropping the attribute
 \texttt{structural}) if you do want these to count as computational steps. */
 
-  rule {} => .   [structural]
-  rule {S} => S  [structural]
+  rule {} => .
+  rule {S} => S
 
 /*@ \subsubsection{Assignment}
 The assigned variable is updated in the state.  The variable is expected
@@ -172,7 +172,7 @@ and counting only the steps corresponding to computational rules as
 transitions (i.e., hiding the structural rules as unobservable, or
 internal steps). */
 
-  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+  rule S1:Stmt S2:Stmt => S1 ~> S2
 
 /*@ \subsubsection{Conditional}
 The conditional statement has two semantic cases, corresponding to
@@ -188,7 +188,7 @@ argument is allowed to be evaluated. */
 We give the semantics of the \texttt{while} loop by unrolling.
 Note that we preferred to make the rule below structural. */
 
-  rule while (B) S => if (B) {S while (B) S} else {}  [structural]
+  rule while (B) S => if (B) {S while (B) S} else {}
 
 /*@ \subsection{Programs}
 The semantics of an IMP program is that its body statement is executed
@@ -205,7 +205,7 @@ a computational step. */
 
   rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->0) </state>
     requires notBool (X in keys(Rho))
-  rule int .Ids; S => S  [structural]
+  rule int .Ids; S => S
 
 //
 // verification ids

diff --git a/test/map-symbolic/assignment-11-spec.k.out.golden b/test/map-symbolic/assignment-11-spec.k.out.golden
@@ -12,8 +12,8 @@
 #And
   <k>
     assignmentResult ( ( MAP
-    X:MyId |-> 1
-    Y:MyId |-> 2 ) [ Z:MyId <- 3 ] ) ~> .
+    X:MyId |-> 1 ) [ Z:MyId <- 3 ]
+    Y:MyId |-> 2 ) ~> .
   </k>
 #And
   {

diff --git a/test/smc/smc.k b/test/smc/smc.k
@@ -81,15 +81,15 @@ module SMC
   rule <k> && E => E ...</k>
        <stack> true : S:ValStack => S </stack>
 
-  rule {} => .   [structural]
-  rule {S} => S  [structural]
+  rule {} => .
+  rule {S} => S
 
   rule X:Id = E:AExp ; => E ~> X =
   rule <k> X = => . ...</k>
        <mem>... X |-> (_ => I) ...</mem>
        <stack> I:Int : S:ValStack => S </stack>
 
-  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+  rule S1:Stmt S2:Stmt => S1 ~> S2
 
   rule if (B:BExp) S1:Block else S2:Block  => B ~> choice(S1,S2)
   rule <k> choice(Bl,_) => Bl ...</k> <stack> true : S:ValStack => S </stack>
@@ -99,7 +99,7 @@ module SMC
 
   rule <k> int (X,Xs => Xs);_ </k> <mem> Rho:Map (.Map => X|->0) </mem>
     requires notBool (X in keys(Rho))
-  rule int .Ids; S => S  [structural]
+  rule int .Ids; S => S
 
   // for add-spec, add-stack-spec, double-sum-spec, double-sum-stack-spec,
   // sum-spec, sum-stack-spec