Skip to content

Commit 2891334

Browse files
rv-jenkinsttuegel
rv-jenkins
and
ttuegel
authored
Update dependency: deps/k_release
* deps/k_release: v5.0.0-3948c10 * test/smc: Fix bracket priority issue * test/smc: Fix warnings * deps/k_release: v5.0.0-d85b66d * deps/k_release: v5.0.0-aa04b03 * test/imp-map-unify: Fix bracket priority issue * test/imp-map-unify: Fix warnings * test/imp: Fix bracket priority issue * test/imp: Fix warnings * test/imp-map-strict: Fix bracket priority issue * test/imp-map-strict: Fix warnings * test/imp-concrete-heat-cool: Fix bracket issues * test/imp-concrete-heat-cool: Fix warnings * test/imp-monosorted: Fix bracket priority issues * test/imp-monosorted: Fix warnings * test/ord: Fix warnings * test/imp-map: Fix bracket priority issue * test/imp-map: Fix warnings * test/imp-concrete-state: Fix bracket priority issue * test/imp-concrete-state: Fix warnings * test/imp-map-unify-strict: Fix bracket priority issue * test/imp-map-unify-strict: Fix warnings Co-authored-by: Thomas Tuegel <[email protected]> Co-authored-by: Thomas Tuegel <[email protected]>
1 parent 3243d1e commit 2891334

File tree

20 files changed

+78
-72
lines changed

20 files changed

+78
-72
lines changed

‎deps/k_release

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
v5.0.0-863727b
1+
v5.0.0-aa04b03

‎test/imp-concrete-heat-cool/imp.k

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,13 @@ module IMP-SYNTAX
55
syntax AExp ::= Int | Id
66
| "-" Int
77
| AExp "/" AExp [left/*, strict*/]
8-
> AExp "+" AExp [left/*, strict*/]
98
| "(" AExp ")" [bracket]
9+
> AExp "+" AExp [left/*, strict*/]
1010
syntax BExp ::= Bool
1111
| AExp "<=" AExp [/*seqstrict,*/ latex({#1}\leq{#2})]
1212
| "!" BExp /*[strict]*/
13-
> BExp "&&" BExp [left/*, strict(1)*/]
1413
| "(" BExp ")" [bracket]
14+
> BExp "&&" BExp [left/*, strict(1)*/]
1515
syntax Block ::= "{" "}"
1616
| "{" Stmt "}"
1717
syntax Stmt ::= Block
@@ -79,7 +79,7 @@ module SYMBOLIC-INT
7979
imports IMP-SYNTAX
8080
imports INT
8181
syntax AExp ::= "symInt"
82-
rule symInt => ?I:Int
82+
rule symInt => ?_I:Int
8383
endmodule
8484

8585
module IMP

‎test/imp-concrete-state/imp.k

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,13 @@ module IMP-SYNTAX
55
syntax AExp ::= Int | Id
66
| "-" Int
77
| AExp "/" AExp [left, seqstrict]
8-
> AExp "+" AExp [left, seqstrict]
98
| "(" AExp ")" [bracket]
9+
> AExp "+" AExp [left, seqstrict]
1010
syntax BExp ::= Bool
1111
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
1212
| "!" BExp [strict]
13-
> BExp "&&" BExp [left, strict(1)]
1413
| "(" BExp ")" [bracket]
14+
> BExp "&&" BExp [left, strict(1)]
1515
syntax Block ::= "{" "}"
1616
| "{" Stmt "}"
1717
syntax Stmt ::= Block
@@ -38,7 +38,7 @@ module SYMBOLIC-INT
3838
imports IMP-SYNTAX
3939
imports INT
4040
syntax AExp ::= "symInt"
41-
rule symInt => ?I:Int
41+
rule symInt => ?_I:Int
4242
endmodule
4343

4444
module IMP

‎test/imp-map-strict/imp.k

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,13 @@ module IMP-SYNTAX
66
syntax AExp ::= Int | Id
77
| "-" Int
88
| AExp "/" AExp [left, seqstrict]
9-
> AExp "+" AExp [left, seqstrict]
109
| "(" AExp ")" [bracket]
10+
> AExp "+" AExp [left, seqstrict]
1111
syntax BExp ::= Bool
1212
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
1313
| "!" BExp [strict]
14-
> BExp "&&" BExp [left, strict(1)]
1514
| "(" BExp ")" [bracket]
15+
> BExp "&&" BExp [left, strict(1)]
1616
syntax Block ::= "{" "}"
1717
| "{" Stmt "}"
1818
syntax Stmt ::= Block
@@ -29,7 +29,7 @@ module SYMBOLIC-INT
2929
imports IMP-SYNTAX
3030
imports INT
3131
syntax AExp ::= "symInt"
32-
rule symInt => ?I:Int
32+
rule symInt => ?_I:Int
3333
endmodule
3434

3535
module IMP

‎test/imp-map-unify-strict/imp.k

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,13 @@ module IMP-SYNTAX
66
syntax AExp ::= Int | Id
77
| "-" Int
88
| AExp "/" AExp [left, seqstrict]
9-
> AExp "+" AExp [left, seqstrict]
109
| "(" AExp ")" [bracket]
10+
> AExp "+" AExp [left, seqstrict]
1111
syntax BExp ::= Bool
1212
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
1313
| "!" BExp [strict]
14-
> BExp "&&" BExp [left, strict(1)]
1514
| "(" BExp ")" [bracket]
15+
> BExp "&&" BExp [left, strict(1)]
1616
syntax Block ::= "{" "}"
1717
| "{" Stmt "}"
1818
syntax Stmt ::= Block
@@ -29,7 +29,7 @@ module SYMBOLIC-INT
2929
imports IMP-SYNTAX
3030
imports INT
3131
syntax AExp ::= "symInt"
32-
rule symInt => ?I:Int
32+
rule symInt => ?_I:Int
3333
endmodule
3434

3535
module IMP

‎test/imp-map-unify/imp.k

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,13 @@ module IMP-SYNTAX
66
syntax AExp ::= Int | Id
77
| "-" Int
88
| AExp "/" AExp [left/*, strict*/]
9-
> AExp "+" AExp [left/*, strict*/]
109
| "(" AExp ")" [bracket]
10+
> AExp "+" AExp [left/*, strict*/]
1111
syntax BExp ::= Bool
1212
| AExp "<=" AExp [/*seqstrict,*/ latex({#1}\leq{#2})]
1313
| "!" BExp /*[strict]*/
14-
> BExp "&&" BExp [left/*, strict(1)*/]
1514
| "(" BExp ")" [bracket]
15+
> BExp "&&" BExp [left/*, strict(1)*/]
1616
syntax Block ::= "{" "}"
1717
| "{" Stmt "}"
1818
syntax Stmt ::= Block
@@ -71,7 +71,7 @@ module SYMBOLIC-INT
7171
imports IMP-SYNTAX
7272
imports INT
7373
syntax AExp ::= "symInt"
74-
rule symInt => ?I:Int
74+
rule symInt => ?_I:Int
7575
endmodule
7676

7777
module IMP

‎test/imp-map/imp.k

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,13 @@ module IMP-SYNTAX
66
syntax AExp ::= Int | Id
77
| "-" Int
88
| AExp "/" AExp [left/*, strict*/]
9-
> AExp "+" AExp [left/*, strict*/]
109
| "(" AExp ")" [bracket]
10+
> AExp "+" AExp [left/*, strict*/]
1111
syntax BExp ::= Bool
1212
| AExp "<=" AExp [/*seqstrict,*/ latex({#1}\leq{#2})]
1313
| "!" BExp /*[strict]*/
14-
> BExp "&&" BExp [left/*, strict(1)*/]
1514
| "(" BExp ")" [bracket]
15+
> BExp "&&" BExp [left/*, strict(1)*/]
1616
syntax Block ::= "{" "}"
1717
| "{" Stmt "}"
1818
syntax Stmt ::= Block
@@ -71,7 +71,7 @@ module SYMBOLIC-INT
7171
imports IMP-SYNTAX
7272
imports INT
7373
syntax AExp ::= "symInt"
74-
rule symInt => ?I:Int
74+
rule symInt => ?_I:Int
7575
endmodule
7676

7777
module IMP

‎test/imp-monosorted/imp.k

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,13 @@ module IMP-SYNTAX
33
syntax AExp ::= "AInt" Int | "AId" Id
44
| "-" Int
55
| AExp "/" AExp [left/*, strict*/]
6-
> AExp "+" AExp [left/*, strict*/]
76
| "(" AExp ")" [bracket]
7+
> AExp "+" AExp [left/*, strict*/]
88
syntax BExp ::= "ABool" Bool
99
| AExp "<=" AExp [/*seqstrict,*/ latex({#1}\leq{#2})]
1010
| "!" BExp /*[strict]*/
11-
> BExp "&&" BExp [left/*, strict(1)*/]
1211
| "(" BExp ")" [bracket]
12+
> BExp "&&" BExp [left/*, strict(1)*/]
1313
syntax Block ::= "{" "}"
1414
| "{" Stmt "}"
1515
syntax Stmt ::= "ABlock" Block
@@ -84,13 +84,13 @@ module IMP-STATE
8484
syntax Bool ::= inState(State, Id) [function]
8585

8686
rule inState(.State, _) => false
87-
rule inState((K:Id |-> _:Int) S:State, K:Id) => true
87+
rule inState((K:Id |-> _:Int) _:State, K:Id) => true
8888
rule inState((K:Id |-> _:Int) S:State, K':Id) => inState(S, K')
8989
requires K =/=K K'
9090

9191
syntax Int ::= get(State, Id) [function, partial]
9292

93-
rule get((K:Id |-> V:Int) S:State, K:Id) => V
93+
rule get((K:Id |-> V:Int) _:State, K:Id) => V
9494
rule get((X:Id |-> _:Int) S:State, Y:Id) => get(S, Y)
9595
requires X =/=K Y
9696

@@ -100,7 +100,7 @@ module SYMBOLIC-INT
100100
imports IMP-SYNTAX
101101
imports INT
102102
syntax AExp ::= "symInt"
103-
rule symInt => AInt ?I:Int
103+
rule symInt => AInt ?_I:Int
104104
endmodule
105105

106106
module IMP

‎test/imp/imp.k

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -28,13 +28,13 @@ argument, because we want to give it a short-circuit semantics. */
2828
syntax AExp ::= Int | Id | "?Int"
2929
| "-" Int [format(%1%2)]
3030
| AExp "/" AExp [left, seqstrict, color(pink)]
31-
> AExp "+" AExp [left, seqstrict, color(pink)]
3231
| "(" AExp ")" [bracket]
32+
> AExp "+" AExp [left, seqstrict, color(pink)]
3333
syntax BExp ::= Bool
3434
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2}), color(pink)]
3535
| "!" BExp [strict, color(pink)]
36-
> BExp "&&" BExp [left, strict(1), color(pink)]
3736
| "(" BExp ")" [bracket]
37+
> BExp "&&" BExp [left, strict(1), color(pink)]
3838
syntax Block ::= "{" "}"
3939
| "{" Stmt "}" [format(%1%i%n%2%d%n%3)]
4040
syntax Stmt ::= Block
@@ -117,7 +117,7 @@ abstraction mechanism is at work here! That means that the rewrites in the
117117
rules below all happen at the beginning of the \textsf{k} cell. */
118118

119119
// Introduce symbolic variables
120-
rule ?Int => ?I:Int
120+
rule ?Int => ?_I:Int
121121

122122
rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0
123123
rule I1 + I2 => I1 +Int I2

‎test/imp/impossible-branch.imp.out.golden

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4,15 +4,15 @@
44
</k>
55
<state>
66
r |-> 0
7-
x |-> ?I:Int
8-
y |-> ?I0:Int
7+
x |-> ?_I:Int
8+
y |-> ?_I0:Int
99
</state>
1010
</T>
1111
#And
1212
{
1313
false
1414
#Equals
15-
?I:Int <=Int ?I0:Int
15+
?_I:Int <=Int ?_I0:Int
1616
}
1717
#Or
1818
<T>
@@ -21,13 +21,13 @@
2121
</k>
2222
<state>
2323
r |-> 0
24-
x |-> ?I:Int
25-
y |-> ?I0:Int
24+
x |-> ?_I:Int
25+
y |-> ?_I0:Int
2626
</state>
2727
</T>
2828
#And
2929
{
3030
true
3131
#Equals
32-
?I:Int <=Int ?I0:Int
32+
?_I:Int <=Int ?_I0:Int
3333
}

‎test/imp/max-inconsistent-prelude-spec.k.out.golden

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
kore-exec: [233424] Error (ErrorException):
2+
The definitions sent to the solver are inconsistent.
3+
CallStack (from HasCallStack):
4+
error, called at src/Kore/Step/SMT/Lemma.hs:104:9 in kore-0.40.0.0-CzNxqIvwhPqHJvDm7pwDgz:Kore.Step.SMT.Lemma
5+
[Error] Critical: Haskell Backend execution failed with code 1 and produced no
6+
output.

‎test/imp/max-symbolic.imp.out.golden

Lines changed: 24 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -3,93 +3,93 @@
33
.
44
</k>
55
<state>
6-
max |-> ?I:Int
7-
x |-> ?I:Int
8-
y |-> ?I0:Int
9-
z |-> ?I1:Int
6+
max |-> ?_I:Int
7+
x |-> ?_I:Int
8+
y |-> ?_I0:Int
9+
z |-> ?_I1:Int
1010
</state>
1111
</T>
1212
#And
1313
{
1414
false
1515
#Equals
16-
?I:Int <=Int ?I0:Int
16+
?_I:Int <=Int ?_I0:Int
1717
}
1818
#And
1919
{
2020
false
2121
#Equals
22-
?I:Int <=Int ?I1:Int
22+
?_I:Int <=Int ?_I1:Int
2323
}
2424
#Or
2525
<T>
2626
<k>
2727
.
2828
</k>
2929
<state>
30-
max |-> ?I0:Int
31-
x |-> ?I:Int
32-
y |-> ?I0:Int
33-
z |-> ?I1:Int
30+
max |-> ?_I0:Int
31+
x |-> ?_I:Int
32+
y |-> ?_I0:Int
33+
z |-> ?_I1:Int
3434
</state>
3535
</T>
3636
#And
3737
{
3838
false
3939
#Equals
40-
?I0:Int <=Int ?I1:Int
40+
?_I0:Int <=Int ?_I1:Int
4141
}
4242
#And
4343
{
4444
true
4545
#Equals
46-
?I:Int <=Int ?I0:Int
46+
?_I:Int <=Int ?_I0:Int
4747
}
4848
#Or
4949
<T>
5050
<k>
5151
.
5252
</k>
5353
<state>
54-
max |-> ?I1:Int
55-
x |-> ?I:Int
56-
y |-> ?I0:Int
57-
z |-> ?I1:Int
54+
max |-> ?_I1:Int
55+
x |-> ?_I:Int
56+
y |-> ?_I0:Int
57+
z |-> ?_I1:Int
5858
</state>
5959
</T>
6060
#And
6161
{
6262
false
6363
#Equals
64-
?I:Int <=Int ?I0:Int
64+
?_I:Int <=Int ?_I0:Int
6565
}
6666
#And
6767
{
6868
true
6969
#Equals
70-
?I:Int <=Int ?I1:Int
70+
?_I:Int <=Int ?_I1:Int
7171
}
7272
#Or
7373
<T>
7474
<k>
7575
.
7676
</k>
7777
<state>
78-
max |-> ?I1:Int
79-
x |-> ?I:Int
80-
y |-> ?I0:Int
81-
z |-> ?I1:Int
78+
max |-> ?_I1:Int
79+
x |-> ?_I:Int
80+
y |-> ?_I0:Int
81+
z |-> ?_I1:Int
8282
</state>
8383
</T>
8484
#And
8585
{
8686
true
8787
#Equals
88-
?I:Int <=Int ?I0:Int
88+
?_I:Int <=Int ?_I0:Int
8989
}
9090
#And
9191
{
9292
true
9393
#Equals
94-
?I0:Int <=Int ?I1:Int
94+
?_I0:Int <=Int ?_I1:Int
9595
}

‎test/imp/unreachable-spec.k

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,8 @@ module UNREACHABLE-SPEC
2525
=> .K
2626
</k>
2727
<state>
28-
a |-> A:Int
29-
b |-> B:Int
30-
r |-> R:Int
28+
a |-> _:Int
29+
b |-> _:Int
30+
r |-> _:Int
3131
</state>
3232
endmodule

0 commit comments

Comments
 (0)