diff options
| -rw-r--r-- | docs/abi-spec.rst | 2 | ||||
| -rw-r--r-- | docs/control-structures.rst | 1 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 12 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 4 |
4 files changed, 11 insertions, 8 deletions
diff --git a/docs/abi-spec.rst b/docs/abi-spec.rst index e106d98b..b81e35a6 100644 --- a/docs/abi-spec.rst +++ b/docs/abi-spec.rst @@ -288,6 +288,8 @@ In effect, a log entry using this ABI is described as: - ``topics[n]``: ``EVENT_INDEXED_ARGS[n - 1]`` (``EVENT_INDEXED_ARGS`` is the series of ``EVENT_ARGS`` that are indexed); - ``data``: ``abi_serialise(EVENT_NON_INDEXED_ARGS)`` (``EVENT_NON_INDEXED_ARGS`` is the series of ``EVENT_ARGS`` that are not indexed, ``abi_serialise`` is the ABI serialisation function used for returning a series of typed values from a function, as described above). +For all fixed-length Solidity types, the ``EVENT_INDEXED_ARGS`` array contains the 32-byte encoded value directly. However, for *types of dynamic length*, which include ``string``, ``bytes``, and arrays, ``EVENT_INDEXED_ARGS`` will contain the *Keccak hash* of the encoded value, rather than the encoded value directly. This allows applications to efficiently query for values of dynamic-length types (by setting the hash of the encoded value as the topic), but leaves applications unable to decode indexed values they have not queried for. For dynamic-length types, application developers face a trade-off between fast search for predetermined values (if the argument is indexed) and legibility of arbitrary values (which requires that the arguments not be indexed). Developers may overcome this tradeoff and achieve both efficient search and arbitrary legibility by defining events with two arguments — one indexed, one not — intended to hold the same value. + JSON ==== diff --git a/docs/control-structures.rst b/docs/control-structures.rst index 0c5825bc..1a8ee25b 100644 --- a/docs/control-structures.rst +++ b/docs/control-structures.rst @@ -295,6 +295,7 @@ Solidity internally allows tuple types, i.e. a list of objects of potentially di // the rest of the values are discarded. (data.length,) = f(); // Sets the length to 7 // The same can be done on the left side. + // If the tuple begins in an empty component, the beginning values are discarded. (,data[3]) = f(); // Sets data[3] to 2 // Components can only be left out at the left-hand-side of assignments, with // one exception: diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index d4887a3d..a8529795 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -560,7 +560,7 @@ void SMTChecker::checkCondition( } smt::CheckResult result; vector<string> values; - tie(result, values) = checkSatisifableAndGenerateModel(expressionsToEvaluate); + tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate); string conditionalComment; if (m_conditionalExecutionHappened) @@ -607,12 +607,12 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co m_interface->push(); addPathConjoinedExpression(expr(_condition)); - auto positiveResult = checkSatisifable(); + auto positiveResult = checkSatisfiable(); m_interface->pop(); m_interface->push(); addPathConjoinedExpression(!expr(_condition)); - auto negatedResult = checkSatisifable(); + auto negatedResult = checkSatisfiable(); m_interface->pop(); if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR) @@ -642,7 +642,7 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co } pair<smt::CheckResult, vector<string>> -SMTChecker::checkSatisifableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate) +SMTChecker::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate) { smt::CheckResult result; vector<string> values; @@ -672,9 +672,9 @@ SMTChecker::checkSatisifableAndGenerateModel(vector<smt::Expression> const& _exp return make_pair(result, values); } -smt::CheckResult SMTChecker::checkSatisifable() +smt::CheckResult SMTChecker::checkSatisfiable() { - return checkSatisifableAndGenerateModel({}).first; + return checkSatisfiableAndGenerateModel({}).first; } void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function) diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 539221cc..d4c2cf6f 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -100,9 +100,9 @@ private: std::pair<smt::CheckResult, std::vector<std::string>> - checkSatisifableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate); + checkSatisfiableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate); - smt::CheckResult checkSatisifable(); + smt::CheckResult checkSatisfiable(); void initializeLocalVariables(FunctionDefinition const& _function); void resetVariables(std::vector<Declaration const*> _variables); |