Skip to content

Commit 93c3931

Browse files
Replace transfer with call in smt tests
1 parent c8ccc6c commit 93c3931

File tree

33 files changed

+95
-253
lines changed

33 files changed

+95
-253
lines changed

test/cmdlineTests/model_checker_targets_balance_chc/err

Lines changed: 0 additions & 7 deletions
This file was deleted.

test/cmdlineTests/model_checker_targets_balance_chc/input.sol

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,8 @@ contract test {
88
--x;
99
x + type(uint).max;
1010
2 / x;
11-
a.transfer(x);
11+
(bool success, ) = a.call{value: x}("");
12+
require(success);
1213
assert(x > 0);
1314
arr.pop();
1415
arr[x];

test/cmdlineTests/model_checker_targets_constant_condition_chc/err

Lines changed: 0 additions & 5 deletions
This file was deleted.

test/cmdlineTests/model_checker_targets_constant_condition_chc/input.sol

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,8 @@ contract test {
88
--x;
99
x + type(uint).max;
1010
2 / x;
11-
a.transfer(x);
11+
(bool success, ) = a.call{value: x}("");
12+
require(success);
1213
assert(x > 0);
1314
arr.pop();
1415
arr[x];

test/cmdlineTests/model_checker_targets_div_by_zero_chc/err

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,9 @@
1-
Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: <amount>}("")' instead.
2-
--> input.sol:10:3:
3-
|
4-
10 | a.transfer(x);
5-
| ^^^^^^^^^^
6-
71
Warning: CHC: Division by zero happens here.
82
Counterexample:
93
arr = []
104
a = 0x0
115
x = 0
6+
success = false
127

138
Transaction trace:
149
test.constructor()

test/cmdlineTests/model_checker_targets_div_by_zero_chc/input.sol

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,10 @@ contract test {
77
--x;
88
x + type(uint).max;
99
2 / x;
10-
a.transfer(x);
10+
(bool success, ) = a.call{value: x}("");
11+
require(success);
1112
assert(x > 0);
1213
arr.pop();
1314
arr[x];
1415
}
15-
}
16+
}

test/cmdlineTests/model_checker_targets_overflow_chc/err

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,9 @@
1-
Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: <amount>}("")' instead.
2-
--> input.sol:10:3:
3-
|
4-
10 | a.transfer(x);
5-
| ^^^^^^^^^^
6-
71
Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
82
Counterexample:
93
arr = []
104
a = 0x0
115
x = 1
6+
success = false
127

138
Transaction trace:
149
test.constructor()

test/cmdlineTests/model_checker_targets_overflow_chc/input.sol

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,10 @@ contract test {
77
--x;
88
x + type(uint).max;
99
2 / x;
10-
a.transfer(x);
10+
(bool success, ) = a.call{value: x}("");
11+
require(success);
1112
assert(x > 0);
1213
arr.pop();
1314
arr[x];
1415
}
15-
}
16+
}

test/cmdlineTests/model_checker_targets_underflow_chc/err

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,9 @@
1-
Warning: 'transfer' is deprecated and scheduled for removal. Use 'call{value: <amount>}("")' instead.
2-
--> input.sol:10:3:
3-
|
4-
10 | a.transfer(x);
5-
| ^^^^^^^^^^
6-
71
Warning: CHC: Underflow (resulting value less than 0) happens here.
82
Counterexample:
93
arr = []
104
a = 0x0
115
x = 0
6+
success = false
127

138
Transaction trace:
149
test.constructor()

test/cmdlineTests/model_checker_targets_underflow_chc/input.sol

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,10 @@ contract test {
77
--x;
88
x + type(uint).max;
99
2 / x;
10-
a.transfer(x);
10+
(bool success, ) = a.call{value: x}("");
11+
require(success);
1112
assert(x > 0);
1213
arr.pop();
1314
arr[x];
1415
}
15-
}
16+
}

0 commit comments

Comments
 (0)