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
How Certora seeds the contract state when running a rule? CVL Support	3	332	March 2, 2022
UNRESOLVED Auto summary CVL Support	1	234	October 20, 2022
Unable to understand the error General Discussion	4	310	July 4, 2022
Did Certora not support interface cast? CVL Support	3	250	November 2, 2022
Prover does not find inherited function CVL Support cli , types , cvl	2	240	April 13, 2023

Certora shows rule (kiss_with_revert) as 'skipped'

Related Topics