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.
Yes this is exactly what im talking about. unfortunately we don’t have documentation on that at the moment. we are working on moving our docs to readthedocs, improve it and add many examples. You can find it here
The filtered is pretty straight forward. It will filter out/in function you specify on the specific rule. for example if i write f.selector != isView
, then view function will not be processed when running a rule. this is useful mainly to reduce run-time complexity - for example if we want to check that a function doesn’t change a var state, we can filter out view function since they cannot change state. You’ll have to use examples to learn the syntax at the moment. if you need more examples/help ask for it and we’ll find and explain the syntax more thoroughly.
By linking ERC20.sol
, could you direct me how to do it? I tried the following command but it seems not helpful.
multi-contract is an important functionality as many contracts communicate with other contracts. You will find some explanations here and here. In some cases you may also need to use linking which (unsurprisingly) links an instance of another contract that appear in the contract you are verifying. You can read about it in the docs here, but here’s an example anyway:
contract Aux{
unit a;
uint b
uint c;
function foo(uint g) public returns (bool){
...
}
}
contract Use_Aux{
Aux q;
uint r;
bool s;
function bar(){
s = q.foo(r)
...
}
}
In the example above, if you try to verify contract Use_Aux
, then q
, the instance of Aux
is unknown to the prover. you will have to link it, meaning you will have to tell the prover the instance q
is of type Aux
, you can find it in Aux.sol
.
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
There’s a difference between a warning and an error.
A syntax warning basically notify you that things are not fully defined and so the prover, behind the scenes, complete what ever it needed to run.
While a syntax error will hard stop the run due to ambiguity and unclear intentions.
In the case that you point out, it seems like the a constructor is defined as taking 2 args, but the spec seems to know only a constructor that takes no args. Im not sure why that is happening, it can occur due to wrong craft of harness file that inherits from the parent contract, or maybe wrong declaration of methods (though constructors are no usually declared).
In any case that warning tells you that something automatic happened, which may or may not be what you intended so you need to pay attention to it.