mirror of https://github.com/crytic/slither
parent
010d84125a
commit
4319bb3605
@ -1,65 +1,76 @@ |
||||
from slither.tools.properties.properties.properties import Property, PropertyType, PropertyReturn, PropertyCaller |
||||
from slither.tools.properties.properties.properties import ( |
||||
Property, |
||||
PropertyType, |
||||
PropertyReturn, |
||||
PropertyCaller, |
||||
) |
||||
|
||||
ERC20_CONFIG = [ |
||||
|
||||
Property(name='init_total_supply()', |
||||
description='The total supply is correctly initialized.', |
||||
content=''' |
||||
\t\treturn this.totalSupply() >= 0 && this.totalSupply() == initialTotalSupply;''', |
||||
type=PropertyType.CODE_QUALITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=False, |
||||
caller=PropertyCaller.ANY), |
||||
|
||||
Property(name='init_owner_balance()', |
||||
description="Owner's balance is correctly initialized.", |
||||
content=''' |
||||
\t\treturn initialBalance_owner == this.balanceOf(crytic_owner);''', |
||||
type=PropertyType.CODE_QUALITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=False, |
||||
caller=PropertyCaller.ANY), |
||||
|
||||
Property(name='init_user_balance()', |
||||
description="User's balance is correctly initialized.", |
||||
content=''' |
||||
\t\treturn initialBalance_user == this.balanceOf(crytic_user);''', |
||||
type=PropertyType.CODE_QUALITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=False, |
||||
caller=PropertyCaller.ANY), |
||||
|
||||
Property(name='init_attacker_balance()', |
||||
description="Attacker's balance is correctly initialized.", |
||||
content=''' |
||||
\t\treturn initialBalance_attacker == this.balanceOf(crytic_attacker);''', |
||||
type=PropertyType.CODE_QUALITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=False, |
||||
caller=PropertyCaller.ANY), |
||||
|
||||
Property(name='init_caller_balance()', |
||||
description="All the users have a positive balance.", |
||||
content=''' |
||||
\t\treturn this.balanceOf(msg.sender) >0 ;''', |
||||
type=PropertyType.CODE_QUALITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=False, |
||||
caller=PropertyCaller.ALL), |
||||
|
||||
Property( |
||||
name="init_total_supply()", |
||||
description="The total supply is correctly initialized.", |
||||
content=""" |
||||
\t\treturn this.totalSupply() >= 0 && this.totalSupply() == initialTotalSupply;""", |
||||
type=PropertyType.CODE_QUALITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=False, |
||||
caller=PropertyCaller.ANY, |
||||
), |
||||
Property( |
||||
name="init_owner_balance()", |
||||
description="Owner's balance is correctly initialized.", |
||||
content=""" |
||||
\t\treturn initialBalance_owner == this.balanceOf(crytic_owner);""", |
||||
type=PropertyType.CODE_QUALITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=False, |
||||
caller=PropertyCaller.ANY, |
||||
), |
||||
Property( |
||||
name="init_user_balance()", |
||||
description="User's balance is correctly initialized.", |
||||
content=""" |
||||
\t\treturn initialBalance_user == this.balanceOf(crytic_user);""", |
||||
type=PropertyType.CODE_QUALITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=False, |
||||
caller=PropertyCaller.ANY, |
||||
), |
||||
Property( |
||||
name="init_attacker_balance()", |
||||
description="Attacker's balance is correctly initialized.", |
||||
content=""" |
||||
\t\treturn initialBalance_attacker == this.balanceOf(crytic_attacker);""", |
||||
type=PropertyType.CODE_QUALITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=False, |
||||
caller=PropertyCaller.ANY, |
||||
), |
||||
Property( |
||||
name="init_caller_balance()", |
||||
description="All the users have a positive balance.", |
||||
content=""" |
||||
\t\treturn this.balanceOf(msg.sender) >0 ;""", |
||||
type=PropertyType.CODE_QUALITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=False, |
||||
caller=PropertyCaller.ALL, |
||||
), |
||||
# Note: there is a potential overflow on the addition, but we dont consider it |
||||
Property(name='init_total_supply_is_balances()', |
||||
description="The total supply is the user and owner balance.", |
||||
content=''' |
||||
\t\treturn this.balanceOf(crytic_owner) + this.balanceOf(crytic_user) + this.balanceOf(crytic_attacker) == this.totalSupply();''', |
||||
type=PropertyType.CODE_QUALITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=False, |
||||
caller=PropertyCaller.ANY), |
||||
] |
||||
Property( |
||||
name="init_total_supply_is_balances()", |
||||
description="The total supply is the user and owner balance.", |
||||
content=""" |
||||
\t\treturn this.balanceOf(crytic_owner) + this.balanceOf(crytic_user) + this.balanceOf(crytic_attacker) == this.totalSupply();""", |
||||
type=PropertyType.CODE_QUALITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=False, |
||||
caller=PropertyCaller.ANY, |
||||
), |
||||
] |
||||
|
@ -1,13 +1,20 @@ |
||||
from slither.tools.properties.properties.properties import PropertyType, PropertyReturn, Property, PropertyCaller |
||||
from slither.tools.properties.properties.properties import ( |
||||
PropertyType, |
||||
PropertyReturn, |
||||
Property, |
||||
PropertyCaller, |
||||
) |
||||
|
||||
ERC20_NotMintable = [ |
||||
Property(name='crytic_supply_constant_ERC20PropertiesNotMintable()', |
||||
description='The total supply does not increase.', |
||||
content=''' |
||||
\t\treturn initialTotalSupply >= totalSupply();''', |
||||
type=PropertyType.MEDIUM_SEVERITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=True, |
||||
caller=PropertyCaller.ANY), |
||||
Property( |
||||
name="crytic_supply_constant_ERC20PropertiesNotMintable()", |
||||
description="The total supply does not increase.", |
||||
content=""" |
||||
\t\treturn initialTotalSupply >= totalSupply();""", |
||||
type=PropertyType.MEDIUM_SEVERITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=True, |
||||
caller=PropertyCaller.ANY, |
||||
), |
||||
] |
||||
|
@ -1,14 +1,20 @@ |
||||
from slither.tools.properties.properties.properties import Property, PropertyType, PropertyReturn, PropertyCaller |
||||
from slither.tools.properties.properties.properties import ( |
||||
Property, |
||||
PropertyType, |
||||
PropertyReturn, |
||||
PropertyCaller, |
||||
) |
||||
|
||||
ERC20_NotMintableNotBurnable = [ |
||||
|
||||
Property(name='crytic_supply_constant_ERC20PropertiesNotMintableNotBurnable()', |
||||
description='The total supply does not change.', |
||||
content=''' |
||||
\t\treturn initialTotalSupply == this.totalSupply();''', |
||||
type=PropertyType.MEDIUM_SEVERITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=True, |
||||
caller=PropertyCaller.ANY), |
||||
] |
||||
Property( |
||||
name="crytic_supply_constant_ERC20PropertiesNotMintableNotBurnable()", |
||||
description="The total supply does not change.", |
||||
content=""" |
||||
\t\treturn initialTotalSupply == this.totalSupply();""", |
||||
type=PropertyType.MEDIUM_SEVERITY, |
||||
return_type=PropertyReturn.SUCCESS, |
||||
is_unit_test=True, |
||||
is_property_test=True, |
||||
caller=PropertyCaller.ANY, |
||||
), |
||||
] |
||||
|
@ -1,11 +1,23 @@ |
||||
from .initialization import (InitializablePresent, InitializableInherited, |
||||
InitializableInitializer, MissingInitializerModifier, MissingCalls, MultipleCalls, InitializeTarget) |
||||
from .initialization import ( |
||||
InitializablePresent, |
||||
InitializableInherited, |
||||
InitializableInitializer, |
||||
MissingInitializerModifier, |
||||
MissingCalls, |
||||
MultipleCalls, |
||||
InitializeTarget, |
||||
) |
||||
|
||||
from .functions_ids import IDCollision, FunctionShadowing |
||||
|
||||
from .variable_initialization import VariableWithInit |
||||
|
||||
from .variables_order import (MissingVariable, DifferentVariableContractProxy, |
||||
DifferentVariableContractNewContract, ExtraVariablesProxy, ExtraVariablesNewContract) |
||||
from .variables_order import ( |
||||
MissingVariable, |
||||
DifferentVariableContractProxy, |
||||
DifferentVariableContractNewContract, |
||||
ExtraVariablesProxy, |
||||
ExtraVariablesNewContract, |
||||
) |
||||
|
||||
from .constant import WereConstant, BecameConstant |
||||
from .constant import WereConstant, BecameConstant |
||||
|
@ -1,13 +1,12 @@ |
||||
|
||||
from slither.visitors.expression.expression import ExpressionVisitor |
||||
|
||||
class HasConditional(ExpressionVisitor): |
||||
|
||||
class HasConditional(ExpressionVisitor): |
||||
def result(self): |
||||
# == True, to convert None to false |
||||
return self._result is True |
||||
|
||||
def _post_conditional_expression(self, expression): |
||||
# if self._result is True: |
||||
# raise('Slither does not support nested ternary operator') |
||||
# if self._result is True: |
||||
# raise('Slither does not support nested ternary operator') |
||||
self._result = True |
||||
|
Loading…
Reference in new issue