-
Notifications
You must be signed in to change notification settings - Fork 3
/
timecontroller_fix_inv_corral.txt
115 lines (111 loc) · 6.96 KB
/
timecontroller_fix_inv_corral.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
Single threaded program detected
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Verifying program while tracking: {assertsPassed}
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Program has a potential bug: Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
False bug
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Verifying program while tracking: {assertsPassed, startTime_TimelockController}
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Program has a potential bug: Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
Warning: old(local var) expression used
True bug
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(62,1): error PF5001: This assertion can fail
Execution trace:
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(10,1): Trace: Thread=1 (CALL FreshRefGenerator, RETURN from FreshRefGenerator , CALL TimelockController_TimelockController, _verisolFirstArg = false, this = T@Ref!val!0, msg.sender = T@Ref!val!2, msg.value = 13, _verisolLastArg = true)
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(10,1): Trace: Thread=1 (CALL IERC20_IERC20)
/home/sallyjunsongwang/SmartInv/verifier/./Libraries/IERC20.sol(7,1): Trace: Thread=1 (_verisolFirstArg = false, this = T@Ref!val!0, msg.sender = T@Ref!val!2, msg.value = 13, _verisolLastArg = true)
/home/sallyjunsongwang/SmartInv/verifier/./Libraries/IERC20.sol(7,1): Trace: Thread=1 (CALL IERC20_IERC20_NoBaseCtor)
/home/sallyjunsongwang/SmartInv/verifier/./Libraries/IERC20.sol(7,1): Trace: Thread=1 (RETURN from IERC20_IERC20_NoBaseCtor )
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(10,1): Trace: Thread=1 (RETURN from IERC20_IERC20 )
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(10,1): Trace: Thread=1 (CALL TimelockController_TimelockController_NoBaseCtor)
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(10,1): Trace: Thread=1 (CALL FreshRefGenerator, RETURN from FreshRefGenerator , CALL FreshRefGenerator, RETURN from FreshRefGenerator , CALL FreshRefGenerator, RETURN from FreshRefGenerator , RETURN from TimelockController_TimelockController_NoBaseCtor )
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(42,1): Trace: Thread=1 (RETURN from TimelockController_TimelockController , CALL CorralChoice_TimelockController, CALL startExecute_TimelockController, _verisolFirstArg = false, this = T@Ref!val!0, msg.sender = T@Ref!val!3, msg.value = -715, _verisolLastArg = true)
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(43,1): Trace: Thread=1 ()
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(44,1): Trace: Thread=1 ()
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(44,1): Trace: Thread=1 (startTime = 719)
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(44,1): Trace: Thread=1 (RETURN from startExecute_TimelockController , RETURN from CorralChoice_TimelockController )
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(44,1): Trace: Thread=1 ()
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(44,1): Trace: Thread=1 (CALL CorralChoice_TimelockController)
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(57,1): Trace: Thread=1 (CALL endExecute_TimelockController, _verisolFirstArg = false, this = T@Ref!val!0, msg.sender = T@Ref!val!4, msg.value = -543, _verisolLastArg = true)
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(58,1): Trace: Thread=1 ()
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(59,1): Trace: Thread=1 ()
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(60,1): Trace: Thread=1 ()
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(62,1): Trace: Thread=1 ()
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(62,1): Trace: Thread=1 (ASSERTION FAILS assert old(__var_19) == __var_22;
)
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(44,1): Trace: Thread=1 (RETURN from endExecute_TimelockController , RETURN from CorralChoice_TimelockController )
/home/sallyjunsongwang/SmartInv/verifier/./timecontroller_fix_inv.sol(44,1): Trace: Thread=1 (Done)
Boogie verification time: 0.27 s
Time spent reading-writing programs: 0.50 s
Time spent checking a program (2): 0.41 s
Time spent checking a path (4): 0.38 s
Number of procedures inlined: 23
Number of variables tracked: 2
Total Time: 1.1730232 s
Total User CPU time: 1.23 s