Pi-Squared-Inc / solidity-demo-semantics

Demonstration Solidity Semantics in K
2 stars 2 forks source link

Uniswap modifications to enable summarization #28

Closed mariaKt closed 2 weeks ago

mariaKt commented 2 weeks ago

This PR creates a copy of the UniswapV2Swap test, and makes the following changes, mostly related to names:

The test has been locally tested to rewrite to .K for the provided input.

mariaKt commented 2 weeks ago

I set up the infrastructure for testing in the examples directory. The idea is that we may want to execute a contract with multiple .tnx files , or none. So, I chose the convention that the transactions will have the same directory structure as the examples directory, but for each C.sol file there will be a matching directory, named C. C will contain all transaction files .tnx we want to execute C.sol with. For each T.tnx, C will also contain the corresponding reference output T.ref.