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 #10567 from blishko/unary-operators-fix

Browse Source 
[SMTChecker] Fix CHC analysis of increment/decrement
This commit is contained in:
Leonardo 2020-12-11 18:52:12 +01:00 committed by GitHub
commit db9aa36d6c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
40 changed files with 150 additions and 59 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -14,6 +14,7 @@ Compiler Features:
* SMTChecker: Support getters.
* SMTChecker: Support named arguments in function calls.
* SMTChecker: Support struct constructor.
* SMTChecker: Create underflow and overflow verification targets for increment/decrement in the CHC engine.
* Standard-Json: Move the recently introduced ``modelCheckerSettings`` key to ``settings.modelChecker``.
* Standard-Json: Properly filter the requested output artifacts.

17
libsolidity/formal/BMC.cpp
View File

@ -356,27 +356,12 @@ void BMC::endVisit(UnaryOperation const& _op)
)
return;
switch (_op.getOperator())
{
case Token::Inc: // ++ (pre- or postfix)
case Token::Dec: // -- (pre- or postfix)
if (_op.getOperator() == Token::Sub && smt::isInteger(*_op.annotation().type))
addVerificationTarget(
VerificationTarget::Type::UnderOverflow,
expr(_op),
&_op
);
break;
case Token::Sub: // -
if (_op.annotation().type->category() == Type::Category::Integer)
addVerificationTarget(
VerificationTarget::Type::UnderOverflow,
expr(_op),
&_op
);
break;
default:
break;
}
}
void BMC::endVisit(FunctionCall const& _funCall)

16
libsolidity/formal/SMTEncoder.cpp
View File

@ -512,7 +512,13 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
auto decl = identifierToVariable(*identifier);
solAssert(decl, "");
auto innerValue = currentValue(*decl);
auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
auto newValue = arithmeticOperation(
_op.getOperator() == Token::Inc ? Token::Add : Token::Sub,
innerValue,
smtutil::Expression(size_t(1)),
_op.annotation().type,
_op
).first;
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
assignment(*decl, newValue);
}
@ -522,7 +528,13 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
)
{
auto innerValue = expr(*subExpr);
auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
auto newValue = arithmeticOperation(
_op.getOperator() == Token::Inc ? Token::Add : Token::Sub,
innerValue,
smtutil::Expression(size_t(1)),
_op.annotation().type,
_op
).first;
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
indexOrMemberAssignment(*subExpr, newValue);
}

2
test/libsolidity/smtCheckerTests/array_members/pop_loop_safe.sol
View File

@ -9,3 +9,5 @@ contract C {
}
}
}
// ----
// Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

1
test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol
View File

@ -11,4 +11,5 @@ contract C {
}
}
// ----
// Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 2529: (150-157): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\nl = 0\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf(0)

2
test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol
View File

@ -11,3 +11,5 @@ contract C {
assert(x[0] == 42);
}
}
// ----
// Warning 4984: (174-177): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

28
test/libsolidity/smtCheckerTests/bmc_coverage/unary_add_minus_overflow_detected.sol Normal file
View File

@ -0,0 +1,28 @@
pragma experimental SMTChecker;
contract C {
uint8 x;
function inc_pre() public {
++x;
}
function dec_pre() public {
--x;
}
/* Commented out because Spacer segfaults in Z3 4.8.9
function inc_post() public {
x++;
}
function dec_post() public {
x--;
}
*/
}
// ====
// SMTEngine: bmc
// ----
// Warning 2661: (87-90): BMC: Overflow (resulting value larger than 255) happens here.
// Warning 4144: (127-130): BMC: Underflow (resulting value less than 0) happens here.

1
test/libsolidity/smtCheckerTests/control_flow/return_1.sol
View File

@ -19,4 +19,3 @@ contract C {
}
}
// ----
// Warning 2661: (158-161): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

1
test/libsolidity/smtCheckerTests/control_flow/return_1_fail.sol
View File

@ -23,4 +23,3 @@ contract C {
// Warning 6328: (274-300): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (304-330): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (334-362): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 2661: (158-161): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

1
test/libsolidity/smtCheckerTests/control_flow/return_2.sol
View File

@ -28,4 +28,3 @@ contract C {
}
}
// ----
// Warning 2661: (188-191): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

1
test/libsolidity/smtCheckerTests/control_flow/return_2_fail.sol
View File

@ -38,4 +38,3 @@ contract C {
// Warning 6328: (437-458): CHC: Assertion violation happens here.
// Warning 6328: (462-490): CHC: Assertion violation happens here.
// Warning 6328: (494-517): CHC: Assertion violation happens here.
// Warning 2661: (188-191): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

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

@ -18,5 +18,6 @@ contract C {
}
}
// ----
// 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.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\ninc()\nState: x = 1, d = 0\nf()
// Warning 2661: (146-149): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

3
test/libsolidity/smtCheckerTests/external_calls/external_safe.sol
View File

@ -16,3 +16,6 @@ contract C {
assert(x < 11);
}
}
// ----
// Warning 6328: (200-214): CHC: Assertion violation might happen here.
// Warning 4661: (200-214): BMC: Assertion violation happens here.

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

@ -21,5 +21,3 @@ contract C{
}
// ----
// Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 2661: (156-159): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (238-241): BMC: Underflow (resulting value less than 0) happens here.

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

@ -26,5 +26,3 @@ contract C{
// Warning 6328: (220-234): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\n\n\nTransaction trace:\nconstructor(0)\nState: x = 1\nf()
// Warning 6328: (245-259): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nconstructor(0)\nState: x = 1\nf()
// Warning 6328: (82-96): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor(0)
// Warning 2661: (156-159): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (238-241): BMC: Underflow (resulting value less than 0) happens here.

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

@ -17,5 +17,3 @@ contract C is A {
}
}
// ----
// Warning 4144: (100-103): BMC: Underflow (resulting value less than 0) happens here.
// Warning 4144: (100-103): BMC: Underflow (resulting value less than 0) happens here.

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

@ -20,5 +20,3 @@ contract C is A {
// Warning 6328: (82-96): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nconstructor()
// Warning 6328: (148-162): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()
// Warning 6328: (180-194): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()
// Warning 4144: (100-103): BMC: Underflow (resulting value less than 0) happens here.
// Warning 4144: (100-103): BMC: Underflow (resulting value less than 0) happens here.

4
test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1.sol
View File

@ -21,7 +21,3 @@ contract C{
}
// ----
// Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 2661: (156-159): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (163-166): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (234-237): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (234-237): BMC: Underflow (resulting value less than 0) happens here.

4
test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol
View File

@ -24,7 +24,3 @@ contract C{
// Warning 6328: (138-152): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nconstructor(0)\nState: x = 1\nf()
// Warning 6328: (184-198): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nconstructor(0)\nState: x = 1\nf()
// Warning 6328: (82-96): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor(0)
// Warning 2661: (156-159): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (163-166): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (234-237): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (234-237): BMC: Underflow (resulting value less than 0) happens here.

1
test/libsolidity/smtCheckerTests/imports/import_base.sol
View File

@ -20,6 +20,7 @@ contract Der is Base {
// ----
// 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 = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\nState: x = 0, a = 0\ng(0)
// 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.
// Warning 2661: (base:100-103): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

2
test/libsolidity/smtCheckerTests/invariants/loop_basic.sol
View File

@ -11,3 +11,5 @@ contract Simple {
}
// ====
// SMTSolvers: z3
// ----
// Warning 4984: (132-135): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

2
test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol
View File

@ -9,3 +9,5 @@ contract Simple {
}
// ====
// SMTSolvers: z3
// ----
// Warning 4984: (116-119): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

2
test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol
View File

@ -15,4 +15,4 @@ contract C
// SMTSolvers: z3
// ----
// Warning 5740: (120-123): Unreachable code.
// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\n\nTransaction trace:\nconstructor()\nf(1)
// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\n\n\nTransaction trace:\nconstructor()\nf(3)

3
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
View File

@ -18,9 +18,10 @@ contract LoopFor2 {
}
}
// ====
// SMTSolvers: z3
// SMTIgnoreCex: yes
// SMTSolvers: z3
// ----
// Warning 4984: (244-249): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (270-273): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (373-392): CHC: Assertion violation happens here.
// Warning 6328: (396-415): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
View File

@ -26,3 +26,4 @@ contract LoopFor2 {
// SMTSolvers: z3
// ----
// Warning 4984: (237-242): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (263-266): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

1
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
View File

@ -21,5 +21,6 @@ contract LoopFor2 {
}
// ----
// Warning 4984: (229-234): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (255-258): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (338-357): CHC: Assertion violation happens here.\nCounterexample:\nb = [], c = []\nn = 1\n\n\nTransaction trace:\nconstructor()\nState: b = [], c = []\ntestUnboundedForLoop(1)
// Warning 6328: (361-380): CHC: Assertion violation happens here.\nCounterexample:\nb = [], c = []\nn = 1\n\n\nTransaction trace:\nconstructor()\nState: b = [], c = []\ntestUnboundedForLoop(1)

7
test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol
View File

@ -7,7 +7,7 @@ contract A {
A.y = A.x++;
assert(A.y == A.x - 1);
// Fails
assert(A.y == 0);
// assert(A.y == 0); // Disabled because of nondeterminism in Spacer
A.y = ++A.x;
assert(A.y == A.x);
delete A.x;
@ -25,6 +25,7 @@ contract A {
assert(A.y == A.x);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (160-176): CHC: Assertion violation happens here.\nCounterexample:\nx = (- 1), y = (- 2)\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, y = 0\na()\nState: x = (- 2), y = (- 2)\na()
// Warning 6328: (373-389): CHC: Assertion violation happens here.\nCounterexample:\nx = 8, y = (- 2)\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, y = 0\na()
// Warning 6328: (424-440): CHC: Assertion violation happens here.

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

@ -10,4 +10,4 @@ contract C {
}
}
// ----
// Warning 6328: (161-174): CHC: Assertion violation happens here.\nCounterexample:\n\na = 6\nb = 5\n\n\nTransaction trace:\nconstructor()\nf(5, 5)
// Warning 6328: (161-174): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nb = 1\n\n\nTransaction trace:\nconstructor()\nf(0, 0)

3
test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol
View File

@ -10,3 +10,6 @@ contract C {
}
}
// ----
// Warning 4984: (129-134): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 115792089237316195423570985008687907853269984665640564039457584007913129639935, b = false\n\nc = 0\n\nTransaction trace:\nconstructor()\nState: a = 0, b = false\nf()\nState: a = 115792089237316195423570985008687907853269984665640564039457584007913129639935, b = false\nf()
// Warning 3944: (137-140): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\na = 0, b = false\n\nc = 0\n\nTransaction trace:\nconstructor()\nState: a = 0, b = false\nf()
// Warning 6328: (150-163): CHC: Assertion violation happens here.\nCounterexample:\na = 115792089237316195423570985008687907853269984665640564039457584007913129639935, b = false\n\nc = 0\n\nTransaction trace:\nconstructor()\nState: a = 0, b = false\nf()

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

@ -15,4 +15,4 @@ contract C
}
}
// ----
// Warning 6328: (240-253): CHC: Assertion violation happens here.\nCounterexample:\narray = []\nx = 38\n\n\nTransaction trace:\nconstructor()\nState: array = []\nf(38)
// Warning 6328: (240-253): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/operators/unary_add_mapping.sol
View File

@ -14,5 +14,7 @@ contract C
assert(b < 3);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (244-257): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\n\nTransaction trace:\nconstructor()\nf(38)
// Warning 6328: (244-257): CHC: Assertion violation happens here.

25
test/libsolidity/smtCheckerTests/operators/unary_add_minus_overflow_detected.sol Normal file
View File

@ -0,0 +1,25 @@
pragma experimental SMTChecker;
contract C {
uint8 x;
function inc_pre() public {
++x;
}
function dec_pre() public {
--x;
}
/* Commented out because Spacer segfaults in Z3 4.8.9
function inc_post() public {
x++;
}
function dec_post() public {
x--;
}
*/
}
// ----
// Warning 4984: (87-90): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\nx = 255\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ndec_pre()\nState: x = 255\ninc_pre()
// Warning 3944: (127-130): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ndec_pre()

16
test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly.sol Normal file
View File

@ -0,0 +1,16 @@
pragma experimental SMTChecker;
contract C {
uint8 x = 254;
function inc_pre() public {
++x;
}
function check() view public {
uint y = x;
assert(y < 256);
}
}
// ----
// Warning 4984: (94-97): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\nx = 255\n\n\n\nTransaction trace:\nconstructor()\nState: x = 254\ninc_pre()\nState: x = 255\ninc_pre()

24
test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly_struct.sol Normal file
View File

@ -0,0 +1,24 @@
pragma experimental SMTChecker;
contract C {
struct S {
uint8 x;
}
S s;
constructor() {
s.x = 254;
}
function inc_pre() public {
++s.x;
}
function check() view public {
uint y = s.x;
assert(y < 256);
}
}
// ----
// Warning 4984: (145-150): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\ns = {x: 255}\n\n\n\nTransaction trace:\nconstructor()\nState: s = {x: 254}\ninc_pre()\nState: s = {x: 255}\ninc_pre()

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

@ -15,4 +15,4 @@ contract C
}
}
// ----
// Warning 6328: (240-253): CHC: Assertion violation happens here.\nCounterexample:\narray = []\nx = 38\n\n\nTransaction trace:\nconstructor()\nState: array = []\nf(38)
// Warning 6328: (240-253): CHC: Assertion violation happens here.\nCounterexample:\narray = []\nx = 0\n\n\nTransaction trace:\nconstructor()\nState: array = []\nf(0)

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

@ -15,4 +15,4 @@ contract C
}
}
// ----
// Warning 6328: (244-257): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\n\nTransaction trace:\nconstructor()\nf(38)
// Warning 6328: (244-257): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\n\nTransaction trace:\nconstructor()\nf(0)

12
test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol
View File

@ -52,6 +52,10 @@ contract C {
// Warning 8364: (258-260): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (271-275): Assertion checker does not yet support this expression.
// Warning 8364: (271-273): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4984: (132-138): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 4984: (142-148): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 3944: (165-171): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 3944: (175-181): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 4984: (200-208): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (185-209): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (213-247): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
@ -87,11 +91,3 @@ contract C {
// Warning 8364: (258-260): Assertion checker does not yet implement type struct C.S storage ref
// Warning 7650: (271-275): Assertion checker does not yet support this expression.
// Warning 8364: (271-273): Assertion checker does not yet implement type struct C.S storage ref
// Warning 4144: (132-138): BMC: Underflow (resulting value less than 0) happens here.
// Warning 2661: (132-138): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (142-148): BMC: Underflow (resulting value less than 0) happens here.
// Warning 2661: (142-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (165-171): BMC: Underflow (resulting value less than 0) happens here.
// Warning 2661: (165-171): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (175-181): BMC: Underflow (resulting value less than 0) happens here.
// Warning 2661: (175-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

2
test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol
View File

@ -15,4 +15,4 @@ contract C {
}
}
// ----
// 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\n\nTransaction trace:\nconstructor()\nf({x: 0, a: []}, {x: 3, a: [5, 5, 5, 5, 5, 5]})
// Warning 6328: (225-245): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 2, a: []}\ns2 = {x: 3, a: [6, 6, 6, 6, 6, 6, 6]}\n\n\nTransaction trace:\nconstructor()\nf({x: 0, a: []}, {x: 3, a: [6, 6, 6, 6, 6, 6, 6]})

2
test/libsolidity/smtCheckerTests/types/struct/struct_unary_sub.sol
View File

@ -16,4 +16,4 @@ contract C {
}
}
// ----
// Warning 6328: (240-260): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 98, a: []}\ns2 = {x: (- 38), a: [5, 5, 5, 5, 5, 5]}\n\n\nTransaction trace:\nconstructor()\nf({x: 0, a: []}, {x: (- 38), a: [5, 5, 5, 5, 5, 5]})
// Warning 6328: (240-260): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 98, a: []}\ns2 = {x: 99, a: [6, 6, 6, 6, 6, 6, 6]}\n\n\nTransaction trace:\nconstructor()\nf({x: 0, a: []}, {x: 99, a: [6, 6, 6, 6, 6, 6, 6]})

3
test/libsolidity/smtCheckerTests/types/unused_mapping.sol
View File

@ -12,6 +12,7 @@ contract C {
if(x == 0) x = 0; // noop state var read
x++;
y++;
assert(y == x);
// Commented out because of nondeterminism in Spacer in Z3 4.8.9
//assert(y == x);
}
}