Skip to content

Commit 10cd735

Browse files
ana-pantilieana-pantilie
authored
Add map-symbolic tests from frontend (#2466)
1 parent 4fb7d68 commit 10cd735

File tree

190 files changed

+3107
-25
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

190 files changed

+3107
-25
lines changed

‎test/sidecondition/Makefile renamed to ‎test/map-symbolic/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
1-
DEF := map-tests
1+
DEF = map-tests
22
include $(CURDIR)/../include.mk

‎test/map-symbolic/assignment

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
claim <k> assignment ( .Map [ x <- 3 ] ) => . </k>
2+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k>
3+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X
4+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Y in_keys(MAP)
5+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool notBool Y in_keys(MAP)
6+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y ==K X
7+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y ==K X andBool Z in_keys(MAP)
8+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y ==K X andBool notBool Z in_keys(MAP)
9+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z =/=K X
10+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z =/=K Y
11+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z =/=K Y andBool notBool Y in_keys(MAP) andBool Z in_keys(MAP)
12+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z ==K Y andBool Z =/=K X
13+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z =/=K Y andBool Z ==K X
14+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z =/=K Y andBool Z =/=K X
15+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z =/=K Y andBool Z =/=K X andBool Y in_keys(MAP) andBool Z in_keys(MAP)
16+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z =/=K Y andBool Z =/=K X andBool notBool Y in_keys(MAP) andBool notBool Z in_keys(MAP)
17+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y ==K X andBool Z ==K Y andBool Z ==K X
18+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y ==K X andBool Z ==K Y andBool Z ==K X andBool X in_keys(MAP)
19+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y ==K X andBool Z ==K Y andBool Z ==K X andBool notBool X in_keys(MAP)
20+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y ==K X andBool Z =/=K Y andBool Z =/=K X
21+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Z ==K X
22+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Z =/=K X
23+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Z ==K Y
24+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Z =/=K Y
25+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Z =/=K Y andBool Z =/=K X
26+
claim <k> assignment ( (X:MyId |-> 3 1 |-> 4) [ 0 <- 5 ] ) => . </k> requires X =/=K 1
27+
claim <k> assignment ( (X:MyId |-> 4) [ X <- 3 ] ) => . </k>
28+
claim <k> assignment ( (X:MyId |-> 3 y |-> 4) [ x <- 5 ] ) => . </k> requires X =/=K y
29+
claim <k> assignment ( ( X:MyId |-> BAL_TO:Int Y:MyId |-> BAL_FROM:Int MAP:Map ) [ Y <- BAL_FROM -Int 30 ] ) => . </k> requires X =/=K Y
30+
claim <k> assignment ( ( foo ( X:MyId ) |-> BAL_TO:Int foo ( Y:MyId ) |-> BAL_FROM:Int MAP:Map ) [ foo ( Y ) <- BAL_FROM -Int 30 ] ) => . </k> requires X =/=K Y
31+
claim <k> assignment ( ( foo ( X:MyId ) |-> BAL_TO:Int foo ( Y:MyId ) |-> BAL_FROM:Int MAP:Map ) [ foo ( Y ) <- BAL_FROM -Int 30 ] ) => . </k> requires foo ( X ) =/=K foo ( Y )

‎test/map-symbolic/assignment-1-spec.k

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// Copyright (c) 2019 K Team. All Rights Reserved.
2+
// generated by gen-tests.sh
3+
4+
requires "map-tests.k"
5+
6+
module VERIFICATION
7+
imports MAP-TESTS
8+
endmodule
9+
10+
module ASSIGNMENT-1-SPEC
11+
imports VERIFICATION
12+
13+
claim <k> assignment ( .Map [ x <- 3 ] ) => . </k>
14+
15+
endmodule

‎test/map-symbolic/assignment-1-spec.k.out.golden

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
<k>
2+
assignmentResult ( x |-> 3 ) ~> .
3+
</k>

‎test/map-symbolic/assignment-10-spec.k

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// Copyright (c) 2019 K Team. All Rights Reserved.
2+
// generated by gen-tests.sh
3+
4+
requires "map-tests.k"
5+
6+
module VERIFICATION
7+
imports MAP-TESTS
8+
endmodule
9+
10+
module ASSIGNMENT-10-SPEC
11+
imports VERIFICATION
12+
13+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z =/=K Y
14+
15+
endmodule

‎test/map-symbolic/assignment-10-spec.k.out.golden

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
#Not ( {
2+
X
3+
#Equals
4+
Y
5+
} )
6+
#And
7+
#Not ( {
8+
Y
9+
#Equals
10+
Z
11+
} )
12+
#And
13+
<k>
14+
assignmentResult ( ( MAP [ Y:MyId <- 2 ]
15+
X:MyId |-> 1 ) [ Z:MyId <- 3 ] ) ~> .
16+
</k>
17+
#And
18+
{
19+
false
20+
#Equals
21+
X:MyId in_keys ( MAP )
22+
}

‎test/map-symbolic/assignment-11-spec.k

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// Copyright (c) 2019 K Team. All Rights Reserved.
2+
// generated by gen-tests.sh
3+
4+
requires "map-tests.k"
5+
6+
module VERIFICATION
7+
imports MAP-TESTS
8+
endmodule
9+
10+
module ASSIGNMENT-11-SPEC
11+
imports VERIFICATION
12+
13+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z =/=K Y andBool notBool Y in_keys(MAP) andBool Z in_keys(MAP)
14+
15+
endmodule

‎test/map-symbolic/assignment-11-spec.k.out.golden

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
#Not ( {
2+
X
3+
#Equals
4+
Y
5+
} )
6+
#And
7+
#Not ( {
8+
Y
9+
#Equals
10+
Z
11+
} )
12+
#And
13+
<k>
14+
assignmentResult ( ( MAP
15+
X:MyId |-> 1
16+
Y:MyId |-> 2 ) [ Z:MyId <- 3 ] ) ~> .
17+
</k>
18+
#And
19+
{
20+
false
21+
#Equals
22+
X:MyId in_keys ( MAP )
23+
}
24+
#And
25+
{
26+
false
27+
#Equals
28+
Y:MyId in_keys ( MAP )
29+
}
30+
#And
31+
{
32+
true
33+
#Equals
34+
Z:MyId in_keys ( MAP )
35+
}

‎test/map-symbolic/assignment-12-spec.k

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// Copyright (c) 2019 K Team. All Rights Reserved.
2+
// generated by gen-tests.sh
3+
4+
requires "map-tests.k"
5+
6+
module VERIFICATION
7+
imports MAP-TESTS
8+
endmodule
9+
10+
module ASSIGNMENT-12-SPEC
11+
imports VERIFICATION
12+
13+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z ==K Y andBool Z =/=K X
14+
15+
endmodule

‎test/map-symbolic/assignment-12-spec.k.out.golden

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#Not ( {
2+
X
3+
#Equals
4+
Z
5+
} )
6+
#And
7+
<k>
8+
assignmentResult ( MAP [ Z:MyId <- 3 ]
9+
X:MyId |-> 1 ) ~> .
10+
</k>
11+
#And
12+
{
13+
false
14+
#Equals
15+
X:MyId in_keys ( MAP )
16+
}

‎test/map-symbolic/assignment-13-spec.k

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// Copyright (c) 2019 K Team. All Rights Reserved.
2+
// generated by gen-tests.sh
3+
4+
requires "map-tests.k"
5+
6+
module VERIFICATION
7+
imports MAP-TESTS
8+
endmodule
9+
10+
module ASSIGNMENT-13-SPEC
11+
imports VERIFICATION
12+
13+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z =/=K Y andBool Z ==K X
14+
15+
endmodule

‎test/map-symbolic/assignment-13-spec.k.out.golden

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#Not ( {
2+
Y
3+
#Equals
4+
Z
5+
} )
6+
#And
7+
<k>
8+
assignmentResult ( MAP [ Y:MyId <- 2 ]
9+
Z:MyId |-> 3 ) ~> .
10+
</k>
11+
#And
12+
{
13+
false
14+
#Equals
15+
Z:MyId in_keys ( MAP )
16+
}

‎test/map-symbolic/assignment-14-spec.k

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// Copyright (c) 2019 K Team. All Rights Reserved.
2+
// generated by gen-tests.sh
3+
4+
requires "map-tests.k"
5+
6+
module VERIFICATION
7+
imports MAP-TESTS
8+
endmodule
9+
10+
module ASSIGNMENT-14-SPEC
11+
imports VERIFICATION
12+
13+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z =/=K Y andBool Z =/=K X
14+
15+
endmodule

‎test/map-symbolic/assignment-14-spec.k.out.golden

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
#Not ( {
2+
X
3+
#Equals
4+
Y
5+
} )
6+
#And
7+
#Not ( {
8+
X
9+
#Equals
10+
Z
11+
} )
12+
#And
13+
#Not ( {
14+
Y
15+
#Equals
16+
Z
17+
} )
18+
#And
19+
<k>
20+
assignmentResult ( MAP [ Y:MyId <- 2 ] [ Z:MyId <- 3 ]
21+
X:MyId |-> 1 ) ~> .
22+
</k>
23+
#And
24+
{
25+
false
26+
#Equals
27+
X:MyId in_keys ( MAP )
28+
}

‎test/map-symbolic/assignment-15-spec.k

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// Copyright (c) 2019 K Team. All Rights Reserved.
2+
// generated by gen-tests.sh
3+
4+
requires "map-tests.k"
5+
6+
module VERIFICATION
7+
imports MAP-TESTS
8+
endmodule
9+
10+
module ASSIGNMENT-15-SPEC
11+
imports VERIFICATION
12+
13+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z =/=K Y andBool Z =/=K X andBool Y in_keys(MAP) andBool Z in_keys(MAP)
14+
15+
endmodule

‎test/map-symbolic/assignment-15-spec.k.out.golden

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
#Not ( {
2+
X
3+
#Equals
4+
Y
5+
} )
6+
#And
7+
#Not ( {
8+
X
9+
#Equals
10+
Z
11+
} )
12+
#And
13+
#Not ( {
14+
Y
15+
#Equals
16+
Z
17+
} )
18+
#And
19+
<k>
20+
assignmentResult ( MAP [ Y:MyId <- 2 ] [ Z:MyId <- 3 ]
21+
X:MyId |-> 1 ) ~> .
22+
</k>
23+
#And
24+
{
25+
false
26+
#Equals
27+
X:MyId in_keys ( MAP )
28+
}
29+
#And
30+
{
31+
true
32+
#Equals
33+
Y:MyId in_keys ( MAP )
34+
}
35+
#And
36+
{
37+
true
38+
#Equals
39+
Z:MyId in_keys ( MAP )
40+
}

‎test/map-symbolic/assignment-16-spec.k

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// Copyright (c) 2019 K Team. All Rights Reserved.
2+
// generated by gen-tests.sh
3+
4+
requires "map-tests.k"
5+
6+
module VERIFICATION
7+
imports MAP-TESTS
8+
endmodule
9+
10+
module ASSIGNMENT-16-SPEC
11+
imports VERIFICATION
12+
13+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y =/=K X andBool Z =/=K Y andBool Z =/=K X andBool notBool Y in_keys(MAP) andBool notBool Z in_keys(MAP)
14+
15+
endmodule

‎test/map-symbolic/assignment-16-spec.k.out.golden

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
#Not ( {
2+
X
3+
#Equals
4+
Y
5+
} )
6+
#And
7+
#Not ( {
8+
X
9+
#Equals
10+
Z
11+
} )
12+
#And
13+
#Not ( {
14+
Y
15+
#Equals
16+
Z
17+
} )
18+
#And
19+
<k>
20+
assignmentResult ( MAP
21+
X:MyId |-> 1
22+
Y:MyId |-> 2
23+
Z:MyId |-> 3 ) ~> .
24+
</k>
25+
#And
26+
{
27+
false
28+
#Equals
29+
X:MyId in_keys ( MAP )
30+
}
31+
#And
32+
{
33+
false
34+
#Equals
35+
Y:MyId in_keys ( MAP )
36+
}
37+
#And
38+
{
39+
false
40+
#Equals
41+
Z:MyId in_keys ( MAP )
42+
}

‎test/map-symbolic/assignment-17-spec.k

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// Copyright (c) 2019 K Team. All Rights Reserved.
2+
// generated by gen-tests.sh
3+
4+
requires "map-tests.k"
5+
6+
module VERIFICATION
7+
imports MAP-TESTS
8+
endmodule
9+
10+
module ASSIGNMENT-17-SPEC
11+
imports VERIFICATION
12+
13+
claim <k> assignment ( (MAP:Map X:MyId |-> 1) [ Y:MyId <- 2 ] [ Z:MyId <- 3 ] ) => . </k> requires Y ==K X andBool Z ==K Y andBool Z ==K X
14+
15+
endmodule

0 commit comments

Comments
 (0)