Minor improvements. Add example

examples/slither-prop/contracts/ERC20.sol

@@ -0,0 +1,43 @@
+
+contract ERC20Buggy {
+
+    uint256 public _totalSupply;
+    mapping(address => uint) public _balanceOf;
+    mapping(address => mapping(address => uint)) public _allowance;
+
+    function transfer(address to, uint256 value) public returns (bool success){
+        _balanceOf[msg.sender] -= value;
+        _balanceOf[to] += value;
+        return true;
+    }
+
+    function transferFrom(address from, address to, uint256 value) public returns (bool success){
+        if(_allowance[msg.sender][from] >= value){
+            _allowance[msg.sender][from] -= value;
+            _balanceOf[from] -= value;
+            _balanceOf[to] += value;
+            return true;
+        }
+        return false;
+    }
+
+    function approve(address _spender, uint256 value) public returns (bool success){
+        _allowance[msg.sender][_spender] = value;
+        return true;
+    }
+
+    function balanceOf(address from) public returns(uint) {
+        return _balanceOf[from];
+    }
+
+    function allowance(address from, address to) public returns(uint) {
+        return _allowance[from][to];
+    }
+
+    function totalSupply() public returns(uint){
+        return _totalSupply;
+    }
+
+    event Transfer(address indexed _from, address indexed _to, uint256 _value);
+    event Approval(address indexed _owner, address indexed _spender, uint256 _value);
+}

examples/slither-prop/contracts/Migrations.sol

@@ -0,0 +1,18 @@
+pragma solidity >=0.4.25 <0.7.0;
+
+contract Migrations {
+  address public owner;
+  uint public last_completed_migration;
+
+  modifier restricted() {
+    if (msg.sender == owner) _;
+  }
+
+  constructor() public {
+    owner = msg.sender;
+  }
+
+  function setCompleted(uint completed) public restricted {
+    last_completed_migration = completed;
+  }
+}

examples/slither-prop/migrations/1_initial_migration.js

@@ -0,0 +1,5 @@
+const Migrations = artifacts.require("Migrations");
+
+module.exports = function(deployer) {
+  deployer.deploy(Migrations);
+};

slither/tools/properties/__main__.py

@@ -3,6 +3,8 @@ import argparse
 import logging
 import sys
 
+from prettytable import PrettyTable
+
 from slither import Slither
 from crytic_compile import cryticparser
 
@@ -30,6 +32,14 @@ def _all_scenarios():
 
     return txt
 
+def _all_properties():
+    table = PrettyTable(["Num", "Description", "Scenario"])
+    idx = 0
+    for scenario, value in ERC20_PROPERTIES.items():
+        for prop in value.properties:
+            table.add_row([idx, prop.description, scenario])
+            idx = idx + 1
+    return table
 
 class ListScenarios(argparse.Action):
     def __call__(self, parser, *args, **kwargs):
@@ -37,6 +47,12 @@ class ListScenarios(argparse.Action):
         parser.exit()
 
 
+class ListProperties(argparse.Action):
+    def __call__(self, parser, *args, **kwargs):
+        logger.info(_all_properties())
+        parser.exit()
+
+
 def parse_args():
     """
     Parse the underlying arguments for the program.
@@ -62,6 +78,12 @@ def parse_args():
                         nargs=0,
                         default=False)
 
+    parser.add_argument('--list-properties',
+                        help='List available properties',
+                        action=ListProperties,
+                        nargs=0,
+                        default=False)
+
     parser.add_argument('--address-owner',
                         help=f'Owner address. Default {OWNER_ADDRESS}',
                         default=None)
@@ -92,8 +114,14 @@ def main():
 
     contract = slither.get_contract_from_name(args.contract)
     if not contract:
-        logger.error(f'{args.contract} not found')
-        return
+        if len(slither.contracts) == 1:
+            contract = slither.contracts[0]
+        else:
+            if args.contract is None:
+                logger.error(f'Specify the target: --contract ContractName')
+            else:
+                logger.error(f'{args.contract} not found')
+            return
 
     addresses = Addresses(args.address_owner, args.address_user, args.address_attacker)
 

slither/tools/properties/platforms/truffle.py

@@ -115,7 +115,10 @@ def generate_unit_test(test_contract: str, filename: str,
 
     content += '});\n'
 
-    output_dir = Path(output_dir, 'test', 'crytic')
+    output_dir = Path(output_dir, 'test')
+    output_dir.mkdir(exist_ok=True)
+
+    output_dir = Path(output_dir, 'crytic')
     output_dir.mkdir(exist_ok=True)
 
     write_file(output_dir, filename, content)
@@ -138,6 +141,8 @@ module.exports = function(deployer) {{
 
     output_dir = Path(output_dir, 'migrations')
 
+    output_dir.mkdir(exist_ok=True)
+
     migration_files = [js_file for js_file in output_dir.iterdir() if js_file.suffix == '.js'
                        and PATTERN_TRUFFLE_MIGRATION.match(js_file.name)]
 

slither/tools/properties/solidity/generate_properties.py

@@ -46,7 +46,7 @@ def generate_test_contract(contract: Contract,
     content += initialization_recommendation
     content += '\t\t// \n'
     content += '\t\t// \n'
-    content += '\t\t// Update the following if totalSupply and balanceOf are external functions:\n\n'
+    content += '\t\t// Update the following if totalSupply and balanceOf are external functions or state variables:\n\n'
     content += '\t\tinitialTotalSupply = totalSupply();\n'
     content += '\t\tinitialBalance_owner = balanceOf(crytic_owner);\n'
     content += '\t\tinitialBalance_user = balanceOf(crytic_user);\n'

slither/utils/type.py

@@ -38,6 +38,12 @@ def export_return_type_from_variable(variable):
     :param variable
     :return: Type
     """
+    if isinstance(variable, MappingType):
+        return export_return_type_from_variable(variable.type_to)
+
+    if isinstance(variable, ArrayType):
+        return variable.type
+
     if isinstance(variable.type, MappingType):
         return export_return_type_from_variable(variable.type.type_to)