search

Pi-Squared-Inc / solidity-demo-semantics

Demonstration Solidity Semantics in K
2 stars 2 forks source link

Uniswapv2librarygetreserves summary #48

Closed mariaKt closed 1 month ago

mariaKt commented 1 month ago

This PR adds summaries for the body of the function Uniswapv2librarygetreserves. https://github.com/Pi-Squared-Inc/solidity-demo-semantics/blob/4fb604f8d6c138a7cb0a04059592f447021f6490/test/examples/swaps/UniswapV2SwapRenamed.sol#L275

We stop before the call to getReserves, as it is through an unknown address.

These summaries save 972 steps (22667 -> 21695).

mariaKt commented 1 month ago

@Robertorosmaninho sure. Can you clarify where it is you want me to anotate? It is matched only when it is Statements in the <contract-fn-body> cell.

Robertorosmaninho commented 1 month ago

@Robertorosmaninho sure. Can you clarify where it is you want me to anotate? It is matched only when it is Statements in the <contract-fn-body> cell.

Yes, my idea was to have Ss:Statements in the k cell too. But it's fine as it is as well!!

mariaKt commented 1 month ago

Alright. Since this is OK with you, I will leave it as is, because I prefer annotations in the LHS myself.