Merge pull request #2219 from ethereum/develop

Release for version 0.4.11

20 files changed, 770 insertions, 226 deletions

diff --git a/docs/assembly.rst b/docs/assembly.rst
index 415bb1a1..420cea17 100644
--- a/docs/assembly.rst
+++ b/docs/assembly.rst
@@ -11,7 +11,7 @@ differs from standalone assembly and then specify assembly itself.
 
 TODO: Write about how scoping rules of inline assembly are a bit different
 and the complications that arise when for example using internal functions
-of libraries. Furhermore, write about the symbols defined by the compiler.
+of libraries. Furthermore, write about the symbols defined by the compiler.
 
 Inline Assembly
 ===============
@@ -29,7 +29,7 @@ arising when writing manual assembly by the following features:
 * labels: ``let x := 10  repeat: x := sub(x, 1) jumpi(repeat, eq(x, 0))``
 * loops: ``for { let i := 0 } lt(i, x) { i := add(i, 1) } { y := mul(2, y) }``
 * switch statements: ``switch x case 0: { y := mul(x, 2) } default: { y := 0 }``
-* function calls: ``function f(x) -> (y) { switch x case 0: { y := 1 } default: { y := mul(x, f(sub(x, 1))) }   }``
+* function calls: ``function f(x) -> y { switch x case 0: { y := 1 } default: { y := mul(x, f(sub(x, 1))) }   }``
 
 .. note::
     Of the above, loops, function calls and switch statements are not yet implemented.
@@ -323,9 +323,12 @@ Access to External Variables and Functions
 ------------------------------------------
 
 Solidity variables and other identifiers can be accessed by simply using their name.
-For storage and memory variables, this will push the address and not the value onto the
-stack. Also note that non-struct and non-array storage variable addresses occupy two slots
-on the stack: One for the address and one for the byte offset inside the storage slot.
+For memory variables, this will push the address and not the value onto the
+stack. Storage variables are different: Values in storage might not occupy a
+full storage slot, so their "address" is composed of a slot and a byte-offset
+inside that slot. To retrieve the slot pointed to by the variable ``x``, you
+used ``x_slot`` and to retrieve the byte-offset you used ``x_offset``.
+
 In assignments (see below), we can even use local Solidity variables to assign to.
 
 Functions external to inline assembly can also be accessed: The assembly will
@@ -340,17 +343,13 @@ changes during the call, and thus references to local variables will be wrong.
 
 .. code::
 
-    pragma solidity ^0.4.0;
+    pragma solidity ^0.4.11;
 
     contract C {
         uint b;
         function f(uint x) returns (uint r) {
             assembly {
-                b pop // remove the offset, we know it is zero
-                sload
-                x
-                mul
-                =: r  // assign to return variable r
+                r := mul(x, sload(b_slot)) // ignore the offset, we know it is zero
             }
         }
     }
@@ -567,7 +566,7 @@ The following example implements the power function by square-and-multiply.
 .. code::
 
     assembly {
-        function power(base, exponent) -> (result) {
+        function power(base, exponent) -> result {
             switch exponent
             0: { result := 1 }
             1: { result := base }
@@ -702,12 +701,12 @@ The following assembly will be generated::
       }
       default: { jump(invalidJumpLabel) }
       // memory allocator
-      function $allocate(size) -> (pos) {
+      function $allocate(size) -> pos {
         pos := mload(0x40)
         mstore(0x40, add(pos, size))
       }
       // the contract function
-      function f(x) -> (y) {
+      function f(x) -> y {
         y := 1
         for { let i := 0 } lt(i, x) { i := add(i, 1) } {
           y := mul(2, y)
diff --git a/docs/bugs.json b/docs/bugs.json
new file mode 100644
index 00000000..1a67d626
--- /dev/null
+++ b/docs/bugs.json
@@ -0,0 +1,103 @@
+[
+    {
+        "name": "ConstantOptimizerSubtraction",
+        "summary": "In some situations, the optimizer replaces certain numbers in the code with routines that compute different numbers.",
+        "description": "The optimizer tries to represent any number in the bytecode by routines that compute them with less gas. For some special numbers, an incorrect routine is generated. This could allow an attacker to e.g. trick victims about a specific amount of ether, or function calls to call different functions (or none at all).",
+        "link": "https://blog.ethereum.org/2017/05/03/solidity-optimizer-bug/",
+        "fixed": "0.4.11",
+        "severity": "low",
+        "conditions": {
+            "optimizer": true
+        }
+    },
+    {
+        "name": "IdentityPrecompileReturnIgnored",
+        "summary": "Failure of the identity precompile was ignored.",
+        "description": "Calls to the identity contract, which is used for copying memory, ignored its return value. On the public chain, calls to the identity precompile can be made in a way that they never fail, but this might be different on private chains.",
+        "severity": "low",
+        "fixed": "0.4.7"
+    },
+    {
+        "name": "OptimizerStateKnowledgeNotResetForJumpdest",
+        "summary": "The optimizer did not properly reset its internal state at jump destinations, which could lead to data corruption.",
+        "description": "The optimizer performs symbolic execution at certain stages. At jump destinations, multiple code paths join and thus it has to compute a common state from the incoming edges. Computing this common state was simplified to just use the empty state, but this implementation was not done properly. This bug can cause data corruption.",
+        "severity": "medium",
+        "introduced": "0.4.5",
+        "fixed": "0.4.6",
+        "conditions": {
+            "optimizer": true
+        }
+    },
+    {
+        "name": "HighOrderByteCleanStorage",
+        "summary": "For short types, the high order bytes were not cleaned properly and could overwrite existing data.",
+        "description": "Types shorter than 32 bytes are packed together into the same 32 byte storage slot, but storage writes always write 32 bytes. For some types, the higher order bytes were not cleaned properly, which made it sometimes possible to overwrite a variable in storage when writing to another one.",
+        "link": "https://blog.ethereum.org/2016/11/01/security-alert-solidity-variables-can-overwritten-storage/",
+        "severity": "high",
+        "introduced": "0.1.6",
+        "fixed": "0.4.4"
+    },
+    {
+        "name": "OptimizerStaleKnowledgeAboutSHA3",
+        "summary": "The optimizer did not properly reset its knowledge about SHA3 operations resulting in some hashes (also used for storage variable positions) not being calculated correctly.",
+        "description": "The optimizer performs symbolic execution in order to save re-evaluating expressions whose value is already known. This knowledge was not properly reset across control flow paths and thus the optimizer sometimes thought that the result of a SHA3 operation is already present on the stack. This could result in data corruption by accessing the wrong storage slot.",
+        "severity": "medium",
+        "fixed": "0.4.3",
+        "conditions": {
+            "optimizer": true
+        }
+    },
+    {
+        "name": "LibrariesNotCallableFromPayableFunctions",
+        "summary": "Library functions threw an exception when called from a call that received Ether.",
+        "description": "Library functions are protected against sending them Ether through a call. Since the DELEGATECALL opcode forwards the information about how much Ether was sent with a call, the library function incorrectly assumed that Ether was sent to the library and threw an exception.",
+        "severity": "low",
+        "introduced": "0.4.0",
+        "fixed": "0.4.2"
+    },
+    {
+        "name": "SendFailsForZeroEther",
+        "summary": "The send function did not provide enough gas to the recipient if no Ether was sent with it.",
+        "description": "The recipient of an Ether transfer automatically receives a certain amount of gas from the EVM to handle the transfer. In the case of a zero-transfer, this gas is not provided which causes the recipient to throw an exception.",
+        "severity": "low",
+        "fixed": "0.4.0"
+    },
+    {
+        "name": "DynamicAllocationInfiniteLoop",
+        "summary": "Dynamic allocation of an empty memory array caused an infinite loop and thus an exception.",
+        "description": "Memory arrays can be created provided a length. If this length is zero, code was generated that did not terminate and thus consumed all gas.",
+        "severity": "low",
+        "fixed": "0.3.6"
+    },
+    {
+        "name": "OptimizerClearStateOnCodePathJoin",
+        "summary": "The optimizer did not properly reset its internal state at jump destinations, which could lead to data corruption.",
+        "description": "The optimizer performs symbolic execution at certain stages. At jump destinations, multiple code paths join and thus it has to compute a common state from the incoming edges. Computing this common state was not done correctly. This bug can cause data corruption, but it is probably quite hard to use for targeted attacks.",
+        "severity": "low",
+        "fixed": "0.3.6",
+        "conditions": {
+            "optimizer": true
+        }
+    },
+    {
+        "name": "CleanBytesHigherOrderBits",
+        "summary": "The higher order bits of short bytesNN types were not cleaned before comparison.",
+        "description": "Two variables of type bytesNN were considered different if their higher order bits, which are not part of the actual value, were different. An attacker might use this to reach seemingly unreachable code paths by providing incorrectly formatted input data.",
+        "severity": "medium/high",
+        "fixed": "0.3.3"
+    },
+    {
+        "name": "ArrayAccessCleanHigherOrderBits",
+        "summary": "Access to array elements for arrays of types with less than 32 bytes did not correctly clean the higher order bits, causing corruption in other array elements.",
+        "description": "Multiple elements of an array of values that are shorter than 17 bytes are packed into the same storage slot. Writing to a single element of such an array did not properly clean the higher order bytes and thus could lead to data corruption.",
+        "severity": "medium/high",
+        "fixed": "0.3.1"
+    },
+    {
+        "name": "AncientCompiler",
+        "summary": "This compiler version is ancient and might contain several undocumented or undiscovered bugs.",
+        "description": "The list of bugs is only kept for compiler versions starting from 0.3.0, so older versions might contain undocumented bugs.",
+        "severity": "high",
+        "fixed": "0.3.0"
+    }
+]
\ No newline at end of file
diff --git a/docs/bugs.rst b/docs/bugs.rst
new file mode 100644
index 00000000..55771a35
--- /dev/null
+++ b/docs/bugs.rst
@@ -0,0 +1,61 @@
+.. index:: Bugs
+
+.. _known_bugs:
+
+##################
+List of Known Bugs
+##################
+
+Below, you can find a JSON-formatted list of some of the known security-relevant bugs in the
+Solidity compiler. The file itself is hosted in the `Github repository
+<https://github.com/ethereum/solidity/blob/develop/docs/bugs.json>`_.
+The list stretches back as far as version 0.3.0, bugs known to be present only
+in versions preceding that are not listed.
+
+There is another file called `bugs_by_version.json
+<https://github.com/ethereum/solidity/blob/develop/docs/bugs_by_version.json>`_,
+which can be used to check which bugs affect a specific version of the compiler.
+
+Contract source verification tools and also other tools interacting with
+contracts should consult this list according to the following criteria:
+
+ - It is mildly suspicious if a contract was compiled with a nightly
+   compiler version instead of a released version. This list does not keep
+   track of unreleased or nightly versions.
+ - It is also mildly suspicious if a contract was compiled with a version that was
+   not the most recent at the time the contract was created. For contracts
+   created from other contracts, you have to follow the creation chain
+   back to a transaction and use the date of that transaction as creation date.
+ - It is highly suspicious if a contract was compiled with a compiler that
+   contains a known bug and the contract was created at a time where a newer
+   compiler version containing a fix was already released.
+
+The JSON file of known bugs below is an array of objects, one for each bug,
+with the following keys:
+
+name
+    Unique name given to the bug
+summary
+    Short description of the bug
+description
+    Detailed description of the bug
+link
+    URL of a website with more detailed information, optional
+introduced
+    The first published compiler version that contained the bug, optional
+fixed
+    The first published compiler version that did not contain the bug anymore
+publish
+    The date at which the bug became known publicly, optional
+severity
+    Severity of the bug: low, medium, high. Takes into account
+    discoverability in contract tests, likelihood of occurrence and
+    potential damage by exploits.
+conditions
+    Conditions that have to be met to trigger the bug. Currently, this
+    is an object that can contain a boolean value ``optimizer``, which
+    means that the optimizer has to be switched on to enable the bug.
+    If no conditions are given, assume that the bug is present.
+
+.. literalinclude:: bugs.json
+   :language: js
diff --git a/docs/bugs_by_version.json b/docs/bugs_by_version.json
new file mode 100644
index 00000000..0f7346b4
--- /dev/null
+++ b/docs/bugs_by_version.json
@@ -0,0 +1,334 @@
+{
+    "0.1.0": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin", 
+            "CleanBytesHigherOrderBits", 
+            "ArrayAccessCleanHigherOrderBits", 
+            "AncientCompiler"
+        ], 
+        "released": "2015-07-10"
+    }, 
+    "0.1.1": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin", 
+            "CleanBytesHigherOrderBits", 
+            "ArrayAccessCleanHigherOrderBits", 
+            "AncientCompiler"
+        ], 
+        "released": "2015-08-04"
+    }, 
+    "0.1.2": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin", 
+            "CleanBytesHigherOrderBits", 
+            "ArrayAccessCleanHigherOrderBits", 
+            "AncientCompiler"
+        ], 
+        "released": "2015-08-20"
+    }, 
+    "0.1.3": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin", 
+            "CleanBytesHigherOrderBits", 
+            "ArrayAccessCleanHigherOrderBits", 
+            "AncientCompiler"
+        ], 
+        "released": "2015-09-25"
+    }, 
+    "0.1.4": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin", 
+            "CleanBytesHigherOrderBits", 
+            "ArrayAccessCleanHigherOrderBits", 
+            "AncientCompiler"
+        ], 
+        "released": "2015-09-30"
+    }, 
+    "0.1.5": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin", 
+            "CleanBytesHigherOrderBits", 
+            "ArrayAccessCleanHigherOrderBits", 
+            "AncientCompiler"
+        ], 
+        "released": "2015-10-07"
+    }, 
+    "0.1.6": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin", 
+            "CleanBytesHigherOrderBits", 
+            "ArrayAccessCleanHigherOrderBits", 
+            "AncientCompiler"
+        ], 
+        "released": "2015-10-16"
+    }, 
+    "0.1.7": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin", 
+            "CleanBytesHigherOrderBits", 
+            "ArrayAccessCleanHigherOrderBits", 
+            "AncientCompiler"
+        ], 
+        "released": "2015-11-17"
+    }, 
+    "0.2.0": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin", 
+            "CleanBytesHigherOrderBits", 
+            "ArrayAccessCleanHigherOrderBits", 
+            "AncientCompiler"
+        ], 
+        "released": "2015-12-02"
+    }, 
+    "0.2.1": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin", 
+            "CleanBytesHigherOrderBits", 
+            "ArrayAccessCleanHigherOrderBits", 
+            "AncientCompiler"
+        ], 
+        "released": "2016-01-30"
+    }, 
+    "0.2.2": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin", 
+            "CleanBytesHigherOrderBits", 
+            "ArrayAccessCleanHigherOrderBits", 
+            "AncientCompiler"
+        ], 
+        "released": "2016-02-17"
+    }, 
+    "0.3.0": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin", 
+            "CleanBytesHigherOrderBits", 
+            "ArrayAccessCleanHigherOrderBits"
+        ], 
+        "released": "2016-03-11"
+    }, 
+    "0.3.1": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin", 
+            "CleanBytesHigherOrderBits"
+        ], 
+        "released": "2016-03-31"
+    }, 
+    "0.3.2": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin", 
+            "CleanBytesHigherOrderBits"
+        ], 
+        "released": "2016-04-18"
+    }, 
+    "0.3.3": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin"
+        ], 
+        "released": "2016-05-27"
+    }, 
+    "0.3.4": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin"
+        ], 
+        "released": "2016-05-31"
+    }, 
+    "0.3.5": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther", 
+            "DynamicAllocationInfiniteLoop", 
+            "OptimizerClearStateOnCodePathJoin"
+        ], 
+        "released": "2016-06-10"
+    }, 
+    "0.3.6": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "SendFailsForZeroEther"
+        ], 
+        "released": "2016-08-10"
+    }, 
+    "0.4.0": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "LibrariesNotCallableFromPayableFunctions"
+        ], 
+        "released": "2016-09-08"
+    }, 
+    "0.4.1": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3", 
+            "LibrariesNotCallableFromPayableFunctions"
+        ], 
+        "released": "2016-09-09"
+    }, 
+    "0.4.10": {
+        "bugs": [
+            "ConstantOptimizerSubtraction"
+        ], 
+        "released": "2017-03-15"
+    }, 
+    "0.4.11": {
+        "bugs": [], 
+        "released": "2017-05-03"
+    }, 
+    "0.4.2": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage", 
+            "OptimizerStaleKnowledgeAboutSHA3"
+        ], 
+        "released": "2016-09-17"
+    }, 
+    "0.4.3": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "HighOrderByteCleanStorage"
+        ], 
+        "released": "2016-10-25"
+    }, 
+    "0.4.4": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored"
+        ], 
+        "released": "2016-10-31"
+    }, 
+    "0.4.5": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored", 
+            "OptimizerStateKnowledgeNotResetForJumpdest"
+        ], 
+        "released": "2016-11-21"
+    }, 
+    "0.4.6": {
+        "bugs": [
+            "ConstantOptimizerSubtraction", 
+            "IdentityPrecompileReturnIgnored"
+        ], 
+        "released": "2016-11-22"
+    }, 
+    "0.4.7": {
+        "bugs": [
+            "ConstantOptimizerSubtraction"
+        ], 
+        "released": "2016-12-15"
+    }, 
+    "0.4.8": {
+        "bugs": [
+            "ConstantOptimizerSubtraction"
+        ], 
+        "released": "2017-01-13"
+    }, 
+    "0.4.9": {
+        "bugs": [
+            "ConstantOptimizerSubtraction"
+        ], 
+        "released": "2017-01-31"
+    }
+}
\ No newline at end of file
diff --git a/docs/common-patterns.rst b/docs/common-patterns.rst
index a2d7ce71..acef13b7 100644
--- a/docs/common-patterns.rst
+++ b/docs/common-patterns.rst
@@ -23,12 +23,12 @@ contract in order to become the "richest", inspired by
 `King of the Ether <https://www.kingoftheether.com/>`_.
 
 In the following contract, if you are usurped as the richest,
-you will recieve the funds of the person who has gone on to
+you will receive the funds of the person who has gone on to
 become the new richest.
 
 ::
 
-    pragma solidity ^0.4.0;
+    pragma solidity ^0.4.11;
 
     contract WithdrawalContract {
         address public richest;
@@ -52,17 +52,12 @@ become the new richest.
             }
         }
 
-        function withdraw() returns (bool) {
+        function withdraw() {
             uint amount = pendingWithdrawals[msg.sender];
             // Remember to zero the pending refund before
             // sending to prevent re-entrancy attacks
             pendingWithdrawals[msg.sender] = 0;
-            if (msg.sender.send(amount)) {
-                return true;
-            } else {
-                pendingWithdrawals[msg.sender] = amount;
-                return false;
-            }
+            msg.sender.transfer(amount);
         }
     }
 
@@ -70,7 +65,7 @@ This is as opposed to the more intuitive sending pattern:
 
 ::
 
-    pragma solidity ^0.4.0;
+    pragma solidity ^0.4.11;
 
     contract SendContract {
         address public richest;
@@ -83,12 +78,8 @@ This is as opposed to the more intuitive sending pattern:
 
         function becomeRichest() payable returns (bool) {
             if (msg.value > mostSent) {
-                // Check if call succeeds to prevent an attacker
-                // from trapping the previous person's funds in
-                // this contract through a callstack attack
-                if (!richest.send(msg.value)) {
-                    throw;
-                }
+                // This line can cause problems (explained below).
+                richest.transfer(msg.value);
                 richest = msg.sender;
                 mostSent = msg.value;
                 return true;
@@ -100,12 +91,16 @@ This is as opposed to the more intuitive sending pattern:
 
 Notice that, in this example, an attacker could trap the
 contract into an unusable state by causing ``richest`` to be
-the address of a  contract that has a fallback function
-which consumes more than the 2300 gas stipend.  That way,
-whenever ``send`` is called to deliver funds to the
-"poisoned" contract, it will cause execution to always fail
-because there will not be enough gas to finish the execution
-of the fallback function.
+the address of a contract that has a fallback function
+which fails (e.g. by using ``revert()`` or by just
+conssuming more than the 2300 gas stipend). That way,
+whenever ``transfer`` is called to deliver funds to the
+"poisoned" contract, it will fail and thus also ``becomeRichest``
+will fail, with the contract being stuck forever.
+
+In contrast, if you use the "withdraw" pattern from the first example,
+the attacker can only cause his or her own withdraw to fail and not the
+rest of the contract's workings.
 
 .. index:: access;restricting
 
@@ -135,7 +130,7 @@ restrictions highly readable.
 
 ::
 
-    pragma solidity ^0.4.0;
+    pragma solidity ^0.4.11;
 
     contract AccessRestriction {
         // These will be assigned at the construction
@@ -152,8 +147,7 @@ restrictions highly readable.
         // a certain address.
         modifier onlyBy(address _account)
         {
-            if (msg.sender != _account)
-                throw;
+            require(msg.sender == _account);
             // Do not forget the "_;"! It will
             // be replaced by the actual function
             // body when the modifier is used.
@@ -169,7 +163,7 @@ restrictions highly readable.
         }
 
         modifier onlyAfter(uint _time) {
-            if (now < _time) throw;
+            require(now >= _time);
             _;
         }
 
@@ -190,8 +184,7 @@ restrictions highly readable.
         // This was dangerous before Solidity version 0.4.0,
         // where it was possible to skip the part after `_;`.
         modifier costs(uint _amount) {
-            if (msg.value < _amount)
-                throw;
+            require(msg.value >= _amount);
             _;
             if (msg.value > _amount)
                 msg.sender.send(msg.value - _amount);
@@ -232,7 +225,7 @@ reached at a certain point in **time**.
 An example for this is a blind auction contract which
 starts in the stage "accepting blinded bids", then
 transitions to "revealing bids" which is ended by
-"determine auction autcome".
+"determine auction outcome".
 
 .. index:: function;modifier
 
@@ -276,7 +269,7 @@ function finishes.
 
 ::
 
-    pragma solidity ^0.4.0;
+    pragma solidity ^0.4.11;
 
     contract StateMachine {
         enum Stages {
@@ -293,7 +286,7 @@ function finishes.
         uint public creationTime = now;
 
         modifier atStage(Stages _stage) {
-            if (stage != _stage) throw;
+            require(stage == _stage);
             _;
         }
 
diff --git a/docs/contracts.rst b/docs/contracts.rst
index 9145f016..8d7af2c1 100644
--- a/docs/contracts.rst
+++ b/docs/contracts.rst
@@ -27,7 +27,7 @@ From ``web3.js``, i.e. the JavaScript
 API, this is done as follows::
 
     // Need to specify some source including contract name for the data param below
-    var source = "contract CONTRACT_NAME { function CONTRACT_NAME(unit a, uint b) {} }";
+    var source = "contract CONTRACT_NAME { function CONTRACT_NAME(uint a, uint b) {} }";
 
     // The json abi array generated by the compiler
     var abiArray = [
@@ -327,7 +327,7 @@ inheritable properties of contracts and may be overridden by derived contracts.
 
 ::
 
-    pragma solidity ^0.4.0;
+    pragma solidity ^0.4.11;
 
     contract owned {
         function owned() { owner = msg.sender; }
@@ -341,8 +341,7 @@ inheritable properties of contracts and may be overridden by derived contracts.
         // function is executed and otherwise, an exception is
         // thrown.
         modifier onlyOwner {
-            if (msg.sender != owner)
-                throw;
+            require(msg.sender == owner);
             _;
         }
     }
@@ -390,7 +389,7 @@ inheritable properties of contracts and may be overridden by derived contracts.
     contract Mutex {
         bool locked;
         modifier noReentrancy() {
-            if (locked) throw;
+            require(!locked);
             locked = true;
             _;
             locked = false;
@@ -401,7 +400,7 @@ inheritable properties of contracts and may be overridden by derived contracts.
         /// The `return 7` statement assigns 7 to the return value but still
         /// executes the statement `locked = false` in the modifier.
         function f() noReentrancy returns (uint) {
-            if (!msg.sender.call()) throw;
+            require(msg.sender.call());
             return 7;
         }
     }
@@ -436,7 +435,7 @@ execution data (``msg.gas``) or make calls to external contracts are disallowed.
 that might have a side-effect on memory allocation are allowed, but those that
 might have a side-effect on other memory objects are not. The built-in functions
 ``keccak256``, ``sha256``, ``ripemd160``, ``ecrecover``, ``addmod`` and ``mulmod``
-are allowed (ever though they do call external contracts).
+are allowed (even though they do call external contracts).
 
 The reason behind allowing side-effects on the memory allocator is that it
 should be possible to construct complex objects like e.g. lookup-tables.
@@ -922,6 +921,35 @@ Such contracts cannot be compiled (even if they contain implemented functions al
 
 If a contract inherits from an abstract contract and does not implement all non-implemented functions by overriding, it will itself be abstract.
 
+.. index:: ! contract;interface, ! interface contract
+
+**********
+Interfaces
+**********
+
+Interfaces are similar to abstract contracts, but they cannot have any functions implemented. There are further restrictions:
+
+#. Cannot inherit other contracts or interfaces.
+#. Cannot define constructor.
+#. Cannot define variables.
+#. Cannot define structs.
+#. Cannot define enums.
+
+Some of these restrictions might be lifted in the future.
+
+Interfaces are basically limited to what the Contract ABI can represent and the conversion between the ABI and
+an Interface should be possible without any information loss.
+
+Interfaces are denoted by their own keyword:
+
+::
+
+    interface Token {
+        function transfer(address recipient, uint amount);
+    }
+
+Contracts can inherit interfaces as they would inherit other contracts.
+
 .. index:: ! library, callcode, delegatecall
 
 .. _libraries:
@@ -960,7 +988,7 @@ more advanced example to implement a set).
 
 ::
 
-    pragma solidity ^0.4.0;
+    pragma solidity ^0.4.11;
 
     library Set {
       // We define a new struct datatype that will be used to
@@ -1006,8 +1034,7 @@ more advanced example to implement a set).
             // The library functions can be called without a
             // specific instance of the library, since the
             // "instance" will be the current contract.
-            if (!Set.insert(knownValues, value))
-                throw;
+            require(Set.insert(knownValues, value));
         }
         // In this contract, we can also directly access knownValues.flags, if we want.
     }
@@ -1101,7 +1128,7 @@ Restrictions for libraries in comparison to contracts:
 
 - No state variables
 - Cannot inherit nor be inherited
-- Cannot recieve Ether
+- Cannot receive Ether
 
 (These might be lifted at a later point.)
 
@@ -1137,7 +1164,7 @@ available without having to add further code.
 Let us rewrite the set example from the
 :ref:`libraries` in this way::
 
-    pragma solidity ^0.4.0;
+    pragma solidity ^0.4.11;
 
     // This is the same code as before, just without comments
     library Set {
@@ -1178,8 +1205,7 @@ Let us rewrite the set example from the
             // corresponding member functions.
             // The following function call is identical to
             // Set.insert(knownValues, value)
-            if (!knownValues.insert(value))
-                throw;
+            require(knownValues.insert(value));
         }
     }
 
diff --git a/docs/control-structures.rst b/docs/control-structures.rst
index 25bf203b..a2d34274 100644
--- a/docs/control-structures.rst
+++ b/docs/control-structures.rst
@@ -113,8 +113,8 @@ actual contract has not been created yet.
 Functions of other contracts have to be called externally. For an external call,
 all function arguments have to be copied to memory.
 
-When calling functions
-of other contracts, the amount of Wei sent with the call and the gas can be specified::
+When calling functions of other contracts, the amount of Wei sent with the call and
+the gas can be specified with special options ``.value()`` and ``.gas()``, respectively::
 
     contract InfoFeed {
         function info() payable returns (uint ret) { return 42; }
@@ -127,8 +127,8 @@ of other contracts, the amount of Wei sent with the call and the gas can be spec
         function callFeed() { feed.info.value(10).gas(800)(); }
     }
 
-The modifier ``payable`` has to be used for ``info``, because otherwise,
-we would not be able to send Ether to it in the call ``feed.info.value(10).gas(800)()``.
+The modifier ``payable`` has to be used for ``info``, because otherwise, the `.value()`
+option would not be available.
 
 Note that the expression ``InfoFeed(addr)`` performs an explicit type conversion stating
 that "we know that the type of the contract at the given address is ``InfoFeed``" and
@@ -235,7 +235,7 @@ creation-dependencies are not possible.
         }
     }
 
-As seen in the example, it is possible to forward Ether to the creation,
+As seen in the example, it is possible to forward Ether to the creation using the ``.value()`` option,
 but it is not possible to limit the amount of gas. If the creation fails
 (due to out-of-stack, not enough balance or other problems), an exception
 is thrown.
@@ -399,6 +399,7 @@ Currently, Solidity automatically generates a runtime exception in the following
 #. If you call ``assert`` with an argument that evaluates to false.
 
 While a user-provided exception is generated in the following situations:
+
 #. Calling ``throw``.
 #. Calling ``require`` with an argument that evaluates to ``false``.
 
@@ -411,4 +412,4 @@ did not occur. Because we want to retain the atomicity of transactions, the safe
 
 If contracts are written so that ``assert`` is only used to test internal conditions and ``require``
 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.
\ No newline at end of file
+opcode can never be reached can be used to check for the absence of errors assuming valid inputs.
diff --git a/docs/frequently-asked-questions.rst b/docs/frequently-asked-questions.rst
index 8a68ae5b..03ee8388 100644
--- a/docs/frequently-asked-questions.rst
+++ b/docs/frequently-asked-questions.rst
@@ -68,7 +68,7 @@ creator. Save it. Then ``selfdestruct(creator);`` to kill and return funds.
 
 Note that if you ``import "mortal"`` at the top of your contracts and declare
 ``contract SomeContract is mortal { ...`` and compile with a compiler that already
-has it (which includes `browser-solidity <https://ethereum.github.io/browser-solidity/>`_), then
+has it (which includes `Remix <https://remix.ethereum.org/>`_), then
 ``kill()`` is taken care of for you. Once a contract is "mortal", then you can
 ``contractname.kill.sendTransaction({from:eth.coinbase})``, just the same as my
 examples.
@@ -665,8 +665,7 @@ What does the following strange check do in the Custom Token contract?
 
 ::
 
-    if (balanceOf[_to] + _value < balanceOf[_to])
-        throw;
+    require((balanceOf[_to] + _value) >= balanceOf[_to]);
 
 Integers in Solidity (and most other machine-related programming languages) are restricted to a certain range.
 For ``uint256``, this is ``0`` up to ``2**256 - 1``. If the result of some operation on those numbers
diff --git a/docs/index.rst b/docs/index.rst
index fc1a4231..1312864a 100644
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -2,7 +2,7 @@ Solidity
 ========
 
 Solidity is a contract-oriented, high-level language whose syntax is similar to that of JavaScript
-and it is designed to target the Ethereum Virtual Machine.
+and it is designed to target the Ethereum Virtual Machine (EVM).
 
 Solidity is statically typed, supports inheritance, libraries and complex
 user-defined types among other features.
@@ -11,8 +11,8 @@ As you will see, it is possible to create contracts for voting,
 crowdfunding, blind auctions, multi-signature wallets and more.
 
 .. note::
-    The best way to try out Solidity right now is using the
-    `Browser-Based Compiler <https://ethereum.github.io/browser-solidity/>`_
+    The best way to try out Solidity right now is using
+    `Remix <https://remix.ethereum.org/>`_
     (it can take a while to load, please be patient).
 
 Useful links
@@ -33,7 +33,7 @@ Useful links
 Available Solidity Integrations
 -------------------------------
 
-* `Browser-Based Compiler <https://ethereum.github.io/browser-solidity/>`_
+* `Remix <https://remix.ethereum.org/>`_
     Browser-based IDE with integrated compiler and Solidity runtime environment without server-side components.
 
 * `Ethereum Studio <https://live.ether.camp/>`_
@@ -48,12 +48,12 @@ Available Solidity Integrations
 * `Package for SublimeText — Solidity language syntax <https://packagecontrol.io/packages/Ethereum/>`_
     Solidity syntax highlighting for SublimeText editor.
 
-* `Atom Ethereum interface <https://github.com/gmtDevs/atom-ethereum-interface>`_
-    Plugin for the Atom editor that features syntax highlighting, compilation and a runtime environment (requires backend node).
+* `Etheratom <https://github.com/0mkara/etheratom>`_
+    Plugin for the Atom editor that features syntax highlighting, compilation and a runtime environment (Backend node & VM compatible).
 
 * `Atom Solidity Linter <https://atom.io/packages/linter-solidity>`_
     Plugin for the Atom editor that provides Solidity linting.
-    
+
 * `Solium <https://github.com/duaraghav8/Solium/>`_
     A commandline linter for Solidity which strictly follows the rules prescribed by the `Solidity Style Guide <http://solidity.readthedocs.io/en/latest/style-guide.html>`_.
 
@@ -78,8 +78,8 @@ Discontinued:
 Solidity Tools
 --------------
 
-* `Dapple <https://github.com/nexusdev/dapple>`_
-    Package and deployment manager for Solidity.
+* `Dapp <https://dapp.readthedocs.io>`_
+    Build tool, package manager, and deployment assistant for Solidity.
 
 * `Solidity REPL <https://github.com/raineorshine/solidity-repl>`_
     Try Solidity instantly with a command-line Solidity console.
@@ -90,6 +90,9 @@ Solidity Tools
 * `evmdis <https://github.com/Arachnid/evmdis>`_
     EVM Disassembler that performs static analysis on the bytecode to provide a higher level of abstraction than raw EVM operations.
 
+* `Doxity <https://github.com/DigixGlobal/doxity>`_
+    Documentation Generator for Solidity.
+
 Third-Party Solidity Parsers and Grammars
 -----------------------------------------
 
@@ -109,7 +112,7 @@ and the :ref:`Ethereum Virtual Machine <the-ethereum-virtual-machine>`.
 The next section will explain several *features* of Solidity by giving
 useful :ref:`example contracts <voting>`
 Remember that you can always try out the contracts
-`in your browser <https://ethereum.github.io/browser-solidity>`_!
+`in your browser <https://remix.ethereum.org>`_!
 
 The last and most extensive section will cover all aspects of Solidity in depth.
 
@@ -136,5 +139,6 @@ Contents
    using-the-compiler.rst
    style-guide.rst
    common-patterns.rst
+   bugs.rst
    contributing.rst
    frequently-asked-questions.rst
diff --git a/docs/installing-solidity.rst b/docs/installing-solidity.rst
index fb405475..a2a3c3da 100644
--- a/docs/installing-solidity.rst
+++ b/docs/installing-solidity.rst
@@ -15,11 +15,11 @@ are not guaranteed to be working and despite best efforts they might contain und
 and/or broken changes. We recommend using the latest release. Package installers below
 will use the latest release.
 
-Browser-Solidity
-================
+Remix
+=====
 
 If you just want to try Solidity for small contracts, you
-can try `browser-solidity <https://ethereum.github.io/browser-solidity>`_
+can try `Remix <https://remix.ethereum.org/>`_
 which does not need any installation. If you want to use it
 without connection to the Internet, you can go to
 https://github.com/ethereum/browser-solidity/tree/gh-pages and
@@ -31,7 +31,7 @@ npm / Node.js
 This is probably the most portable and most convenient way to install Solidity locally.
 
 A platform-independent JavaScript library is provided by compiling the C++ source
-into JavaScript using Emscripten. It can be used in projects directly (such as Browser-Solidity).
+into JavaScript using Emscripten. It can be used in projects directly (such as Remix).
 Please refer to the `solc-js <https://github.com/ethereum/solc-js>`_ repository for instructions.
 
 It also contains a commandline tool called `solcjs`, which can be installed via npm:
@@ -250,6 +250,7 @@ The version string in detail
 ============================
 
 The Solidity version string contains four parts:
+
 - the version number
 - pre-release tag, usually set to ``develop.YYYY.MM.DD`` or ``nightly.YYYY.MM.DD``
 - commit in the format of ``commit.GITHASH``
@@ -280,4 +281,4 @@ Example:
 3. a breaking change is introduced - version is bumped to 0.5.0
 4. the 0.5.0 release is made
 
-This behaviour works well with the version pragma.
+This behaviour works well with the  :ref:`version pragma <version_pragma>`.
diff --git a/docs/introduction-to-smart-contracts.rst b/docs/introduction-to-smart-contracts.rst
index f02447cf..9001a08c 100644
--- a/docs/introduction-to-smart-contracts.rst
+++ b/docs/introduction-to-smart-contracts.rst
@@ -146,7 +146,7 @@ single account.
 
 The line ``event Sent(address from, address to, uint amount);`` declares
 a so-called "event" which is fired in the last line of the function
-``send``. User interfaces (as well as server appliances of course) can
+``send``. User interfaces (as well as server applications of course) can
 listen for those events being fired on the blockchain without much
 cost. As soon as it is fired, the listener will also receive the
 arguments ``from``, ``to`` and ``amount``, which makes it easy to track
@@ -161,7 +161,7 @@ transactions. In order to listen for this event, you would use ::
                 "Sender: " + Coin.balances.call(result.args.from) +
                 "Receiver: " + Coin.balances.call(result.args.to));
         }
-    }
+    })
 
 Note how the automatically generated function ``balances`` is called from
 the user interface.
diff --git a/docs/layout-of-source-files.rst b/docs/layout-of-source-files.rst
index 1e27b7c0..715b29ae 100644
--- a/docs/layout-of-source-files.rst
+++ b/docs/layout-of-source-files.rst
@@ -7,6 +7,8 @@ and pragma directives.
 
 .. index:: ! pragma, version
 
+.. _version_pragma:
+
 Version Pragma
 ==============
 
@@ -24,7 +26,7 @@ The version pragma is used as follows::
   pragma solidity ^0.4.0;
 
 Such a source file will not compile with a compiler earlier than version 0.4.0
-and it will also not work on a compiler starting form version 0.5.0 (this
+and it will also not work on a compiler starting from version 0.5.0 (this
 second condition is added by using ``^``). The idea behind this is that
 there will be no breaking changes until version ``0.5.0``, so we can always
 be sure that our code will compile the way we intended it to. We do not fix
@@ -151,9 +153,9 @@ remapping ``=/``.
 If there are multiple remappings that lead to a valid file, the remapping
 with the longest common prefix is chosen.
 
-**browser-solidity**:
+**Remix**:
 
-The `browser-based compiler <https://ethereum.github.io/browser-solidity>`_
+`Remix <https://remix.ethereum.org/>`_
 provides an automatic remapping for github and will also automatically retrieve
 the file over the network:
 You can import the iterable mapping by e.g.
diff --git a/docs/miscellaneous.rst b/docs/miscellaneous.rst
index 2865d884..914dfacd 100644
--- a/docs/miscellaneous.rst
+++ b/docs/miscellaneous.rst
@@ -314,6 +314,14 @@ Comments are of course also not permitted and used here only for explanatory pur
       }
     }
 
+.. note::
+    Note the ABI definition above has no fixed order. It can change with compiler versions.
+
+.. note::
+    Since the bytecode of the resulting contract contains the metadata hash, any change to
+    the metadata will result in a change of the bytecode. Furthermore, since the metadata
+    includes a hash of all the sources used, a single whitespace change in any of the source
+    codes will result in a different metadata, and subsequently a different bytecode.
 
 Encoding of the Metadata Hash in the Bytecode
 =============================================
diff --git a/docs/security-considerations.rst b/docs/security-considerations.rst
index 77e1bf08..33c613d8 100644
--- a/docs/security-considerations.rst
+++ b/docs/security-considerations.rst
@@ -22,7 +22,11 @@ you should be more careful.
 This section will list some pitfalls and general security recommendations but
 can, of course, never be complete. Also, keep in mind that even if your
 smart contract code is bug-free, the compiler or the platform itself might
-have a bug.
+have a bug. A list of some publicly known security-relevant bugs of the compiler
+can be found in the
+:ref:`list of known bugs<known_bugs>`, which is also machine-readable. Note
+that there is a bug bounty program that covers the code generator of the
+Solidity compiler.
 
 As always, with open source documentation, please help us extend this section
 (especially, some examples would not hurt)!
@@ -75,7 +79,7 @@ outlined further below:
 
 ::
 
-  pragma solidity ^0.4.0;
+  pragma solidity ^0.4.11;
 
   contract Fund {
       /// Mapping of ether shares of the contract.
@@ -84,8 +88,7 @@ outlined further below:
       function withdraw() {
           var share = shares[msg.sender];
           shares[msg.sender] = 0;
-          if (!msg.sender.send(share))
-              throw;
+          msg.sender.transfer(share);
       }
   }
 
@@ -117,25 +120,27 @@ Sending and Receiving Ether
   During the execution of the fallback function, the contract can only rely
   on the "gas stipend" (2300 gas) being available to it at that time. This stipend is not enough to access storage in any way.
   To be sure that your contract can receive Ether in that way, check the gas requirements of the fallback function
-  (for example in the "details" section in browser-solidity).
+  (for example in the "details" section in Remix).
 
 - There is a way to forward more gas to the receiving contract using
-  ``addr.call.value(x)()``. This is essentially the same as ``addr.send(x)``,
+  ``addr.call.value(x)()``. This is essentially the same as ``addr.transfer(x)``,
   only that it forwards all remaining gas and opens up the ability for the
-  recipient to perform more expensive actions. This might include calling back
+  recipient to perform more expensive actions (and it only returns a failure code
+  and does not automatically propagate the error). This might include calling back
   into the sending contract or other state changes you might not have thought of.
   So it allows for great flexibility for honest users but also for malicious actors.
 
-- If you want to send Ether using ``address.send``, there are certain details to be aware of:
+- If you want to send Ether using ``address.transfer``, there are certain details to be aware of:
 
   1. If the recipient is a contract, it causes its fallback function to be executed which can, in turn, call back the sending contract.
   2. Sending Ether can fail due to the call depth going above 1024. Since the caller is in total control of the call
-     depth, they can force the transfer to fail; make sure to always check the return value of ``send``. Better yet,
+     depth, they can force the transfer to fail; take this possibility into account or use ``send`` and make sure to always check its return value. Better yet,
      write your contract using a pattern where the recipient can withdraw Ether instead.
   3. Sending Ether can also fail because the execution of the recipient contract
-     requires more than the allotted amount of gas (explicitly by using ``throw`` or
+     requires more than the allotted amount of gas (explicitly by using ``require``,
+     ``assert``, ``revert``, ``throw`` or
      because the operation is just too expensive) - it "runs out of gas" (OOG).
-     If the return value of ``send`` is checked, this might provide a
+     If you use ``transfer`` or ``send`` with a return value check, this might provide a
      means for the recipient to block progress in the sending contract. Again, the best practice here is to use
      a :ref:`"withdraw" pattern instead of a "send" pattern <withdrawal_pattern>`.
 
@@ -158,7 +163,7 @@ Never use tx.origin for authorization. Let's say you have a wallet contract like
 
 ::
 
-    pragma solidity ^0.4.0;
+    pragma solidity ^0.4.11;
 
     // THIS CONTRACT CONTAINS A BUG - DO NOT USE
     contract TxUserWallet {
@@ -168,9 +173,9 @@ Never use tx.origin for authorization. Let's say you have a wallet contract like
             owner = msg.sender;
         }
 
-        function transfer(address dest, uint amount) {
-            if (tx.origin != owner) { throw; }
-            if (!dest.call.value(amount)()) throw;
+        function transferTo(address dest, uint amount) {
+            require(tx.origin == owner);
+            dest.transfer(amount);
         }
     }
 
@@ -188,7 +193,7 @@ Now someone tricks you into sending ether to the address of this attack wallet:
         }
 
         function() {
-            TxUserWallet(msg.sender).transfer(owner, msg.sender.balance);
+            TxUserWallet(msg.sender).transferTo(owner, msg.sender.balance);
         }
     }
 
diff --git a/docs/solidity-by-example.rst b/docs/solidity-by-example.rst
index 7e08c6b4..4ed474df 100644
--- a/docs/solidity-by-example.rst
+++ b/docs/solidity-by-example.rst
@@ -36,7 +36,7 @@ of votes.
 
 ::
 
-    pragma solidity ^0.4.0;
+    pragma solidity ^0.4.11;
 
     /// @title Voting with delegation.
     contract Ballot {
@@ -51,8 +51,7 @@ of votes.
         }
 
         // This is a type for a single proposal.
-        struct Proposal
-        {
+        struct Proposal {
             bytes32 name;   // short name (up to 32 bytes)
             uint voteCount; // number of accumulated votes
         }
@@ -88,14 +87,14 @@ of votes.
         // Give `voter` the right to vote on this ballot.
         // May only be called by `chairperson`.
         function giveRightToVote(address voter) {
-            if (msg.sender != chairperson || voters[voter].voted) {
-                // `throw` terminates and reverts all changes to
-                // the state and to Ether balances. It is often
-                // a good idea to use this if functions are
-                // called incorrectly. But watch out, this
-                // will also consume all provided gas.
-                throw;
-            }
+            // If the argument of `require` evaluates to `false`,
+            // it terminates and reverts all changes to
+            // the state and to Ether balances. It is often
+            // a good idea to use this if functions are
+            // called incorrectly. But watch out, this
+            // will currently also consume all provided gas
+            // (this is planned to change in the future).
+            require((msg.sender == chairperson) && !voters[voter].voted);
             voters[voter].weight = 1;
         }
 
@@ -103,12 +102,10 @@ of votes.
         function delegate(address to) {
             // assigns reference
             Voter sender = voters[msg.sender];
-            if (sender.voted)
-                throw;
+            require(!sender.voted);
 
             // Self-delegation is not allowed.
-            if (to == msg.sender)
-                throw;
+            require(to != msg.sender);
 
             // Forward the delegation as long as
             // `to` also delegated.
@@ -122,8 +119,7 @@ of votes.
                 to = voters[to].delegate;
 
                 // We found a loop in the delegation, not allowed.
-                if (to == msg.sender) 
-                    throw;
+                require(to != msg.sender);
             }
 
             // Since `sender` is a reference, this
@@ -146,8 +142,7 @@ of votes.
         /// to proposal `proposals[proposal].name`.
         function vote(uint proposal) {
             Voter sender = voters[msg.sender];
-            if (sender.voted)
-                throw;
+            require(!sender.voted);
             sender.voted = true;
             sender.vote = proposal;
 
@@ -219,7 +214,7 @@ activate themselves.
 
 ::
 
-    pragma solidity ^0.4.0;
+    pragma solidity ^0.4.11;
 
     contract SimpleAuction {
         // Parameters of the auction. Times are either
@@ -270,22 +265,21 @@ activate themselves.
             // the transaction. The keyword payable
             // is required for the function to
             // be able to receive Ether.
-            if (now > auctionStart + biddingTime) {
-                // Revert the call if the bidding
-                // period is over.
-                throw;
-            }
-            if (msg.value <= highestBid) {
-                // If the bid is not higher, send the
-                // money back.
-                throw;
-            }
+
+            // Revert the call if the bidding
+            // period is over.
+            require(now <= (auctionStart + biddingTime));
+
+            // If the bid is not higher, send the
+            // money back.
+            require(msg.value > highestBid);
+            
             if (highestBidder != 0) {
                 // Sending back the money by simply using
                 // highestBidder.send(highestBid) is a security risk
                 // because it can be prevented by the caller by e.g.
                 // raising the call stack to 1023. It is always safer
-                // to let the recipient withdraw their money themselves.
+                // to let the recipients withdraw their money themselves.
                 pendingReturns[highestBidder] += highestBid;
             }
             highestBidder = msg.sender;
@@ -328,18 +322,15 @@ activate themselves.
             // external contracts.
 
             // 1. Conditions
-            if (now <= auctionStart + biddingTime)
-                throw; // auction did not yet end
-            if (ended)
-                throw; // this function has already been called
+            require(now >= (auctionStart + biddingTime)); // auction did not yet end
+            require(!ended); // this function has already been called
 
             // 2. Effects
             ended = true;
             AuctionEnded(highestBidder, highestBid);
 
             // 3. Interaction
-            if (!beneficiary.send(highestBid))
-                throw;
+            beneficiary.transfer(highestBid);
         }
     }
 
@@ -382,7 +373,7 @@ high or low invalid bids.
 
 ::
 
-    pragma solidity ^0.4.0;
+    pragma solidity ^0.4.11;
 
     contract BlindAuction {
         struct Bid {
@@ -410,8 +401,8 @@ high or low invalid bids.
         /// functions. `onlyBefore` is applied to `bid` below:
         /// The new function body is the modifier's body where
         /// `_` is replaced by the old function body.
-        modifier onlyBefore(uint _time) { if (now >= _time) throw; _; }
-        modifier onlyAfter(uint _time) { if (now <= _time) throw; _; }
+        modifier onlyBefore(uint _time) { require(now < _time); _; }
+        modifier onlyAfter(uint _time) { require(now > _time); _; }
 
         function BlindAuction(
             uint _biddingTime,
@@ -455,13 +446,9 @@ high or low invalid bids.
             onlyBefore(revealEnd)
         {
             uint length = bids[msg.sender].length;
-            if (
-                _values.length != length ||
-                _fake.length != length ||
-                _secret.length != length
-            ) {
-                throw;
-            }
+            require(_values.length == length);
+            require(_fake.length == length);
+            require(_secret.length == length);
 
             uint refund;
             for (uint i = 0; i < length; i++) {
@@ -482,8 +469,7 @@ high or low invalid bids.
                 // the same deposit.
                 bid.blindedBid = 0;
             }
-            if (!msg.sender.send(refund))
-                throw;
+            msg.sender.transfer(refund);
         }
 
         // This is an "internal" function which means that it
@@ -528,14 +514,12 @@ high or low invalid bids.
         function auctionEnd()
             onlyAfter(revealEnd)
         {
-            if (ended)
-                throw;
+            require(!ended);
             AuctionEnded(highestBidder, highestBid);
             ended = true;
             // We send all the money we have, because some
             // of the refunds might have failed.
-            if (!beneficiary.send(this.balance))
-                throw;
+            beneficiary.transfer(this.balance);
         }
     }
 
@@ -547,7 +531,7 @@ Safe Remote Purchase
 
 ::
 
-    pragma solidity ^0.4.0;
+    pragma solidity ^0.4.11;
 
     contract Purchase {
         uint public value;
@@ -559,26 +543,26 @@ Safe Remote Purchase
         function Purchase() payable {
             seller = msg.sender;
             value = msg.value / 2;
-            if (2 * value != msg.value) throw;
+            require((2 * value) == msg.value);
         }
 
-        modifier require(bool _condition) {
-            if (!_condition) throw;
+        modifier condition(bool _condition) {
+            require(_condition);
             _;
         }
 
         modifier onlyBuyer() {
-            if (msg.sender != buyer) throw;
+            require(msg.sender == buyer);
             _;
         }
 
         modifier onlySeller() {
-            if (msg.sender != seller) throw;
+            require(msg.sender == seller);
             _;
         }
 
         modifier inState(State _state) {
-            if (state != _state) throw;
+            require(state == _state);
             _;
         }
 
@@ -595,8 +579,7 @@ Safe Remote Purchase
         {
             aborted();
             state = State.Inactive;
-            if (!seller.send(this.balance))
-                throw;
+            seller.transfer(this.balance);
         }
 
         /// Confirm the purchase as buyer.
@@ -605,7 +588,7 @@ Safe Remote Purchase
         /// is called.
         function confirmPurchase()
             inState(State.Created)
-            require(msg.value == 2 * value)
+            condition(msg.value == (2 * value))
             payable
         {
             purchaseConfirmed();
@@ -624,10 +607,12 @@ Safe Remote Purchase
             // otherwise, the contracts called using `send` below
             // can call in again here.
             state = State.Inactive;
-            // This actually allows both the buyer and the seller to
-            // block the refund.
-            if (!buyer.send(value) || !seller.send(this.balance))
-                throw;
+
+            // NOTE: This actually allows both the buyer and the seller to
+            // block the refund - the withdraw pattern should be used.
+
+            buyer.transfer(value);
+            seller.transfer(this.balance));
         }
     }
 
diff --git a/docs/structure-of-a-contract.rst b/docs/structure-of-a-contract.rst
index 24ef69a6..224eb368 100644
--- a/docs/structure-of-a-contract.rst
+++ b/docs/structure-of-a-contract.rst
@@ -62,13 +62,13 @@ Function modifiers can be used to amend the semantics of functions in a declarat
 
 ::
 
-  pragma solidity ^0.4.0;
+  pragma solidity ^0.4.11;
 
   contract Purchase {
       address public seller;
 
       modifier onlySeller() { // Modifier
-          if (msg.sender != seller) throw;
+          require(msg.sender == seller);
           _;
       }
 
diff --git a/docs/style-guide.rst b/docs/style-guide.rst
index 9aae3d7b..0742d2e9 100644
--- a/docs/style-guide.rst
+++ b/docs/style-guide.rst
@@ -164,7 +164,7 @@ Functions should be grouped according to their visibility and ordered:
 - internal
 - private
 
-Within a grouping, place the `constant` functions last.
+Within a grouping, place the ``constant`` functions last.
 
 Yes::
 
diff --git a/docs/types.rst b/docs/types.rst
index 243a9a0c..c400aecb 100644
--- a/docs/types.rst
+++ b/docs/types.rst
@@ -64,6 +64,12 @@ expression ``x << y`` is equivalent to ``x * 2**y`` and ``x >> y`` is
 equivalent to ``x / 2**y``. This means that shifting negative numbers
 sign extends. Shifting by a negative amount throws a runtime exception.
 
+.. warning::
+    The results produced by shift right of negative values of signed integer types is different from those produced
+    by other programming languages. In Solidity, shift right maps to division so the shifted negative values
+    are going to be rounded towards zero (truncated). In other programming languages the shift right of negative values
+    works like division with rounding down (towards negative infinity).
+
 .. index:: address, balance, send, call, callcode, delegatecall, transfer
 
 .. _address:
@@ -123,6 +129,8 @@ In a similar way, the function ``delegatecall`` can be used: The difference is t
 
 All three functions ``call``, ``delegatecall`` and ``callcode`` are very low-level functions and should only be used as a *last resort* as they break the type-safety of Solidity.
 
+The ``.gas()`` option is available on all three methods, while the ``.value()`` option is not supported for ``delegatecall``.
+
 .. note::
     All contracts inherit the members of address, so it is possible to query the balance of the
     current contract using ``this.balance``.
@@ -232,7 +240,7 @@ a non-rational number).
     Integer literals and rational number literals belong to number literal types.
     Moreover, all number literal expressions (i.e. the expressions that
     contain only number literals and operators) belong to number literal
-    types.  So the number literal expressions `1 + 2` and `2 + 1` both
+    types.  So the number literal expressions ``1 + 2`` and ``2 + 1`` both
     belong to the same number literal type for the rational number three.
 
 .. note::
@@ -261,7 +269,7 @@ a non-rational number).
 String Literals
 ---------------
 
-String literals are written with either double or single-quotes (``"foo"`` or ``'bar'``).  They do not imply trailing zeroes as in C; `"foo"`` represents three bytes not four.  As with integer literals, their type can vary, but they are implicitly convertible to ``bytes1``, ..., ``bytes32``, if they fit, to ``bytes`` and to ``string``.
+String literals are written with either double or single-quotes (``"foo"`` or ``'bar'``).  They do not imply trailing zeroes as in C; ``"foo"`` represents three bytes not four.  As with integer literals, their type can vary, but they are implicitly convertible to ``bytes1``, ..., ``bytes32``, if they fit, to ``bytes`` and to ``string``.
 
 String literals support escape characters, such as ``\n``, ``\xNN`` and ``\uNNNN``. ``\xNN`` takes a hex value and inserts the appropriate byte, while ``\uNNNN`` takes a Unicode codepoint and inserts an UTF-8 sequence.
 
@@ -412,7 +420,7 @@ Example that shows how to use internal function types::
 
 Another example that uses external function types::
 
-    pragma solidity ^0.4.5;
+    pragma solidity ^0.4.11;
 
     contract Oracle {
       struct Request {
@@ -437,7 +445,7 @@ Another example that uses external function types::
         oracle.query("USD", this.oracleResponse);
       }
       function oracleResponse(bytes response) {
-        if (msg.sender != address(oracle)) throw;
+        require(msg.sender == address(oracle));
         // Use the data
       }
     }
@@ -714,7 +722,7 @@ shown in the following example:
 
 ::
 
-    pragma solidity ^0.4.0;
+    pragma solidity ^0.4.11;
 
     contract CrowdFunding {
         // Defines a new type with two fields.
@@ -755,8 +763,7 @@ shown in the following example:
                 return false;
             uint amount = c.amount;
             c.amount = 0;
-            if (!c.beneficiary.send(amount))
-                throw;
+            c.beneficiary.transfer(amount);
             return true;
         }
     }
diff --git a/docs/units-and-global-variables.rst b/docs/units-and-global-variables.rst
index 49fe5d84..246cc564 100644
--- a/docs/units-and-global-variables.rst
+++ b/docs/units-and-global-variables.rst
@@ -22,8 +22,8 @@ unit and units are considered naively in the following way:
  * ``1 minutes == 60 seconds``
  * ``1 hours == 60 minutes``
  * ``1 days == 24 hours``
- * ``1 weeks = 7 days``
- * ``1 years = 365 days``
+ * ``1 weeks == 7 days``
+ * ``1 years == 365 days``
 
 Take care if you perform calendar calculations using these units, because
 not every year equals 365 days and not even every day has 24 hours
@@ -93,13 +93,14 @@ Mathematical and Cryptographic Functions
 ``keccak256(...) returns (bytes32)``:
     compute the Ethereum-SHA-3 (Keccak-256) hash of the (tightly packed) arguments
 ``sha3(...) returns (bytes32)``:
-    alias to `keccak256()`
+    alias to ``keccak256()``
 ``sha256(...) returns (bytes32)``:
     compute the SHA-256 hash of the (tightly packed) arguments
 ``ripemd160(...) returns (bytes20)``:
     compute RIPEMD-160 hash of the (tightly packed) arguments
 ``ecrecover(bytes32 hash, uint8 v, bytes32 r, bytes32 s) returns (address)``:
     recover the address associated with the public key from elliptic curve signature or return zero on error
+    (`example usage <https://ethereum.stackexchange.com/q/1777/222>`_)
 ``revert()``:
     abort execution and revert state changes
 
@@ -128,17 +129,23 @@ Address Related
 
 ``<address>.balance`` (``uint256``):
     balance of the :ref:`address` in Wei
-``<address>.send(uint256 amount) returns (bool)``:
-    send given amount of Wei to :ref:`address`, returns ``false`` on failure
 ``<address>.transfer(uint256 amount)``:
     send given amount of Wei to :ref:`address`, throws on failure
+``<address>.send(uint256 amount) returns (bool)``:
+    send given amount of Wei to :ref:`address`, returns ``false`` on failure
+``<address>.call(...) returns (bool)``:
+    issue low-level ``CALL``, returns ``false`` on failure
+``<address>.callcode(...) returns (bool)``:
+    issue low-level ``CALLCODE``, returns ``false`` on failure
+``<address>.delegatecall(...) returns (bool)``:
+    issue low-level ``DELEGATECALL``, returns ``false`` on failure
 
 For more information, see the section on :ref:`address`.
 
 .. warning::
     There are some dangers in using ``send``: The transfer fails if the call stack depth is at 1024
     (this can always be forced by the caller) and it also fails if the recipient runs out of gas. So in order
-    to make safe Ether transfers, always check the return value of ``send`` or even better:
+    to make safe Ether transfers, always check the return value of ``send``, use ``transfer`` or even better:
     Use a pattern where the recipient withdraws the money.
 
 .. index:: this, selfdestruct
diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst
index 08f18132..7aa997f8 100644
--- a/docs/using-the-compiler.rst
+++ b/docs/using-the-compiler.rst
@@ -29,21 +29,21 @@ files reside, so things like ``import "/etc/passwd";`` only work if you add ``=/
 
 If there are multiple matches due to remappings, the one with the longest common prefix is selected.
 
+For security reasons the compiler has restrictions what directories it can access. Paths (and their subdirectories) of source files specified on the commandline and paths defined by remappings are allowed for import statements, but everything else is rejected. Additional paths (and their subdirectories) can be allowed via the ``--allow-paths /sample/path,/another/sample/path`` switch.
+
 If your contracts use :ref:`libraries <libraries>`, you will notice that the bytecode contains substrings of the form ``__LibraryName______``. You can use ``solc`` as a linker meaning that it will insert the library addresses for you at those points:
 
 Either add ``--libraries "Math:0x12345678901234567890 Heap:0xabcdef0123456"`` to your command to provide an address for each library or store the string in a file (one library per line) and run ``solc`` using ``--libraries fileName``.
 
 If ``solc`` is called with the option ``--link``, all input files are interpreted to be unlinked binaries (hex-encoded) in the ``__LibraryName____``-format given above and are linked in-place (if the input is read from stdin, it is written to stdout). All options except ``--libraries`` are ignored (including ``-o``) in this case.
 
+If ``solc`` is called with the option ``--standard-json``, it will expect a JSON input (as explained below) on the standard input, and return a JSON output on the standard output.
+
 .. _compiler-api:
 
 Compiler Input and Output JSON Description
 ******************************************
 
-.. warning::
-
-    This JSON interface is not yet supported by the Solidity compiler, but will be released in a future version.
-
 These JSON formats are used by the compiler API as well as are available through ``solc``. These are subject to change,
 some fields are optional (as noted), but it is aimed at to only make backwards compatible changes.
 
@@ -119,22 +119,27 @@ Input Description
         //
         // The available output types are as follows:
         //   abi - ABI
-        //   ast - AST of all source files
-        //   why3 - Why3 translated output
+        //   ast - AST of all source files (not supported atm)
+        //   legacyAST - legacy AST of all source files
         //   devdoc - Developer documentation (natspec)
         //   userdoc - User documentation (natspec)
         //   metadata - Metadata
-        //   evm.ir - New assembly format before desugaring
+        //   ir - New assembly format before desugaring
         //   evm.assembly - New assembly format after desugaring
-        //   evm.legacyAssemblyJSON - Old-style assembly format in JSON
-        //   evm.opcodes - Opcodes list
+        //   evm.legacyAssembly - Old-style assembly format in JSON
+        //   evm.bytecode.object - Bytecode object
+        //   evm.bytecode.opcodes - Opcodes list
+        //   evm.bytecode.sourceMap - Source mapping (useful for debugging)
+        //   evm.bytecode.linkReferences - Link references (if unlinked object)
+        //   evm.deployedBytecode* - Deployed bytecode (has the same options as evm.bytecode)
         //   evm.methodIdentifiers - The list of function hashes
         //   evm.gasEstimates - Function gas estimates
-        //   evm.bytecode - Bytecode
-        //   evm.deployedBytecode - Deployed bytecode
-        //   evm.sourceMap - Source mapping (useful for debugging)
         //   ewasm.wast - eWASM S-expressions format (not supported atm)
         //   ewasm.wasm - eWASM binary format (not supported atm)
+        //
+        // Note that using a using `evm`, `evm.bytecode`, `ewasm`, etc. will select every
+        // target part of that output.
+        //
         outputSelection: {
           // Enable the metadata and bytecode outputs of every single contract.
           "*": {
@@ -148,9 +153,9 @@ Input Description
           "*": {
             "*": [ "evm.sourceMap" ]
           },
-          // Enable the AST and Why3 output of every single file.
+          // Enable the legacy AST output of every single file.
           "*": {
-            "": [ "ast", "why3" ]
+            "": [ "legacyAST" ]
           }
         }
       }
@@ -174,12 +179,14 @@ Output Description
           ],
           // Mandatory: Error type, such as "TypeError", "InternalCompilerError", "Exception", etc
           type: "TypeError",
-          // Mandatory: Component where the error originated, such as "general", "why3", "ewasm", etc.
+          // Mandatory: Component where the error originated, such as "general", "ewasm", etc.
           component: "general",
           // Mandatory ("error" or "warning")
           severity: "error",
           // Mandatory
           message: "Invalid keyword"
+          // Optional: the message formatted with source location
+          formattedMessage: "sourceFile.sol:100: Invalid keyword"
         }
       ],
       // This contains the file-level outputs. In can be limited/filtered by the outputSelection settings.
@@ -188,7 +195,9 @@ Output Description
           // Identifier (used in source maps)
           id: 1,
           // The AST object
-          ast: {}
+          ast: {},
+          // The legacy AST object
+          legacyAST: {}
         }
       },
       // This contains the contract-level outputs. It can be limited/filtered by the outputSelection settings.
@@ -199,17 +208,26 @@ Output Description
             // The Ethereum Contract ABI. If empty, it is represented as an empty array.
             // See https://github.com/ethereum/wiki/wiki/Ethereum-Contract-ABI
             abi: [],
+            // See the Metadata Output documentation (serialised JSON string)
+            metadata: "{...}",
+            // User documentation (natspec)
+            userdoc: {},
+            // Developer documentation (natspec)
+            devdoc: {},
+            // Intermediate representation (string)
+            ir: "",
+            // EVM-related outputs
             evm: {
-              // Intermediate representation (string)
-              ir: "",
               // Assembly (string)
               assembly: "",
-              // Old-style assembly (string)
-              legacyAssemblyJSON: [],
+              // Old-style assembly (object)
+              legacyAssembly: {},
               // Bytecode and related details.
               bytecode: {
                 // The bytecode as a hex string.
                 object: "00fe",
+                // Opcodes list (string)
+                opcodes: "",
                 // The source mapping as a string. See the source mapping definition.
                 sourceMap: "",
                 // If given, this is an unlinked object.
@@ -222,45 +240,36 @@ Output Description
                     ]
                   }
                 }
-              }
+              },
               // The same layout as above.
               deployedBytecode: { },
-              // Opcodes list (string)
-              opcodes: "",
               // The list of function hashes
               methodIdentifiers: {
-                "5c19a95c": "delegate(address)",
+                "delegate(address)": "5c19a95c"
               },
               // Function gas estimates
               gasEstimates: {
                 creation: {
-                  dataCost: 420000,
-                  // -1 means infinite (aka. unknown)
-                  executionCost: -1
+                  codeDepositCost: "420000",
+                  executionCost: "infinite",
+                  totalCost: "infinite"
                 },
                 external: {
-                  "delegate(address)": 25000
+                  "delegate(address)": "25000"
                 },
                 internal: {
-                  "heavyLifting()": -1
+                  "heavyLifting()": "infinite"
                 }
               }
             },
-            // See the Metadata Output documentation
-            metadata: {},
+            // eWASM related outputs
             ewasm: {
               // S-expressions format
               wast: "",
               // Binary format (hex string)
               wasm: ""
-            },
-            // User documentation (natspec)
-            userdoc: {},
-            // Developer documentation (natspec)
-            devdoc: {}
+            }
           }
         }
-      },
-      // Why3 output (string)
-      why3: ""
+      }
     }