diff --git a/Changelog.md b/Changelog.md index 4776af413..809808ef4 100644 --- a/Changelog.md +++ b/Changelog.md @@ -12,6 +12,7 @@ Compiler Features: * SMTChecker: Show contract name in counterexample function call. * SMTChecker: Support try/catch statements. * SMTChecker: Output internal and trusted external function calls in a counterexample's transaction trace. + * SMTChecker: Synthesize untrusted functions called externally. Bugfixes: * Code Generator: Fix length check when decoding malformed error data in catch clause. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 32898c9cd..18ca57e87 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -676,6 +676,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall || function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View; + if (!usesStaticCall) { state().newState(); @@ -683,13 +684,23 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) m_context.variable(*var)->increaseIndex(); } - auto postCallState = vector{state().state()} + currentStateVariables(); auto error = errorFlag().increaseIndex(); + + Predicate const& callPredicate = *createSymbolicBlock( + nondetInterfaceSort(*m_currentContract, state()), + "nondet_call_" + uniquePrefix(), + PredicateType::ExternalCallUntrusted, + &_funCall + ); + auto postCallState = vector{state().state()} + currentStateVariables(); vector stateExprs{error, state().thisAddress(), state().abi(), state().crypto()}; + auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState); - // TODO this could instead add the summary of the called function, where that summary - // basically has the nondet interface of this summary as a constraint. - m_context.addAssertion(nondet); + auto nondetCall = callPredicate(stateExprs + preCallState + postCallState); + + addRule(smtutil::Expression::implies(nondet, nondetCall), nondetCall.name); + + m_context.addAssertion(nondetCall); solAssert(m_errorDest, ""); connectBlocks(m_currentBlock, predicate(*m_errorDest), errorFlag().currentValue() > 0); // To capture the possibility of a reentrant call, we record in the call graph that the current function @@ -1179,7 +1190,8 @@ smtutil::Expression CHC::predicate(Predicate const& _block) return constructor(_block, m_context); case PredicateType::FunctionSummary: case PredicateType::InternalCall: - case PredicateType::ExternalCall: + case PredicateType::ExternalCallTrusted: + case PredicateType::ExternalCallUntrusted: return smt::function(_block, m_currentContract, m_context); case PredicateType::FunctionBlock: solAssert(m_currentFunction, ""); @@ -1256,7 +1268,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) Predicate const& callPredicate = *createSummaryBlock( *function, *calledContract, - kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCall + kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCallTrusted ); auto to = smt::function(callPredicate, calledContract, m_context); addRule(smtutil::Expression::implies(from, to), to.name); @@ -1561,19 +1573,30 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& string txCex = summaryPredicate->formatSummaryCall(summaryArgs); list calls; - auto dfs = [&](unsigned node, unsigned depth, auto&& _dfs) -> void { + auto dfs = [&](unsigned parent, unsigned node, unsigned depth, auto&& _dfs) -> void { auto pred = nodePred(node); + auto parentPred = nodePred(parent); solAssert(pred && pred->isSummary(), ""); + solAssert(parentPred && parentPred->isSummary(), ""); + auto callTraceSize = calls.size(); if (!pred->isConstructorSummary()) for (unsigned v: callGraph[node]) - _dfs(v, depth + 1, _dfs); - calls.push_front(string(depth * 2, ' ') + pred->formatSummaryCall(nodeArgs(node))); + _dfs(node, v, depth + 1, _dfs); + calls.push_front(string(depth * 4, ' ') + pred->formatSummaryCall(nodeArgs(node))); if (pred->isInternalCall()) calls.front() += " -- internal call"; - else if (pred->isExternalCall()) - calls.front() += " -- external call"; + else if (pred->isExternalCallTrusted()) + calls.front() += " -- trusted external call"; + else if (pred->isExternalCallUntrusted()) + { + calls.front() += " -- untrusted external call"; + if (calls.size() > callTraceSize + 1) + calls.front() += ", synthesized as:"; + } + else if (pred->isFunctionSummary() && parentPred->isExternalCallUntrusted()) + calls.front() += " -- reentrant call"; }; - dfs(summaryId, 0, dfs); + dfs(summaryId, summaryId, 0, dfs); path.emplace_back(boost::algorithm::join(calls, "\n")); } @@ -1596,7 +1619,14 @@ map> CHC::summaryCalls(CHCSolverInterface::CexGraph c q.pop(); Predicate const* nodePred = Predicate::predicate(_graph.nodes.at(node).name); - if (nodePred->isSummary() && (_root == root || nodePred->isInternalCall() || nodePred->isExternalCall())) + Predicate const* rootPred = Predicate::predicate(_graph.nodes.at(root).name); + if (nodePred->isSummary() && ( + _root == root || + nodePred->isInternalCall() || + nodePred->isExternalCallTrusted() || + nodePred->isExternalCallUntrusted() || + rootPred->isExternalCallUntrusted() + )) { calls[root].push_back(node); root = node; diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index 730f27b34..aa7abd91e 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -121,6 +121,11 @@ FunctionDefinition const* Predicate::programFunction() const return nullptr; } +FunctionCall const* Predicate::programFunctionCall() const +{ + return dynamic_cast(m_node); +} + optional> Predicate::stateVariables() const { if (auto const* fun = programFunction()) @@ -141,7 +146,11 @@ optional> Predicate::stateVariables() const bool Predicate::isSummary() const { - return m_type == PredicateType::ConstructorSummary || m_type == PredicateType::FunctionSummary || m_type == PredicateType::InternalCall || m_type == PredicateType::ExternalCall; + return isFunctionSummary() || + isInternalCall() || + isExternalCallTrusted() || + isExternalCallUntrusted() || + isConstructorSummary(); } bool Predicate::isFunctionSummary() const @@ -154,9 +163,14 @@ bool Predicate::isInternalCall() const return m_type == PredicateType::InternalCall; } -bool Predicate::isExternalCall() const +bool Predicate::isExternalCallTrusted() const { - return m_type == PredicateType::ExternalCall; + return m_type == PredicateType::ExternalCallTrusted; +} + +bool Predicate::isExternalCallUntrusted() const +{ + return m_type == PredicateType::ExternalCallUntrusted; } bool Predicate::isConstructorSummary() const @@ -171,10 +185,13 @@ bool Predicate::isInterface() const string Predicate::formatSummaryCall(vector const& _args) const { + solAssert(isSummary(), ""); + if (auto contract = programContract()) return contract->name() + ".constructor()"; - solAssert(isSummary(), ""); + if (auto funCall = programFunctionCall()) + return funCall->location().text(); auto stateVars = stateVariables(); solAssert(stateVars.has_value(), ""); diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h index 366cac846..e091ec963 100644 --- a/libsolidity/formal/Predicate.h +++ b/libsolidity/formal/Predicate.h @@ -38,7 +38,8 @@ enum class PredicateType FunctionSummary, FunctionBlock, InternalCall, - ExternalCall, + ExternalCallTrusted, + ExternalCallUntrusted, Error, Custom }; @@ -94,6 +95,10 @@ public: /// or nullptr otherwise. FunctionDefinition const* programFunction() const; + /// @returns the FunctionCall that this predicate represents + /// or nullptr otherwise. + FunctionCall const* programFunctionCall() const; + /// @returns the program state variables in the scope of this predicate. std::optional> stateVariables() const; @@ -106,8 +111,11 @@ public: /// @returns true if this predicate represents an internal function call. bool isInternalCall() const; - /// @returns true if this predicate represents an external function call. - bool isExternalCall() const; + /// @returns true if this predicate represents a trusted external function call. + bool isExternalCallTrusted() const; + + /// @returns true if this predicate represents an untrusted external function call. + bool isExternalCallUntrusted() const; /// @returns true if this predicate represents a constructor summary. bool isConstructorSummary() const; diff --git a/test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol b/test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol index e88f95050..618aaff99 100644 --- a/test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol +++ b/test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol @@ -15,4 +15,4 @@ contract C { } } // ---- -// Warning 6328: (184-213): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[], [], []]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()\n C.s() -- internal call +// Warning 6328: (184-213): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[], [], []]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()\n C.s() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol index 68432d3c9..4bf0bbe8b 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_1.sol @@ -21,4 +21,4 @@ contract C { } } // ---- -// Warning 6328: (359-373): CHC: Assertion violation happens here.\nCounterexample:\nx = 7\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call +// Warning 6328: (359-373): CHC: Assertion violation happens here.\nCounterexample:\nx = 7\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol index 512c1d6dc..bf8173cbc 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_2.sol @@ -21,4 +21,4 @@ contract C { } } // ---- -// Warning 6328: (365-379): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call +// Warning 6328: (365-379): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol index 38b17e1ee..a7774f53b 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_3.sol @@ -21,4 +21,4 @@ contract C { } } // ---- -// Warning 6328: (358-372): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call +// Warning 6328: (358-372): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol index 862383521..c12ccaa2b 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_inside_modifiers_4.sol @@ -21,4 +21,4 @@ contract C { } } // ---- -// Warning 6328: (365-379): CHC: Assertion violation happens here.\nCounterexample:\nx = 7\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call +// Warning 6328: (365-379): CHC: Assertion violation happens here.\nCounterexample:\nx = 7\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol index a52d16585..8aa3c3a46 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol @@ -43,6 +43,6 @@ contract C { } } // ---- -// Warning 6328: (288-302): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.test()\n C.reset_if_overflow() -- internal call -// Warning 6328: (535-552): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(1)\nState: x = 1\nC.test()\n C.reset_if_overflow() -- internal call -// Warning 6328: (648-662): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(10)\nState: x = 10\nC.test()\n C.reset_if_overflow() -- internal call +// Warning 6328: (288-302): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.test()\n C.reset_if_overflow() -- internal call +// Warning 6328: (535-552): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(1)\nState: x = 1\nC.test()\n C.reset_if_overflow() -- internal call +// Warning 6328: (648-662): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(10)\nState: x = 10\nC.test()\n C.reset_if_overflow() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/nested_if.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/nested_if.sol index f52fd03b2..df6fc1ba7 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/nested_if.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/nested_if.sol @@ -22,5 +22,5 @@ contract C { } } // ---- -// Warning 6328: (147-174): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nb = 2\n\nTransaction trace:\nC.constructor()\nC.test(0, 2)\n C.nested_if(0, 2) -- internal call\n C.nested_if(0, 2) -- internal call +// Warning 6328: (147-174): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nb = 2\n\nTransaction trace:\nC.constructor()\nC.test(0, 2)\n C.nested_if(0, 2) -- internal call\n C.nested_if(0, 2) -- internal call // Warning 6838: (332-348): BMC: Condition is always false. diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if2.sol index 42ae6c9b2..1156b3fdf 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if2.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if2.sol @@ -14,4 +14,4 @@ contract C { } } // ---- -// Warning 6328: (89-114): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\n\nTransaction trace:\nC.constructor()\nC.test(0)\n C.simple_if(0) -- internal call +// Warning 6328: (89-114): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\n\nTransaction trace:\nC.constructor()\nC.test(0)\n C.simple_if(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_array.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_array.sol index caeaa30b4..4f50c49b7 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_array.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_array.sol @@ -25,4 +25,4 @@ contract C { } } // ---- -// Warning 6328: (205-222): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0]\nC.check()\n C.conditional_store() -- internal call +// Warning 6328: (205-222): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0]\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0]\nC.check()\n C.conditional_store() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_state_var.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_state_var.sol index c63eb5d2d..e01ef1bcd 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_state_var.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_state_var.sol @@ -19,4 +19,4 @@ contract C { } } // ---- -// Warning 6328: (132-146): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.check()\n C.conditional_increment() -- internal call +// Warning 6328: (132-146): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.check()\n C.conditional_increment() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_struct.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_struct.sol index 910bcab20..e7385eb05 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_struct.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_struct.sol @@ -22,4 +22,4 @@ contract C { } } // ---- -// Warning 6328: (156-172): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 0}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0}\nC.check()\n C.conditional_increment() -- internal call +// Warning 6328: (156-172): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 0}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0}\nC.check()\n C.conditional_increment() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_struct_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_struct_2.sol index 56fb8aa17..e07f9a731 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_struct_2.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_struct_2.sol @@ -22,4 +22,4 @@ contract C { } } // ---- -// Warning 6328: (156-172): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 0}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0}\nC.check()\n C.conditional_increment() -- internal call +// Warning 6328: (156-172): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 0}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0}\nC.check()\n C.conditional_increment() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_tuple.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_tuple.sol index ba053223c..f88a90bfb 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_tuple.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_tuple.sol @@ -23,5 +23,5 @@ contract C { } } // ---- -// Warning 6328: (160-174): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, y = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.check()\n C.conditional_increment() -- internal call -// Warning 6328: (194-208): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, y = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.check()\n C.conditional_increment() -- internal call +// Warning 6328: (160-174): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, y = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.check()\n C.conditional_increment() -- internal call +// Warning 6328: (194-208): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, y = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.check()\n C.conditional_increment() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/require.sol b/test/libsolidity/smtCheckerTests/control_flow/require.sol index 414483b1d..ecbbdb283 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/require.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/require.sol @@ -31,4 +31,4 @@ contract C { } // ---- // Warning 6321: (429-442): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 6328: (448-465): CHC: Assertion violation happens here.\nCounterexample:\nx = true\n\nTransaction trace:\nC.constructor()\nState: x = false\nC.i()\n C.m() -- internal call +// Warning 6328: (448-465): CHC: Assertion violation happens here.\nCounterexample:\nx = true\n\nTransaction trace:\nC.constructor()\nState: x = false\nC.i()\n C.m() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/revert.sol b/test/libsolidity/smtCheckerTests/control_flow/revert.sol index 7c82285a4..f47259025 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/revert.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/revert.sol @@ -33,4 +33,4 @@ contract C { // Warning 5740: (116-129): Unreachable code. // Warning 5740: (221-234): Unreachable code. // Warning 6321: (408-421): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 6328: (427-444): CHC: Assertion violation happens here.\nCounterexample:\nx = true\n\nTransaction trace:\nC.constructor()\nState: x = false\nC.i()\n C.m() -- internal call +// Warning 6328: (427-444): CHC: Assertion violation happens here.\nCounterexample:\nx = true\n\nTransaction trace:\nC.constructor()\nState: x = false\nC.i()\n C.m() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol index 372de56e9..5e8910a6e 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol @@ -15,4 +15,4 @@ contract c { } } // ---- -// Warning 6328: (227-236): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call +// Warning 6328: (227-236): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol index 13bd6407d..5acc7d5cd 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_inside_branch.sol @@ -17,5 +17,5 @@ contract c { } } // ---- -// Warning 6328: (202-218): CHC: Assertion violation happens here.\nCounterexample:\nx = 101\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call -// Warning 6328: (242-252): CHC: Assertion violation happens here.\nCounterexample:\nx = 101\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call +// Warning 6328: (202-218): CHC: Assertion violation happens here.\nCounterexample:\nx = 101\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call +// Warning 6328: (242-252): CHC: Assertion violation happens here.\nCounterexample:\nx = 101\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol index b1e5ddba4..079bdc945 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol @@ -15,4 +15,4 @@ contract c { } } // ---- -// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call +// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol index 98a90ddcb..0126551f0 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol @@ -15,4 +15,4 @@ contract c { } } // ---- -// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call +// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol index a5f78b5fc..471b35a1e 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_inside_branch.sol @@ -24,4 +24,4 @@ contract c { } } // ---- -// Warning 6328: (360-370): CHC: Assertion violation happens here.\nCounterexample:\nx = 102\na = false\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g(false)\n c.f() -- internal call\n c.f() -- internal call +// Warning 6328: (360-370): CHC: Assertion violation happens here.\nCounterexample:\nx = 102\na = false\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g(false)\n c.f() -- internal call\n c.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol index bc424d224..b6572a31a 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol @@ -15,4 +15,4 @@ contract c { } } // ---- -// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call +// Warning 6328: (225-235): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol index 20d015d58..a55d2d80c 100644 --- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol +++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol @@ -11,4 +11,4 @@ contract C { } } // ---- -// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(data)\n C.fi(data, 2437) -- internal call +// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(data)\n C.fi(data, 2437) -- internal call diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol index 8b68414e2..862dec605 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol @@ -34,4 +34,4 @@ contract C { } } // ---- -// Warning 6328: (528-565): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 1, y = 0, z = 0, s = 0\nC.f() +// Warning 6328: (528-565): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 1, y = 0, z = 0, s = 0\nC.f()\n s.f() -- untrusted external call\n s.f() -- untrusted external call, synthesized as:\n C.inv() -- reentrant call diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol index 8c15ca1f4..ae5ce0ba1 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol @@ -29,4 +29,4 @@ contract C { } } // ---- -// Warning 6328: (299-313): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, s = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 0, y = 0, s = 0\nC.f() +// Warning 6328: (299-313): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, s = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 0, y = 0, s = 0\nC.f()\n s.f() -- untrusted external call diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol index 3eefd469a..3023632b6 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol @@ -16,4 +16,4 @@ contract C { } } // ---- -// Warning 6328: (239-253): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0) +// Warning 6328: (239-253): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0)\n D(target).e() -- untrusted external call, synthesized as:\n C.broken() -- reentrant call diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol index d847c8513..a67f15ce0 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol @@ -13,4 +13,4 @@ contract C { } } // ---- -// Warning 6328: (150-164): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0) +// Warning 6328: (150-164): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0)\n D(target).e() -- untrusted external call, synthesized as:\n C.call(0) -- reentrant call diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol index c19bc5217..dd570f854 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol @@ -28,4 +28,4 @@ contract C is A { } // ---- // Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f() -// Warning 6328: (385-399): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nd = 0\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.call(0) +// Warning 6328: (385-399): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nd = 0\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.call(0)\n d.d() -- untrusted external call, synthesized as:\n C.f() -- reentrant call diff --git a/test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol b/test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol index 0c0b119a3..fa1ecde0c 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol @@ -27,4 +27,4 @@ contract C { } } // ---- -// Warning 6328: (307-321): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, d = 0, lock = false\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0, lock = false\nC.f() +// Warning 6328: (307-321): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, d = 0, lock = false\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0, lock = false\nC.f()\n d.d() -- untrusted external call, synthesized as:\n C.set(1) -- reentrant call diff --git a/test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol b/test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol index c41dd27e2..3eb56bf72 100644 --- a/test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol +++ b/test/libsolidity/smtCheckerTests/function_selector/function_types_sig.sol @@ -25,7 +25,7 @@ contract C { } // ---- // Warning 7650: (284-296): Assertion checker does not yet support this expression. -// Warning 6328: (470-495): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.check()\n C.f() -- internal call\n C.g() -- internal call -// Warning 6328: (540-565): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.check()\n C.f() -- internal call\n C.g() -- internal call\n C.i() -- internal call\n C.i() -- internal call +// Warning 6328: (470-495): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.check()\n C.f() -- internal call\n C.g() -- internal call +// Warning 6328: (540-565): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.check()\n C.f() -- internal call\n C.g() -- internal call\n C.i() -- internal call\n C.i() -- internal call // Warning 7650: (284-296): Assertion checker does not yet support this expression. // Warning 7650: (284-296): Assertion checker does not yet support this expression. diff --git a/test/libsolidity/smtCheckerTests/function_selector/homer.sol b/test/libsolidity/smtCheckerTests/function_selector/homer.sol index f34b4b39a..1ad2ebd53 100644 --- a/test/libsolidity/smtCheckerTests/function_selector/homer.sol +++ b/test/libsolidity/smtCheckerTests/function_selector/homer.sol @@ -43,4 +43,4 @@ contract Homer is ERC165, Simpson { // ---- -// Warning 6328: (1373-1428): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nHomer.constructor()\nHomer.check()\n Homer.supportsInterface(1941353618) -- internal call\n Homer.supportsInterface(33540519) -- internal call\n Homer.supportsInterface(2342435274) -- internal call +// Warning 6328: (1373-1428): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nHomer.constructor()\nHomer.check()\n Homer.supportsInterface(1941353618) -- internal call\n Homer.supportsInterface(33540519) -- internal call\n Homer.supportsInterface(2342435274) -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var.sol b/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var.sol index e21451a6a..915259b3d 100644 --- a/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var.sol +++ b/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var.sol @@ -16,4 +16,4 @@ contract C } } // ---- -// Warning 6328: (209-223): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nb = true\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g(true)\n C.f() -- internal call +// Warning 6328: (209-223): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nb = true\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g(true)\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_3.sol b/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_3.sol index 72143619a..d1ada0fd0 100644 --- a/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/function_inside_branch_modify_state_var_3.sol @@ -24,5 +24,5 @@ contract C } // ---- -// Warning 6328: (209-223): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nb = true\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g(true)\n C.f() -- internal call -// Warning 6328: (321-335): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nb = false\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.h(false)\n C.f() -- internal call +// Warning 6328: (209-223): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nb = true\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g(true)\n C.f() -- internal call +// Warning 6328: (321-335): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nb = false\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.h(false)\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol index 99061f439..f8e32e6d8 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_bound_1_fail.sol @@ -18,4 +18,4 @@ contract C } } // ---- -// Warning 6328: (261-277): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(1)\n L.add(1, 999) -- internal call +// Warning 6328: (261-277): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(1)\n L.add(1, 999) -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol index 7265cb19f..f0c353b7e 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol @@ -16,4 +16,4 @@ contract D } } // ---- -// Warning 6328: (191-206): CHC: Assertion violation happens here.\nCounterexample:\nc = 0\n_y = 0\n\nTransaction trace:\nD.constructor()\nState: c = 0\nD.g(0) +// Warning 6328: (191-206): CHC: Assertion violation happens here.\nCounterexample:\nc = 0\n_y = 0\n\nTransaction trace:\nD.constructor()\nState: c = 0\nD.g(0)\n c.f(_y) -- untrusted external call diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol index 367c6b9ee..b5abe65fe 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol @@ -12,4 +12,4 @@ contract C } // ---- -// Warning 6328: (161-174): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h(0) -- internal call +// Warning 6328: (161-174): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol index f9ad2a3a0..8f405a748 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol @@ -16,4 +16,4 @@ contract C } // ---- -// Warning 6328: (229-242): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h(0) -- internal call\n C.k(0) -- internal call +// Warning 6328: (229-242): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h(0) -- internal call\n C.k(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol index 283e018ac..49da35b7b 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol @@ -12,4 +12,4 @@ contract C } // ---- -// Warning 6328: (163-176): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h(0) -- internal call +// Warning 6328: (163-176): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol index e317c652b..d2e887342 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol @@ -17,4 +17,4 @@ contract C } } // ---- -// Warning 6328: (245-261): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(1)\n L.add(1, 999) -- internal call +// Warning 6328: (245-261): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(1)\n L.add(1, 999) -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol index 6d2c62d2c..5d46fef23 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol @@ -13,4 +13,4 @@ contract C } // ---- -// Warning 6328: (144-157): CHC: Assertion violation happens here.\nCounterexample:\na = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0\nC.g()\n C.f(0) -- internal call +// Warning 6328: (144-157): CHC: Assertion violation happens here.\nCounterexample:\na = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0\nC.g()\n C.f(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol index 8fc94bfce..84acebabb 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol @@ -14,4 +14,4 @@ contract C } // ---- -// Warning 6328: (152-165): CHC: Assertion violation happens here.\nCounterexample:\na = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0\nC.g()\n C.f(1) -- internal call\n C.f(0) -- internal call +// Warning 6328: (152-165): CHC: Assertion violation happens here.\nCounterexample:\na = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0\nC.g()\n C.f(1) -- internal call\n C.f(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_inheritance.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_inheritance.sol index c10c96e50..96d7ecfbf 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_call_inheritance.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_call_inheritance.sol @@ -17,4 +17,4 @@ contract A is B { } } // ---- -// Warning 6328: (254-268): CHC: Assertion violation happens here.\nCounterexample:\nx = 42\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.a()\n B.b() -- internal call\n C.c() -- internal call +// Warning 6328: (254-268): CHC: Assertion violation happens here.\nCounterexample:\nx = 42\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.a()\n B.b() -- internal call\n C.c() -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol index 729b77226..e5ac5b180 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol @@ -22,7 +22,7 @@ contract C{ // ---- // Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning. // Warning 6328: (138-152): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f() -// Warning 6328: (170-184): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call -// Warning 6328: (220-234): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call -// Warning 6328: (245-259): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call +// Warning 6328: (170-184): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call +// Warning 6328: (220-234): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call +// Warning 6328: (245-259): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call // Warning 6328: (82-96): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0) diff --git a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol index 2a26caa5d..400f68cc2 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol @@ -22,5 +22,5 @@ contract C{ // ---- // Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning. // Warning 6328: (138-152): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f() -// Warning 6328: (184-198): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call\n C.g() -- internal call +// Warning 6328: (184-198): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor(0)\nState: x = 1\nC.f()\n C.g() -- internal call\n C.g() -- internal call // Warning 6328: (82-96): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor(0) diff --git a/test/libsolidity/smtCheckerTests/functions/library_constant.sol b/test/libsolidity/smtCheckerTests/functions/library_constant.sol index 276b8d870..ecf6939ec 100644 --- a/test/libsolidity/smtCheckerTests/functions/library_constant.sol +++ b/test/libsolidity/smtCheckerTests/functions/library_constant.sol @@ -20,4 +20,4 @@ contract C { } // ---- // Warning 6328: (136-155): CHC: Assertion violation happens here.\nCounterexample:\nTON = 1000\n\nTransaction trace:\nl1.constructor()\nState: TON = 1000\nl1.f1() -// Warning 4984: (229-234): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\nTransaction trace:\nC.constructor()\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129639935)\n l1.f2(115792089237316195423570985008687907853269984665640564039457584007913129639935, 1) -- internal call +// Warning 4984: (229-234): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\nTransaction trace:\nC.constructor()\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129639935)\n l1.f2(115792089237316195423570985008687907853269984665640564039457584007913129639935, 1) -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol b/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol index f7efcd046..f33106deb 100644 --- a/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol +++ b/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol @@ -28,5 +28,5 @@ contract D is C { } } // ---- -// Warning 6328: (237-251): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.proxy()\n C.f() -- internal call\n A.f() -- internal call -// Warning 6328: (360-374): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nD.constructor()\nState: x = 0\nA.proxy()\n D.f() -- internal call\n C.f() -- internal call\n A.f() -- internal call +// Warning 6328: (237-251): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.proxy()\n C.f() -- internal call\n A.f() -- internal call +// Warning 6328: (360-374): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nD.constructor()\nState: x = 0\nA.proxy()\n D.f() -- internal call\n C.f() -- internal call\n A.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_call_2.sol b/test/libsolidity/smtCheckerTests/functions/this_external_call_2.sol index ccb500572..34d56c66e 100644 --- a/test/libsolidity/smtCheckerTests/functions/this_external_call_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/this_external_call_2.sol @@ -13,4 +13,4 @@ contract C { } } // ---- -// Warning 6328: (141-156): CHC: Assertion violation happens here.\nCounterexample:\na = 42\nx = 42\n\nTransaction trace:\nC.constructor()\nState: a = 0\nC.f(42)\n C.g(42) -- external call +// Warning 6328: (141-156): CHC: Assertion violation happens here.\nCounterexample:\na = 42\nx = 42\n\nTransaction trace:\nC.constructor()\nState: a = 0\nC.f(42)\n C.g(42) -- trusted external call diff --git a/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol b/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol index f1823c01d..14ea90cc2 100644 --- a/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol +++ b/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol @@ -18,4 +18,4 @@ contract C is A { } } // ---- -// Warning 6328: (259-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.proxy()\n C.f() -- internal call +// Warning 6328: (259-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.proxy()\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/imports/import_base.sol b/test/libsolidity/smtCheckerTests/imports/import_base.sol index 6a7151e2d..c3932fe71 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_base.sol +++ b/test/libsolidity/smtCheckerTests/imports/import_base.sol @@ -17,9 +17,11 @@ contract Der is Base { assert(y > x); } } +// ==== +// SMTIgnoreCex: yes // ---- // Warning 4984: (der:101-109): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. -// Warning 6328: (der:113-126): CHC: Assertion violation happens here.\nCounterexample:\nx = 3, a = 7\ny = 0\n\nTransaction trace:\nDer.constructor()\nState: x = 0, a = 0\nDer.g(0)\n Base.f() -- internal call +// Warning 6328: (der:113-126): CHC: Assertion violation happens here. // Warning 4984: (base:100-103): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 2661: (base:100-103): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 2661: (der:101-109): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/imports/import_library.sol b/test/libsolidity/smtCheckerTests/imports/import_library.sol index 0d177e1e5..ddbc5b244 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_library.sol +++ b/test/libsolidity/smtCheckerTests/imports/import_library.sol @@ -15,4 +15,4 @@ library L { } } // ---- -// Warning 6328: (c:113-126): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n L.f() -- internal call +// Warning 6328: (c:113-126): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n L.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol index 1740b66aa..3eab6a343 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol @@ -20,4 +20,4 @@ contract C { } } // ---- -// Warning 6328: (287-300): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, owner = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, owner = 0\nC.g(1)\n C.f() -- internal call +// Warning 6328: (287-300): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, owner = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, owner = 0\nC.g(1)\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol index 8bee0d496..e4ee540d8 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi_functions.sol @@ -22,4 +22,4 @@ contract C } } // ---- -// Warning 6328: (311-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(1)\n C.g(1, 0) -- internal call +// Warning 6328: (311-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(1)\n C.g(1, 0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol index a4f564cbf..c8f1113b2 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol @@ -24,4 +24,4 @@ contract C { } // ---- // Warning 2072: (282-288): Unused local variable. -// Warning 6328: (304-328): CHC: Assertion violation happens here.\nCounterexample:\na = false, x = 3, d = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = false, x = 0, d = 0\nC.g()\n C.g() -- internal call +// Warning 6328: (304-328): CHC: Assertion violation happens here.\nCounterexample:\na = false, x = 3, d = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = false, x = 0, d = 0\nC.g()\n d.d() -- untrusted external call, synthesized as:\n C.f() -- reentrant call\n C.g() -- internal call\n d.d() -- untrusted external call, synthesized as:\n C.h() -- reentrant call diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_1.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_1.sol index 60659fcdc..e37f001ad 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_1.sol @@ -10,4 +10,4 @@ contract C { } } // ---- -// Warning 6328: (203-216): CHC: Assertion violation happens here.\nCounterexample:\n\na = 6\n\nTransaction trace:\nC.constructor()\nC.g(6)\n C.f(6) -- internal call +// Warning 6328: (203-216): CHC: Assertion violation happens here.\nCounterexample:\n\na = 6\n\nTransaction trace:\nC.constructor()\nC.g(6)\n C.f(6) -- internal call diff --git a/test/libsolidity/smtCheckerTests/operators/function_call_named_arguments.sol b/test/libsolidity/smtCheckerTests/operators/function_call_named_arguments.sol index b77180d35..a223845e7 100644 --- a/test/libsolidity/smtCheckerTests/operators/function_call_named_arguments.sol +++ b/test/libsolidity/smtCheckerTests/operators/function_call_named_arguments.sol @@ -29,4 +29,4 @@ contract C { } } // ---- -// Warning 6328: (507-521): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.call()\n L.l(2, 3) -- internal call\n L.l(3, 3) -- internal call\n C.f(1, 2, true) -- internal call\n C.f(1, 2, false) -- internal call +// Warning 6328: (507-521): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.call()\n L.l(2, 3) -- internal call\n L.l(3, 3) -- internal call\n C.f(1, 2, true) -- internal call\n C.f(1, 2, false) -- internal call diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_mul_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_mul_overflow.sol index 2b97419a8..df7dc7e5f 100644 --- a/test/libsolidity/smtCheckerTests/overflow/signed_mul_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/signed_mul_overflow.sol @@ -5,6 +5,8 @@ contract C { return x * y; } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 3944: (110-115): CHC: Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here.\nCounterexample:\n\nx = (- 3)\ny = 19298681539552699237261830834781317975544997444273427339909597334652188273323\n = 0\n\nTransaction trace:\nC.constructor()\nC.f((- 3), 19298681539552699237261830834781317975544997444273427339909597334652188273323) -// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = (- 1)\ny = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f((- 1), (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)) +// Warning 3944: (110-115): CHC: Underflow (resulting value less than -57896044618658097711785492504343953926634992332820282019728792003956564819968) happens here. +// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/special/event.sol b/test/libsolidity/smtCheckerTests/special/event.sol index 9f5a27a5a..824baa751 100644 --- a/test/libsolidity/smtCheckerTests/special/event.sol +++ b/test/libsolidity/smtCheckerTests/special/event.sol @@ -27,4 +27,4 @@ contract C { // ---- // Warning 6321: (280-284): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. // Warning 6321: (430-434): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. -// Warning 6328: (440-449): CHC: Assertion violation happens here.\nCounterexample:\nx = false\n\nTransaction trace:\nC.constructor()\nState: x = true\nC.h()\n C.h_data() -- internal call\n C.h_data() -- internal call +// Warning 6328: (440-449): CHC: Assertion violation happens here.\nCounterexample:\nx = false\n\nTransaction trace:\nC.constructor()\nState: x = true\nC.h()\n C.h_data() -- internal call\n C.h_data() -- internal call diff --git a/test/libsolidity/smtCheckerTests/special/msg_sig.sol b/test/libsolidity/smtCheckerTests/special/msg_sig.sol index 69f06fb0d..67ca2eee4 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_sig.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_sig.sol @@ -26,5 +26,5 @@ contract C } // ---- // Warning 6328: (76-105): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6328: (403-432): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n C.fi() -- internal call\n C.gi() -- internal call +// Warning 6328: (403-432): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n C.fi() -- internal call\n C.gi() -- internal call // Warning 6328: (543-572): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_3.sol b/test/libsolidity/smtCheckerTests/try_catch/try_3.sol index 70c516a71..d21deaed2 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_3.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_3.sol @@ -22,4 +22,4 @@ contract C { } // ---- // Warning 5667: (291-305): Unused try/catch parameter. Remove or comment out the variable name to silence this warning. -// Warning 6328: (312-326): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.postinc() -- internal call +// Warning 6328: (312-326): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.postinc() -- internal call diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol index 1435070f6..c5ee0e83c 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol @@ -22,6 +22,6 @@ contract C { } // ---- // Warning 2519: (197-203): This declaration shadows an existing declaration. -// Warning 6328: (218-232): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f() -// Warning 6328: (306-316): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f() +// Warning 6328: (218-232): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()\n d.d() -- untrusted external call +// Warning 6328: (306-316): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()\n d.d() -- untrusted external call // Warning 6328: (426-440): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol b/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol index 940be6f68..5d03a0454 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol @@ -14,4 +14,4 @@ contract C { } } // ---- -// Warning 6328: (278-338): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n C.g() -- external call +// Warning 6328: (278-338): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n C.g() -- trusted external call diff --git a/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol b/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol index 9570d910e..b0eeb56ae 100644 --- a/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol +++ b/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol @@ -15,8 +15,8 @@ contract C { // Warning 6031: (214-218): Internal error: Expression undefined for SMT solver. // Warning 6031: (222-226): Internal error: Expression undefined for SMT solver. // Warning 7229: (238-244): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons -// Warning 6328: (207-227): CHC: Assertion violation happens here.\nCounterexample:\na = 0, b = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0, b = 0\nC.g()\n C.f(0, 0) -- internal call -// Warning 6328: (231-245): CHC: Assertion violation happens here.\nCounterexample:\na = 0, b = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0, b = 0\nC.g()\n C.f(0, 0) -- internal call +// Warning 6328: (207-227): CHC: Assertion violation happens here.\nCounterexample:\na = 0, b = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0, b = 0\nC.g()\n C.f(0, 0) -- internal call +// Warning 6328: (231-245): CHC: Assertion violation happens here.\nCounterexample:\na = 0, b = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0, b = 0\nC.g()\n C.f(0, 0) -- internal call // Warning 5729: (214-218): BMC does not yet implement this type of function call. // Warning 5729: (222-226): BMC does not yet implement this type of function call. // Warning 7229: (238-244): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons diff --git a/test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol b/test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol index 7acf90f65..25865fd33 100644 --- a/test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol +++ b/test/libsolidity/smtCheckerTests/typecast/implicit_cast_string_literal_byte.sol @@ -13,4 +13,4 @@ contract C { function g(bytes1 b) internal pure {} } // ---- -// Warning 6328: (186-207): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n C.g(0) -- internal call +// Warning 6328: (186-207): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n C.g(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_return.sol b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_return.sol index 5242bb225..d5c684645 100644 --- a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_return.sol +++ b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_return.sol @@ -9,4 +9,4 @@ contract C { } } // ---- -// Warning 6328: (238-259): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.a()\n C.f1() -- internal call\n C.g() -- internal call\n C.f1() -- internal call\n C.g() -- internal call +// Warning 6328: (238-259): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.a()\n C.f1() -- internal call\n C.g() -- internal call\n C.f1() -- internal call\n C.g() -- internal call diff --git a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_return_multi.sol b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_return_multi.sol index 7fa97398d..e7b5c702e 100644 --- a/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_return_multi.sol +++ b/test/libsolidity/smtCheckerTests/typecast/string_literal_to_fixed_bytes_return_multi.sol @@ -12,4 +12,4 @@ contract C { } } // ---- -// Warning 6328: (442-461): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.a()\n C.f2() -- internal call\n C.h() -- internal call +// Warning 6328: (442-461): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.a()\n C.f2() -- internal call\n C.h() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol index 27c4ae415..54d2a7d6b 100644 --- a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol +++ b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol @@ -17,6 +17,7 @@ contract C } // ==== // EVMVersion: >spuriousDragon +// SMTIgnoreCex: yes // ---- // Warning 2072: (224-240): Unused local variable. -// Warning 6328: (266-281): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\ndata = [7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 14, 7, 7, 7, 19, 7, 7, 7, 7, 7, 7, 7, 27, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7]\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0, [7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 14, 7, 7, 7, 19, 7, 7, 7, 7, 7, 7, 7, 27, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7]) +// Warning 6328: (266-281): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol index c9c67454c..43e98884c 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol +++ b/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol @@ -13,7 +13,9 @@ contract C assert(a.balance > b.balance); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (295-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 100\na = 39\nb = 38\n\nTransaction trace:\nC.constructor()\nC.f(100, 39, 38) +// Warning 6328: (295-324): CHC: Assertion violation happens here. // Warning 1236: (217-232): BMC: Insufficient funds happens here. // Warning 1236: (236-251): BMC: Insufficient funds happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_2.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_2.sol index 4797bf87e..61afe48c9 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_2.sol @@ -20,4 +20,4 @@ contract C } } // ---- -// Warning 6328: (436-453): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.g(0, 0, c)\n C.f([], [], c) -- internal call +// Warning 6328: (436-453): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.g(0, 0, c)\n C.f([], [], c) -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol index 1f51ad667..477715f89 100644 --- a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol @@ -24,4 +24,4 @@ contract C } } // ---- -// Warning 6328: (421-452): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\nTransaction trace:\nC.constructor()\nC.g(38)\n C.f(map) -- internal call +// Warning 6328: (421-452): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\nTransaction trace:\nC.constructor()\nC.g(38)\n C.f(map) -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol index 8bf130b90..7183f73dd 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol @@ -24,4 +24,4 @@ contract C } } // ---- -// Warning 6328: (425-456): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\nTransaction trace:\nC.constructor()\nC.g(38)\n C.f(map) -- internal call +// Warning 6328: (425-456): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\nTransaction trace:\nC.constructor()\nC.g(38)\n C.f(map) -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_2.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_2.sol index 8fa944c8d..0388174ee 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_2.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_2.sol @@ -12,4 +12,4 @@ contract C } } // ---- -// Warning 6328: (116-130): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0)\n C.g() -- internal call +// Warning 6328: (116-130): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0)\n C.g() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol index 74cb607d9..49f0d6b40 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol @@ -12,4 +12,4 @@ contract c { } } // ---- -// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21239\n\nTransaction trace:\nc.constructor()\nc.g(38, 21239)\n c.f(map, 38, 21239) -- internal call +// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21239\n\nTransaction trace:\nc.constructor()\nc.g(38, 21239)\n c.f(map, 38, 21239) -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_4.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_4.sol index b5ac53820..766e73c8a 100644 --- a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_4.sol +++ b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_4.sol @@ -15,4 +15,4 @@ contract C { } } // ---- -// Warning 6328: (261-276): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568)\n C.g() -- internal call +// Warning 6328: (261-276): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568)\n C.g() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_5.sol b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_5.sol index e61cb7e0b..39f7a4758 100644 --- a/test/libsolidity/smtCheckerTests/types/string_literal_assignment_5.sol +++ b/test/libsolidity/smtCheckerTests/types/string_literal_assignment_5.sol @@ -13,4 +13,4 @@ contract C { } } // ---- -// Warning 6328: (251-266): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568)\n C.g() -- internal call +// Warning 6328: (251-266): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293568\n\nTransaction trace:\nC.constructor()\nC.f(52647538817385212172903286807934654968315727694643370704309751478220717293568)\n C.g() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_return.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_return.sol index 925ff0187..294841062 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_return.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_return.sol @@ -17,4 +17,4 @@ contract C { } } // ---- -// Warning 6328: (265-286): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n C.s() -- internal call +// Warning 6328: (265-286): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n C.s() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol index e6eda42cc..643df8657 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol @@ -14,5 +14,7 @@ contract C { assert(s1.x == s2.x); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (225-245): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 2, a: []}\ns2 = {x: 3, a: [5, 5, 5, 5, 5, 5]}\n\nTransaction trace:\nC.constructor()\nC.f({x: 0, a: []}, {x: 3, a: [5, 5, 5, 5, 5, 5]}) +// Warning 6328: (225-245): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_empty.sol b/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_empty.sol index 3fa3211ee..2954f1e13 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_empty.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_declarations_function_empty.sol @@ -14,4 +14,4 @@ contract C } } // ---- -// Warning 6328: (224-234): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call +// Warning 6328: (224-234): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/tuple_function.sol b/test/libsolidity/smtCheckerTests/types/tuple_function.sol index 9243f2fef..3b03eb313 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_function.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_function.sol @@ -14,5 +14,5 @@ contract C } } // ---- -// Warning 6328: (182-196): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call -// Warning 6328: (200-214): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call +// Warning 6328: (182-196): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call +// Warning 6328: (200-214): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol b/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol index 62ee604fe..3c6f57014 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol @@ -14,4 +14,4 @@ contract C } } // ---- -// Warning 6328: (199-213): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call +// Warning 6328: (199-213): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol b/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol index 4e50b3aee..620fbed94 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol @@ -16,5 +16,5 @@ contract C } } // ---- -// Warning 6328: (205-219): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call -// Warning 6328: (223-237): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call +// Warning 6328: (205-219): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call +// Warning 6328: (223-237): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/unchecked/check_var_init.sol b/test/libsolidity/smtCheckerTests/unchecked/check_var_init.sol index 77e972b87..3ecfa49fc 100644 --- a/test/libsolidity/smtCheckerTests/unchecked/check_var_init.sol +++ b/test/libsolidity/smtCheckerTests/unchecked/check_var_init.sol @@ -17,4 +17,4 @@ contract D { } // ---- // Warning 3944: (66-80): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor() -// Warning 3944: (193-207): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n D.h() -- internal call +// Warning 3944: (193-207): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n D.h() -- internal call diff --git a/test/libsolidity/smtCheckerTests/unchecked/unchecked_called_by_checked.sol b/test/libsolidity/smtCheckerTests/unchecked/unchecked_called_by_checked.sol index ea708f035..bdc6aa1e6 100644 --- a/test/libsolidity/smtCheckerTests/unchecked/unchecked_called_by_checked.sol +++ b/test/libsolidity/smtCheckerTests/unchecked/unchecked_called_by_checked.sol @@ -12,4 +12,4 @@ contract C { } } // ---- -// Warning 4984: (273-294): CHC: Overflow (resulting value larger than 65535) happens here.\nCounterexample:\n\na = 65024\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(65024)\n C.add(65024, 256) -- internal call +// Warning 4984: (273-294): CHC: Overflow (resulting value larger than 65535) happens here.\nCounterexample:\n\na = 65024\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(65024)\n C.add(65024, 256) -- internal call