cerc-io/solidity
15
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

Remove nondet tests

Browse Source
This commit is contained in:
Leonardo Alt 2020-10-27 17:48:12 +00:00
parent f2f84a7f97
commit 25f75ce547
3 changed files with 14 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
libsolidity/formal/Predicate.cpp
View File

@ -301,9 +301,17 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
solAssert(_expr.name == "tuple_constructor", ""); solAssert(_expr.name == "tuple_constructor", "");
auto const& tupleSort = dynamic_cast<TupleSort const&>(*_expr.sort); auto const& tupleSort = dynamic_cast<TupleSort const&>(*_expr.sort);
solAssert(tupleSort.components.size() == 2, ""); solAssert(tupleSort.components.size() == 2, "");
auto length = stoul(_expr.arguments.at(1).name);
// Limit this counterexample size to 1k.
// Some OSs give you "unlimited" memory through swap and other virtual memory,
// so purely relying on bad_alloc being thrown is not a good idea.
// In that case, the array allocation might cause OOM and the program is killed.
if (length >= 1024)
return {};
try try
{ {
vector<string> array(stoul(_expr.arguments.at(1).name)); vector<string> array(length);
if (!fillArray(_expr.arguments.at(0), array, arrayType)) if (!fillArray(_expr.arguments.at(0), array, arrayType))
return {}; return {};
return "[" + boost::algorithm::join(array, ", ") + "]"; return "[" + boost::algorithm::join(array, ", ") + "]";

6
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
View File

@ -7,9 +7,7 @@ contract C {
function f(bool b) public { function f(bool b) public {
if (b) if (b)
s.x[2] |= 1; s.x[2] |= 1;
assert(s.x[2] != 1); // Removed because of Spacer nondeterminism.
//assert(s.x[2] != 1);
} }
} }
// ----
// Warning 6328: (173-192): CHC: Assertion violation might happen here.
// Warning 7812: (173-192): BMC: Assertion violation might happen here.

5
test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol
View File

@ -17,7 +17,8 @@ contract C
// Should not fail since knowledge is erased only for mapping (uint => uint). // Should not fail since knowledge is erased only for mapping (uint => uint).
assert(severalMaps8[0][0] == 42); assert(severalMaps8[0][0] == 42);
// Should not fail since singleMap == severalMaps3d[0][0] is not possible. // Should not fail since singleMap == severalMaps3d[0][0] is not possible.
assert(severalMaps3d[0][0][0] == 42); // Removed because of Spacer nondeterminism.
//assert(severalMaps3d[0][0][0] == 42);
// Should fail since singleMap == map is possible. // Should fail since singleMap == map is possible.
assert(map[0] == 42); assert(map[0] == 42);
} }
@ -26,4 +27,4 @@ contract C
} }
} }
// ---- // ----
// Warning 6328: (781-801): CHC: Assertion violation happens here. // Warning 6328: (830-850): CHC: Assertion violation happens here.