|
|
|
@ -37,7 +37,7 @@ ERC20_Transferable = [ |
|
|
|
|
name="crytic_less_than_total_ERC20Properties()", |
|
|
|
|
description="Balance of one user must be less or equal to the total supply.", |
|
|
|
|
content=""" |
|
|
|
|
\t\treturn this.balanceOf(msg.sender) <= totalSupply();""", |
|
|
|
|
\t\treturn this.balanceOf(msg.sender) <= this.totalSupply();""", |
|
|
|
|
type=PropertyType.MEDIUM_SEVERITY, |
|
|
|
|
return_type=PropertyReturn.SUCCESS, |
|
|
|
|
is_unit_test=True, |
|
|
|
@ -48,7 +48,7 @@ ERC20_Transferable = [ |
|
|
|
|
name="crytic_totalSupply_consistant_ERC20Properties()", |
|
|
|
|
description="Balance of the crytic users must be less or equal to the total supply.", |
|
|
|
|
content=""" |
|
|
|
|
\t\treturn this.balanceOf(crytic_owner) + this.balanceOf(crytic_user) + this.balanceOf(crytic_attacker) <= totalSupply();""", |
|
|
|
|
\t\treturn this.balanceOf(crytic_owner) + this.balanceOf(crytic_user) + this.balanceOf(crytic_attacker) <= this.totalSupply();""", |
|
|
|
|
type=PropertyType.MEDIUM_SEVERITY, |
|
|
|
|
return_type=PropertyReturn.SUCCESS, |
|
|
|
|
is_unit_test=True, |
|
|
|
|