Skip to content

Commit d1d5580

Browse files
Adding List.update unit test only for MInt{64}
1 parent 9748736 commit d1d5580

File tree

4 files changed

+2961
-0
lines changed

4 files changed

+2961
-0
lines changed
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
module LIST-UPDATE
2+
3+
imports INT
4+
imports MINT
5+
imports BOOL
6+
imports LIST
7+
imports K-EQUAL
8+
9+
syntax MInt{64}
10+
11+
syntax List ::= "listOfMInt" [macro]
12+
rule listOfMInt => ListItem(2p64) (ListItem(3p64) (ListItem(4p64) .List))
13+
14+
syntax Bool ::= "testListUpdate" [function]
15+
// This function only support MInt{64} for now, use MInt{256} can cause undefined behavior
16+
rule testListUpdate => listOfMInt[2p64 <- 10p64] ==K listOfMInt[2 <- 10p64]
17+
18+
endmodule

0 commit comments

Comments
 (0)