Certora shows rule (kiss_with_revert) as 'skipped'

balajiram · August 6, 2022, 8:05pm

Am I doing anything wrong ?

monseabrb/dss-gate/blob/certora/certora/Gate1.spec#L79


      
          {
            env e;
          
          
  kiss(e, usr);
          
          
  assert(bud(usr) == 1, "The bud method did not add integration as expected.");
          
          
}
          
          
// Verify that method 'kiss' reverts as expected
          rule kiss_with_revert(address usr)
          {
            env e;
          
          
  uint256 _withdrawAfter = withdrawafter();
          
          
  uint256 _wardStatus = wards(e.msg.sender);
            uint256 _budStatus = bud(usr); // TODO : requireinvariant bud can be only 0 or 1.
            require(bud(usr) == 0 || bud(usr) == 1, "bud should be either 0 or 1");
          
          
  kiss@withrevert(e, usr);

balajiram · August 6, 2022, 8:13pm

never mind, found the issue(camelcase). The method name withdrawAfter() vs withdrawafter() should match.

Topic		Replies	Views
Prover does not find inherited function CVL Support cli , types , cvl	2	197	April 13, 2023
Need example of a couple types of functions Epoch Infinity	4	296	March 11, 2022
Rules that involves external contract interactions keep time out CVL Support cvl	15	431	March 30, 2023
Function overloading warning	5	478	March 9, 2022
Is it possible to specify arguments to an arbitrary function? CVL Support	1	381	March 21, 2022

Certora shows rule (kiss_with_revert) as 'skipped'

Related Topics