Change effect of assert to invalid opcode.

1 files changed, 6 insertions, 3 deletions

diff --git a/docs/control-structures.rst b/docs/control-structures.rst
index df8ac729..f1b2e6da 100644
--- a/docs/control-structures.rst
+++ b/docs/control-structures.rst
@@ -398,10 +398,13 @@ Currently, Solidity automatically generates a runtime exception in the following
 
 While a user-provided exception is generated in the following situations:
 #. Calling ``throw``.
-#. The condition of ``assert(condition)`` is not met.
 
 Internally, Solidity performs a revert operation (instruction ``0xfd``) when a user-provided exception is thrown. In contrast, it performs an invalid operation
-(instruction ``0xfe``) if a runtime exception is encountered. In both cases, this causes
+(instruction ``0xfe``) if a runtime exception is encountered or the condition of an ``assert`` call is not met. In both cases, this causes
 the EVM to revert all changes made to the state. The reason for this is that there is no safe way to continue execution, because an expected effect
 did not occur. Because we want to retain the atomicity of transactions, the safest thing to do is to revert all changes and make the whole transaction
-(or at least call) without effect.
\ No newline at end of file
+(or at least call) without effect.
+
+If contracts are written so that ``assert`` is only used to test internal conditions and ``throw`` or
+``revert`` is used in case of malformed input, a formal analysis tool that verifies that the invalid
+opcode can never be reached can be used to check for the absence of errors assuming valid inputs.