@@ -108,7 +108,7 @@ test-prove-dss:
108
108
109
109
.PHONY : test-integration
110
110
test-integration :
111
- $(MAKE ) -C kevm-pyk/ test-integration PYTEST_ARGS+=' -k "(test_kast.py or test_run.py or test_solc_to_k.py )"'
111
+ $(MAKE ) -C kevm-pyk/ test-integration PYTEST_ARGS+=' -k "(test_kast.py or test_run.py)"'
112
112
113
113
.PHONY : profile
114
114
profile :
@@ -131,28 +131,6 @@ KPROVE_EXT = k
131
131
KEVM_OPTS ?=
132
132
KPROVE_OPTS ?=
133
133
134
-
135
- tests/specs/examples/% -bin-runtime.k : KEVM_OPTS += --verbose
136
-
137
- tests/specs/examples/erc20-spec/haskell/timestamp : tests/specs/examples/erc20-bin-runtime.k
138
- .PHONY : tests/specs/examples/erc20-bin-runtime.k
139
- tests/specs/examples/erc20-bin-runtime.k : tests/specs/examples/ERC20.sol $(KEVM_LIB ) /$(haskell_kompiled )
140
- $(KEVM ) solc-to-k $< ERC20 $(KEVM_OPTS ) --verbose --definition $(KEVM_LIB ) /$(haskell_dir ) --main-module ERC20-VERIFICATION > $@
141
-
142
- tests/specs/examples/erc721-spec/haskell/timestamp : tests/specs/examples/erc721-bin-runtime.k
143
- .PHONY : tests/specs/examples/erc721-bin-runtime.k
144
- tests/specs/examples/erc721-bin-runtime.k : tests/specs/examples/ERC721.sol $(KEVM_LIB ) /$(haskell_kompiled )
145
- $(KEVM ) solc-to-k $< ERC721 $(KEVM_OPTS ) --verbose --definition $(KEVM_LIB ) /$(haskell_dir ) --main-module ERC721-VERIFICATION > $@
146
-
147
- tests/specs/examples/storage-spec/haskell/timestamp : tests/specs/examples/storage-bin-runtime.k
148
- .PHONY : tests/specs/examples/storage-bin-runtime.k
149
- tests/specs/examples/storage-bin-runtime.k : tests/specs/examples/Storage.sol $(KEVM_LIB ) /$(haskell_kompiled )
150
- $(KEVM ) solc-to-k $< Storage $(KEVM_OPTS ) --verbose --definition $(KEVM_LIB ) /$(haskell_dir ) --main-module STORAGE-VERIFICATION > $@
151
-
152
- .PHONY : tests/specs/examples/empty-bin-runtime.k
153
- tests/specs/examples/empty-bin-runtime.k : tests/specs/examples/Empty.sol $(KEVM_LIB ) /$(haskell_kompiled )
154
- $(KEVM ) solc-to-k $< Empty $(KEVM_OPTS ) --verbose --definition $(KEVM_LIB ) /$(haskell_dir ) --main-module EMPTY-VERIFICATION > $@
155
-
156
134
.SECONDEXPANSION :
157
135
tests/specs/% .prove : tests/specs/% tests/specs/$$(firstword $$(subst /, ,$$* ) ) /$$(KPROVE_FILE ) /$(TEST_SYMBOLIC_BACKEND ) /timestamp
158
136
$(UV_RUN ) kevm-pyk prove $< $(KEVM_OPTS ) $(KPROVE_OPTS ) \
0 commit comments