Function overloading warning

5

Thanks a lot for the detailed and clear answers!

  1. Re the unwinding condition in a loop - name() and symbol() are getters of string types. strings are being handled internally with loops (because they are of dynamic size) which make necessitate careful handling.
    Since here the name and the symbol aren’t interesting for any rules, you can either filter them out with the filtered feature, or you can use the optimistic_loop to make them pass.

By the filtered feature, do you mean filtered {}? Example. Is there more information about the keyword? I tried to search for its usage in the documents but I didn’t find it.

SpartanProtocol invoked add_liquidity function which, in turn, called balanceOf of a specific ERC20 token. Since the the function balanceOf does not exist in SpartanProtocol, and you never linked the ERC20.sol as part of your verification context, then the prover doesn’t know what this function does.

By linking ERC20.sol, could you direct me how to do it? I tried the following command but it seems not helpful.

certoraRun SpartaProtocolPool.sol ERC20.sol --verify SpartaProtocolPool:Spartan.spec

I saw the option --link but I’m not sure if it can be used here.

  1. Re the function pointer error - im not sure what triggered it, i will need some more info to understand. To get a more elaborative error message. On your list of jobs go to the run that failed and click on the clipboard on the right (right next to the abort job button). Send this link so we can go through the text.

An example is this dump. The first two lines:

Syntax warning in spec file: using a function pointer for a function with overloadings (SpartaProtocolPool.constructor(), SpartaProtocolPool.constructor(address,address)), returning the first overloading
Syntax warning in spec file: using a function pointer for a function with overloadings (SpartaProtocolPool.constructor(), SpartaProtocolPool.constructor(address,address)), returning the first overloading

Much appreciated. :pray: