Potential spurious Re-Entrancy Vulnerability findings:

[nuevoalex]

I recently ran the latest Oyente against the contracts in the Augur project, and for the most part the output looks good, but the detection of Re-Entrancy vulnerabilities seems it may have some issues.

The full output from running against all of our contracts can be found here: https://gist.github.com/nuevoalex/d6c05e546189a4dc90802b179e75478a

Here is an example of a case where Re-Entrancy was detected:

contract /home/alex/Work/augur-core/source/contracts/trading/FillOrder.sol:FillOrder:
	============ Results ===========
	  EVM Code Coverage: 			 23.1%
	  Parity Multisig Bug 2: 		 False
	  Callstack Depth Attack Vulnerability:  False
	  Transaction-Ordering Dependence (TOD): True
	  Timestamp Dependency: 		 False
	  Re-Entrancy Vulnerability: 		 True
Flow1
/home/alex/Work/augur-core/source/contracts/trading/FillOrder.sol:56:19: Warning: Transaction-Ordering Dependency.
        Participant creator;
        ^
Spanning multiple lines.
Flow2
/home/alex/Work/augur-core/source/contracts/trading/FillOrder.sol:17:198: Warning: Transaction-Ordering Dependency.
// CONSIDER: At some point it would probably be a good idea to shift much of the logic from trading contracts into extensions. In particular this means sorting for making and WCL calculcations + order walking for taking.
^
Spanning multiple lines.
/home/alex/Work/augur-core/source/contracts/trading/FillOrder.sol:379:27: Warning: Re-Entrancy Vulnerability.
        uint256 _result = this.fillOrder(msg.sender, _orderId, _amountFillerWants, _tradeGroupId)
/home/alex/Work/augur-core/source/contracts/trading/FillOrder.sol:17:198: Warning: Re-Entrancy Vulnerability.
// CONSIDER: At some point it would probably be a good idea to shift much of the logic from trading contracts into extensions. In particular this means sorting for making and WCL calculcations + order walking for taking.
^
Spanning multiple lines.
/home/alex/Work/augur-core/source/contracts/trading/FillOrder.sol:32:33: Warning: Re-Entrancy Vulnerability.
        IShareToken[] shortShareTokens;
        ^
Spanning multiple lines.
/home/alex/Work/augur-core/source/contracts/trading/FillOrder.sol:28:13: Warning: Re-Entrancy Vulnerability.
        IMarket market;
        ^
Spanning multiple lines.
/home/alex/Work/augur-core/source/contracts/trading/FillOrder.sol:381:9: Warning: Re-Entrancy Vulnerability.
        _market.assertBalances()
/home/alex/Work/augur-core/source/contracts/trading/FillOrder.sol:34:6: Warning: Re-Entrancy Vulnerability.
    }
    ^
Spanning multiple lines.
/home/alex/Work/augur-core/source/contracts/trading/FillOrder.sol:17:184: Warning: Re-Entrancy Vulnerability.
// CONSIDER: At some point it would probably be a good idea to shift much of the logic from trading contracts into extensions. In particular this means sorting for making and WCL calculcations + order walking fo
/home/alex/Work/augur-core/source/contracts/trading/FillOrder.sol:380:35: Warning: Re-Entrancy Vulnerability.
        IMarket _market = IOrders(controller.lookup("Orders")
/home/alex/Work/augur-core/source/contracts/trading/FillOrder.sol:380:27: Warning: Re-Entrancy Vulnerability.
        IMarket _market = IOrders(controller.lookup("Orders")).getMarket(_orderId)
/home/alex/Work/augur-core/source/contracts/trading/FillOrder.sol:38:24: Warning: Re-Entrancy Vulnerability.
        uint256 outcome;
        ^
Spanning multiple lines.
/home/alex/Work/augur-core/source/contracts/trading/FillOrder.sol:30:13: Warning: Re-Entrancy Vulnerability.
        ICash denominationToken;
        ^
Spanning multiple lines.
	====== Analysis Completed ======

I'm certain at least some portion of this is unintended (The cases that are comments or variable declaration), but more generally it seems to be providing a lot of false positives for this vulnerability case unless I'm missing something.

[luongnt95]

Thanks for reporting the bug. Will be working on it