Pi-Squared-Inc / solidity-demo-semantics

Demonstration Solidity Semantics in K
2 stars 2 forks source link

Summary for the body of setUp #44

Closed mariaKt closed 1 month ago

mariaKt commented 1 month ago

This PR adds a summarized rule for the body of the function setUp of the uniswapV2SwapTest contract. https://github.com/Pi-Squared-Inc/solidity-demo-semantics/blob/b1c267efb4298bacb4be09dd1715441b489d22ed/test/examples/swaps/UniswapV2SwapRenamed.sol#L697

We do not summarize the call itself, since this is a public function.

The code in setUp contains no branches. This includes the constructor of uniswapV2Swap https://github.com/Pi-Squared-Inc/solidity-demo-semantics/blob/b1c267efb4298bacb4be09dd1715441b489d22ed/test/examples/swaps/UniswapV2SwapRenamed.sol#L24 which creates a new uniswapV2Router02 and then calls its public function setLocalPair. https://github.com/Pi-Squared-Inc/solidity-demo-semantics/blob/b1c267efb4298bacb4be09dd1715441b489d22ed/test/examples/swaps/UniswapV2SwapRenamed.sol#L213 Because we statically know the address, we can summarize these calls as well.