Prover does not find inherited function

CVL Support
, ,
1

Hello,

I am trying to update an existing specification for DssVest to properly check my updated implementation. DssVest now inherits from Openzeppelin’s ERC2771Context, which means it uses _msgSender() instead of msg.sender everywhere.
Obviously I have to reflect that in the spec, and tried to do so. But the prover says it is unable to find the function in the contract. Click one of the yellow “[something]_revert” checks to find this error message:

ERROR:

Rule-check skipped. Skipping reason: Rule unrestrict_revert cannot be compiled since '_msgSender' does not exist in checked contract 'DssVestMintable'.

This is weird: this function is inherited, it should be there. Can anybody tell me how to fix this, please?

2

Hi @malteish,

_msgSender() is an internal function. Therefore the prover doesn’t know about it. You can only call public/external functions.

You can either change its visibility or use e.msg.sender in your rules instead.

3

Ah yes, I didn’t think of that. e.msg.sender doesn’t necessarily return the same as _msgSender() though, because of meta transactions.
I guess I will try to inherit from DssVest and expose a public function that just does a return _msgSender().

Thank you for pointing me in this direction!