File tree Expand file tree Collapse file tree 6 files changed +10
-10
lines changed
model_checker_invariants_all
model_checker_invariants_contract_reentrancy
model_checker_invariants_contract
model_checker_invariants_reentrancy
standard_model_checker_invariants_contract
standard_model_checker_invariants_reentrancy Expand file tree Collapse file tree 6 files changed +10
-10
lines changed Original file line number Diff line number Diff line change @@ -5,8 +5,8 @@ Warning: Return value of low-level calls not used.
5
5
| ^^^^^^^^^^^
6
6
7
7
Info: Contract invariant(s) for model_checker_invariants_all/input.sol:test:
8
- ((x <= 0 ) || true)
8
+ (! (x >= 1 ) || true)
9
9
Reentrancy property(ies) for model_checker_invariants_all/input.sol:test:
10
- (((!(x <= 0) || (x' <= 0 )) && (!(x <= 0) || (<errorCode> <= 0 ))) || true)
10
+ (((!(x <= 0) || ! (x' >= 1 )) && (!(x <= 0) || ! (<errorCode> >= 1 ))) || true)
11
11
<errorCode> = 0 -> no errors
12
12
<errorCode> = 1 -> Assertion failed at assert(x == 0)
Original file line number Diff line number Diff line change 1
1
Info: Contract invariant(s) for model_checker_invariants_contract/input.sol:test:
2
- ((x <= 0 ) || true)
2
+ (! (x >= 1 ) || true)
Original file line number Diff line number Diff line change @@ -5,8 +5,8 @@ Warning: Return value of low-level calls not used.
5
5
| ^^^^^^^^^^^
6
6
7
7
Info: Contract invariant(s) for model_checker_invariants_contract_reentrancy/input.sol:test:
8
- ((x <= 0 ) || true)
8
+ (! (x >= 1 ) || true)
9
9
Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test:
10
- (((!(x <= 0) || (x' <= 0 )) && (!(x <= 0) || (<errorCode> <= 0 ))) || true)
10
+ (((!(x <= 0) || ! (x' >= 1 )) && (!(x <= 0) || ! (<errorCode> >= 1 ))) || true)
11
11
<errorCode> = 0 -> no errors
12
12
<errorCode> = 1 -> Assertion failed at assert(x == 0)
Original file line number Diff line number Diff line change @@ -5,6 +5,6 @@ Warning: Return value of low-level calls not used.
5
5
| ^^^^^^^^^^^
6
6
7
7
Info: Reentrancy property(ies) for model_checker_invariants_reentrancy/input.sol:test:
8
- (((!(x <= 0) || (x' <= 0 )) && (!(x <= 0) || (<errorCode> <= 0 ))) || true)
8
+ (((!(x <= 0) || ! (x' >= 1 )) && (!(x <= 0) || ! (<errorCode> >= 1 ))) || true)
9
9
<errorCode> = 0 -> no errors
10
10
<errorCode> = 1 -> Assertion failed at assert(x < 10)
Original file line number Diff line number Diff line change 5
5
"component" : " general" ,
6
6
"errorCode" : " 1180" ,
7
7
"formattedMessage" : "Info: Contract invariant(s) for A:test:
8
- ((x <= 0 ) || true)
8
+ (! (x >= 1 ) || true)
9
9
10
10
11
11
",
12
12
"message" : "Contract invariant(s) for A:test:
13
- ((x <= 0 ) || true)
13
+ (! (x >= 1 ) || true)
14
14
",
15
15
"severity" : " info" ,
16
16
"type" : " Info"
Original file line number Diff line number Diff line change 25
25
"component" : " general" ,
26
26
"errorCode" : " 1180" ,
27
27
"formattedMessage" : "Info: Reentrancy property(ies) for A:test:
28
- (((!(x <= 0) || (x' <= 0 )) && (!(x <= 0) || (<errorCode> <= 0 ))) || true)
28
+ (((!(x <= 0) || ! (x' >= 1 )) && (!(x <= 0) || ! (<errorCode> >= 1 ))) || true)
29
29
<errorCode> = 0 -> no errors
30
30
<errorCode> = 1 -> Assertion failed at assert(x < 10)
31
31
32
32
33
33
",
34
34
"message" : "Reentrancy property(ies) for A:test:
35
- (((!(x <= 0) || (x' <= 0 )) && (!(x <= 0) || (<errorCode> <= 0 ))) || true)
35
+ (((!(x <= 0) || ! (x' >= 1 )) && (!(x <= 0) || ! (<errorCode> >= 1 ))) || true)
36
36
<errorCode> = 0 -> no errors
37
37
<errorCode> = 1 -> Assertion failed at assert(x < 10)
38
38
",
You can’t perform that action at this time.
0 commit comments