cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #10662 from blishko/smt-external-error

Browse Source 
[SMTChecker] Carry error information across external calls
This commit is contained in:
Leonardo 2020-12-29 11:05:21 +01:00 committed by GitHub
commit 840b194bea
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
32 changed files with 202 additions and 79 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -10,6 +10,7 @@ Compiler Features:
Bugfixes:
* Code Generator: Fix length check when decoding malformed error data in catch clause.
* SMTChecker: Fix false negatives in overriding modifiers.
* SMTChecker: Fix false negatives when analyzing external function calls.
### 0.8.0 (2020-12-16)

20
libsolidity/formal/CHC.cpp
View File

@ -642,10 +642,20 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
}
auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + postCallState);
auto error = errorFlag().increaseIndex();
vector<smtutil::Expression> 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);
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
// can call any of the external methods of the current contract.
solAssert(m_currentContract && m_currentFunction, "");
for (auto const* definedFunction: contractFunctions(*m_currentContract))
if (!definedFunction->isConstructor() && definedFunction->isPublic())
m_callGraph[m_currentFunction].insert(definedFunction);
m_context.addAssertion(errorFlag().currentValue() == 0);
}
@ -889,7 +899,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
/// 0 steps to be taken, used as base for the inductive
/// rule for each function.
auto const& iface = *m_nondetInterfaces.at(contract);
addRule(smt::nondetInterface(iface, *contract, m_context, 0, 0), "base_nondet");
addRule(smtutil::Expression::implies(errorFlag().currentValue() == 0, smt::nondetInterface(iface, *contract, m_context, 0, 0)), "base_nondet");
for (auto const* function: contractFunctions(*contract))
{
@ -907,10 +917,12 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
auto state1 = stateVariablesAtIndex(1, *contract);
auto state2 = stateVariablesAtIndex(2, *contract);
auto errorPre = errorFlag().currentValue();
auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
auto errorPost = errorFlag().increaseIndex();
auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)};
vector<smtutil::Expression> args{errorPost, state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)};
args += state1 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
vector<smtutil::Expression>{state().state(2)} +
@ -918,7 +930,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) +
applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); });
connectBlocks(nondetPre, nondetPost, (*m_summaries.at(contract).at(function))(args));
connectBlocks(nondetPre, nondetPost, errorPre == 0 && (*m_summaries.at(contract).at(function))(args));
}
}
}

12
libsolidity/formal/PredicateInstance.cpp
View File

@ -36,14 +36,22 @@ smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition cons
smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
{
auto& state = _context.state();
auto const& state = _context.state();
vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state()};
return _pred(stateExprs + currentStateVariables(_contract, _context));
}
smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx)
smtutil::Expression nondetInterface(
Predicate const& _pred,
ContractDefinition const& _contract,
EncodingContext& _context,
unsigned _preIdx,
unsigned _postIdx)
{
auto const& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(), state.abi(), state.crypto()};
return _pred(
stateExprs +
vector<smtutil::Expression>{_context.state().state(_preIdx)} +
stateVariablesAtIndex(_preIdx, _contract, _context) +
vector<smtutil::Expression>{_context.state().state(_postIdx)} +

6
libsolidity/formal/PredicateSort.cpp
View File

@ -41,7 +41,11 @@ SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicSta
auto varSorts = stateSorts(_contract);
vector<SortPointer> stateSort{_state.stateSort()};
return make_shared<FunctionSort>(
stateSort + varSorts + stateSort + varSorts,
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} +
stateSort +
varSorts +
stateSort +
varSorts,
SortProvider::boolSort
);
}

2
libsolidity/formal/PredicateSort.h
View File

@ -37,7 +37,7 @@ namespace solidity::frontend::smt
*
* 2. Nondet interface
* The nondeterminism behavior of a contract. Signature:
* nondet_interface(blockchainState, stateVariables, blockchainState', stateVariables').
* nondet_interface(error, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
*
* 3. Constructor entry/summary
* The summary of a contract's deployment procedure.

1
libsolidity/formal/SymbolicState.h
View File

@ -88,6 +88,7 @@ public:
/// Error flag.
//@{
SymbolicIntVariable& errorFlag() { return m_error; }
SymbolicIntVariable const& errorFlag() const { return m_error; }
smtutil::SortPointer const& errorFlagSort() const { return m_error.sort(); }
//@}

20
test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice.sol
View File

@ -11,21 +11,17 @@ contract C {
// should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately
//assert(b1.length == b3.length); // fails for now
bytes memory b4 = abi.encode(data[5:10]);
assert(b1.length == b4.length); // should fail
// Disabled because of Spacer nondeterminism
//bytes memory b4 = abi.encode(data[5:10]);
//assert(b1.length == b4.length); // should fail
uint x = 5;
uint y = 10;
bytes memory b5 = abi.encode(data[x:y]);
// Disabled because of Spacer nondeterminism in Z3 4.8.9
//uint x = 5;
//uint y = 10;
//bytes memory b5 = abi.encode(data[x:y]);
// should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately
assert(b1.length == b5.length); // fails for now
//assert(b1.length == b5.length); // fails for now
}
}
// ----
// Warning 6328: (311-341): CHC: Assertion violation happens here.
// Warning 1218: (694-724): CHC: Error trying to invoke SMT solver.
// Warning 6328: (694-724): CHC: Assertion violation might happen here.
// Warning 1218: (945-975): CHC: Error trying to invoke SMT solver.
// Warning 6328: (945-975): CHC: Assertion violation might happen here.
// Warning 4661: (694-724): BMC: Assertion violation happens here.
// Warning 4661: (945-975): BMC: Assertion violation happens here.

22
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol
View File

@ -12,13 +12,15 @@ contract C {
//assert(b1.length == b3.length); // fails for now
bytes memory b4 = abi.encodePacked(data[5:10]);
assert(b1.length == b4.length); // should fail
// Disabled because of Spacer nondeterminism
//assert(b1.length == b4.length); // should fail
uint x = 5;
uint y = 10;
bytes memory b5 = abi.encodePacked(data[x:y]);
// Disabled because of Spacer nondeterminism
//uint x = 5;
//uint y = 10;
//bytes memory b5 = abi.encodePacked(data[x:y]);
// should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately
assert(b1.length == b5.length); // fails for now
//assert(b1.length == b5.length); // fails for now
bytes memory b6 = abi.encode(data[5:10]);
assert(b4.length == b6.length); // should fail
@ -26,12 +28,4 @@ contract C {
}
// ----
// Warning 6328: (330-360): CHC: Assertion violation happens here.
// Warning 1218: (725-755): CHC: Error trying to invoke SMT solver.
// Warning 6328: (725-755): CHC: Assertion violation might happen here.
// Warning 1218: (982-1012): CHC: Error trying to invoke SMT solver.
// Warning 6328: (982-1012): CHC: Assertion violation might happen here.
// Warning 1218: (1078-1108): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1078-1108): CHC: Assertion violation might happen here.
// Warning 4661: (725-755): BMC: Assertion violation happens here.
// Warning 4661: (982-1012): BMC: Assertion violation happens here.
// Warning 4661: (1078-1108): BMC: Assertion violation happens here.
// Warning 6328: (1182-1212): CHC: Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol
View File

@ -16,8 +16,9 @@ contract C {
assert(b1.length != b5.length); // should fail
assert(b1.length == b5.length); // should fail
bytes memory b6 = abi.encode(x, z, a);
assert(b1.length == b6.length); // should fail
// Commented out because of nondeterminism in Spacer in Z3 4.8.9
//bytes memory b6 = abi.encode(x, z, a);
//assert(b1.length == b6.length); // should fail
}
}
// ----
@ -28,7 +29,6 @@ contract C {
// Warning 6328: (560-590): CHC: Assertion violation might happen here.
// Warning 1218: (609-639): CHC: Error trying to invoke SMT solver.
// Warning 6328: (609-639): CHC: Assertion violation might happen here.
// Warning 6328: (700-730): CHC: Assertion violation happens here.
// Warning 4661: (451-481): BMC: Assertion violation happens here.
// Warning 4661: (560-590): BMC: Assertion violation happens here.
// Warning 4661: (609-639): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/abi/abi_encode_simple.sol
View File

@ -14,7 +14,8 @@ contract C {
bytes memory b5 = abi.encode(y, y, y, y, a, a, a);
assert(b1.length != b5.length); // should fail
assert(b1.length == b5.length); // should fail
// Disabled because of nondeterminism in Spacer Z3 4.8.9
//assert(b1.length == b5.length); // should fail
}
}
// ----
@ -24,7 +25,6 @@ contract C {
// Warning 6328: (421-451): CHC: Assertion violation might happen here.
// Warning 1218: (524-554): CHC: Error trying to invoke SMT solver.
// Warning 6328: (524-554): CHC: Assertion violation might happen here.
// Warning 6328: (573-603): CHC: Assertion violation happens here.
// Warning 4661: (330-360): BMC: Assertion violation happens here.
// Warning 4661: (421-451): BMC: Assertion violation happens here.
// Warning 4661: (524-554): BMC: Assertion violation happens here.

23
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol
View File

@ -6,8 +6,9 @@ contract C {
bytes memory b2 = abi.encodeWithSignature(sig, y, z, a);
assert(b1.length == b2.length);
bytes memory b3 = abi.encodeWithSignature(sig, y, z, b);
assert(b1.length == b3.length); // should fail
// Disabled because of nondeterminism in Spacer Z3 4.8.9
//bytes memory b3 = abi.encodeWithSignature(sig, y, z, b);
//assert(b1.length == b3.length); // should fail
bytes memory b4 = abi.encodeWithSignature(sig, t, z, a);
assert(b1.length == b4.length); // should fail
@ -21,14 +22,10 @@ contract C {
}
}
// ----
// Warning 6328: (403-433): CHC: Assertion violation happens here.
// Warning 6328: (512-542): CHC: Assertion violation happens here.
// Warning 1218: (633-663): CHC: Error trying to invoke SMT solver.
// Warning 6328: (633-663): CHC: Assertion violation might happen here.
// Warning 1218: (682-712): CHC: Error trying to invoke SMT solver.
// Warning 6328: (682-712): CHC: Assertion violation might happen here.
// Warning 1218: (793-823): CHC: Error trying to invoke SMT solver.
// Warning 6328: (793-823): CHC: Assertion violation might happen here.
// Warning 4661: (633-663): BMC: Assertion violation happens here.
// Warning 4661: (682-712): BMC: Assertion violation happens here.
// Warning 4661: (793-823): BMC: Assertion violation happens here.
// Warning 5667: (139-154): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (575-605): CHC: Assertion violation happens here.
// Warning 6328: (696-726): CHC: Assertion violation happens here.
// Warning 6328: (745-775): CHC: Assertion violation happens here.
// Warning 1218: (856-886): CHC: Error trying to invoke SMT solver.
// Warning 6328: (856-886): CHC: Assertion violation might happen here.
// Warning 4661: (856-886): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol
View File

@ -10,4 +10,4 @@ contract C {
}
}
// ----
// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 21238\n\n\nTransaction trace:\nconstructor()\nf(21238)
// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 2437\n\n\nTransaction trace:\nconstructor()\nf(2437)

2
test/libsolidity/smtCheckerTests/external_calls/external.sol
View File

@ -17,4 +17,4 @@ contract C {
}
}
// ----
// Warning 6328: (200-214): CHC: Assertion violation happens here.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\nf()\nState: x = 1, d = 0\nf()\nState: x = 2, d = 0\ng()
// Warning 6328: (200-214): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol
View File

@ -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\n\n\nTransaction trace:\nconstructor()\nState: owner = 1, y = 0, z = 0, s = 0\ninv()
// Warning 6328: (528-565): CHC: Assertion violation happens here.\nCounterexample:\nowner = (- 1), y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = (- 1), y = 0, z = 0, s = 0\nf()

1
test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
View File

@ -21,5 +21,6 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 4984: (146-149): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (146-149): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (189-203): CHC: Assertion violation happens here.
// Warning 2661: (146-149): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

19
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol Normal file
View File

@ -0,0 +1,19 @@
pragma experimental SMTChecker;
interface D { function e() external; }
contract C {
bool locked = true;
function call(address target) public {
locked = false;
D(target).e();
locked = true;
}
function broken() public view {
assert(locked);
}
}
// ----
// Warning 6328: (239-253): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\n\nTransaction trace:\nconstructor()\nState: locked = true\ncall(0)

16
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol Normal file
View File

@ -0,0 +1,16 @@
pragma experimental SMTChecker;
interface D { function e() external; }
contract C {
bool locked = true;
function call(address target) public {
assert(locked);
locked = false;
D(target).e();
locked = true;
}
}
// ----
// Warning 6328: (150-164): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\n\nTransaction trace:\nconstructor()\nState: locked = true\ncall(0)

31
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol Normal file
View File

@ -0,0 +1,31 @@
pragma experimental SMTChecker;
abstract contract D {
function d() virtual public {}
}
contract A {
int x = 0;
function f() virtual public view {
assert(x == 0); // should hold
assert(x == 1); // should fail
}
}
contract C is A {
constructor() {
x = 1;
}
function call(D d) public {
d.d();
}
function f() public view override {
assert(x == 1); // should hold
assert(x == 0); // should fail
}
}
// ----
// Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf()
// Warning 6328: (385-399): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nd = 0\n\n\nTransaction trace:\nconstructor()\nState: x = 1\ncall(0)

33
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol Normal file
View File

@ -0,0 +1,33 @@
pragma experimental SMTChecker;
abstract contract D {
function d() virtual public;
}
contract C {
bytes data;
bytes32 kec;
constructor(bytes memory _data) {
data = _data;
kec = keccak256(data);
}
function check(bytes memory _data) public view {
bytes32 _kec = keccak256(data);
assert(_kec == kec); // should hold
assert(kec == keccak256(_data)); // should fail
}
function ext(D d) public {
d.d();
}
}
// ----
// Warning 1218: (335-366): CHC: Error trying to invoke SMT solver.
// Warning 6328: (335-366): CHC: Assertion violation might happen here.
// Warning 1218: (335-366): CHC: Error trying to invoke SMT solver.
// Warning 6328: (335-366): CHC: Assertion violation might happen here.
// Warning 4661: (335-366): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol
View File

@ -15,4 +15,4 @@ contract C is B {
}
}
// ----
// Warning 6328: (165-179): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(11)
// Warning 6328: (165-179): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 9\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(9)

6
test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
View File

@ -12,6 +12,8 @@ contract C {
assert(y == x);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (162-176): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 1\n\n\nTransaction trace:\nconstructor(0, 0)\nState: x = 0\nf(1)
// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 5\na = 115792089237316195423570985008687907853269984665640564039457584007913129639935\nb = 1\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935, 1)
// Warning 6328: (162-176): CHC: Assertion violation happens here.
// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

12
test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
View File

@ -12,10 +12,16 @@ contract C
require(map[0] == map[1]);
assert(map[0] == map[1]);
d.g(y);
// Storage knowledge is cleared after an external call.
assert(map[0] == map[1]);
assert(map[0] == 0); // should fail
}
function set(uint x) public {
map[0] = x;
map[1] = x;
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (297-321): CHC: Assertion violation might happen here.
// Warning 4661: (297-321): BMC: Assertion violation happens here.
// Warning 6328: (267-286): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol
View File

@ -18,5 +18,7 @@ contract C {
assert(y == 1); // should fail
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (307-321): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (307-321): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol
View File

@ -17,4 +17,4 @@ contract C {
}
}
// ----
// Warning 6328: (293-307): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (293-307): CHC: Assertion violation happens here.

14
test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
View File

@ -4,17 +4,13 @@ contract C
{
function f(uint x) public pure {
require(x < 100);
for(uint i = 0; i < 10; ++i) {
// Overflows due to resetting x.
for(uint i = 0; i < 5; ++i) {
x = x + 1;
}
// Assertion is safe but current solver version cannot solve it.
// Keep test for next solver release.
assert(x > 0);
// Disabled because of non-determinism in Spacer in Z3 4.8.9, check with next solver release.
//assert(x > 0);
}
}
// ----
// Warning 4984: (176-181): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (296-309): CHC: Assertion violation might happen here.
// Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (296-309): BMC: Assertion violation happens here.
// Warning 4984: (139-144): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 2661: (139-144): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

2
test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal.sol
View File

@ -13,5 +13,7 @@ contract C {
assert(y[0] == (bytes1("d") | bytes1("e")) ^ bytes1("f"));
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (189-208): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol
View File

@ -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\n\n\nTransaction trace:\nconstructor()\nState: a = false, x = 0, d = 0\nf()
// Warning 6328: (304-328): CHC: Assertion violation happens here.\nCounterexample:\na = false, x = 3, d = 0\n\n = 0\n\nTransaction trace:\nconstructor()\nState: a = false, x = 0, d = 0\ng()

2
test/libsolidity/smtCheckerTests/types/address_transfer_2.sol
View File

@ -14,6 +14,6 @@ contract C
}
}
// ----
// Warning 6328: (295-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 100\na = 7719\nb = 7720\n\n\nTransaction trace:\nconstructor()\nf(100, 7719, 7720)
// Warning 6328: (295-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 100\na = 7720\nb = 7719\n\n\nTransaction trace:\nconstructor()\nf(100, 7720, 7719)
// Warning 1236: (217-232): BMC: Insufficient funds happens here.
// Warning 1236: (236-251): BMC: Insufficient funds happens here.

2
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol
View File

@ -26,5 +26,7 @@ contract C
assert(b[0] == 1);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (572-589): CHC: Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/types/array_branch_1d.sol
View File

@ -2,7 +2,8 @@ pragma experimental SMTChecker;
contract C
{
function f(bool b, uint[] memory c) public {
function f(bool b, uint[] memory c) public pure {
require(c.length >= 1 && c.length <= 2);
c[0] = 0;
if (b)
c[0] = 1;
@ -10,5 +11,4 @@ contract C
}
}
// ----
// Warning 2018: (47-148): Function state mutability can be restricted to pure
// Warning 6328: (128-144): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 18, 14, 14, 21, 14, 14, 23, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14]\n\n\nTransaction trace:\nconstructor()\nf(false, [7719, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 18, 14, 14, 21, 14, 14, 23, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14])
// Warning 6328: (176-192): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 14]\n\n\nTransaction trace:\nconstructor()\nf(false, [38, 14])

2
test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol
View File

@ -24,4 +24,4 @@ contract C
}
}
// ----
// Warning 6328: (421-452): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 8855\n\n\nTransaction trace:\nconstructor()\ng(8855)
// Warning 6328: (421-452): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\n\nTransaction trace:\nconstructor()\ng(38)

2
test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol
View File

@ -24,4 +24,4 @@ contract C
}
}
// ----
// Warning 6328: (425-456): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 8855\n\n\nTransaction trace:\nconstructor()\ng(8855)
// Warning 6328: (425-456): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\n\nTransaction trace:\nconstructor()\ng(38)