Skip to content

Commit dbc9394

Browse files
rootroot
root
authored and
root
committed
Add InvCon output: .inv file for 201804_BEC (BecToken)
1 parent 28c8137 commit dbc9394

1 file changed

Lines changed: 181 additions & 0 deletions

File tree

‎results/201804_BEC/BecToken.inv‎

Lines changed: 181 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,181 @@
1+
Daikon version 5.8.6, released December 2, 2020; http://plse.cs.washington.edu/daikon.
2+
Reading declaration files Processing trace data; reading 1 dtrace file:
3+
Warning: Daikon is using a dataflow hierarchy analysis on a data trace that does not appear to be over a program execution, consider running Daikon with the --nohierarchy flag.
4+
5+
===========================================================================
6+
BecToken.approve(address,uint256):::EXIT2
7+
this == orig(this)
8+
this.ERC20Basic_own_totalSupply == this.decimals
9+
this.ERC20Basic_own_totalSupply == msg.value
10+
this.ERC20Basic_own_totalSupply == orig(msg.value)
11+
this.ERC20Basic_own_totalSupply == orig(this.StandardToken_own_allowed[post(pair(_spender,msg.sender))].getSubValue())
12+
this.BasicToken_own_balances == orig(this.BasicToken_own_balances)
13+
this.StandardToken_own_allowed == orig(this.StandardToken_own_allowed)
14+
this.StandardToken_own_allowed[].getSubLength() == orig(this.StandardToken_own_allowed[].getSubLength())
15+
this.Ownable_own_owner == orig(this.Ownable_own_owner)
16+
this.Pausable_own_paused == orig(this.Pausable_own_paused)
17+
this.decimals == msg.value
18+
this.decimals == orig(msg.value)
19+
this.decimals == orig(this.StandardToken_own_allowed[post(pair(_spender,msg.sender))].getSubValue())
20+
_spender == orig(_spender)
21+
_value == orig(_value)
22+
msg.sender == orig(msg.sender)
23+
msg.value == orig(msg.value)
24+
msg.value == orig(this.StandardToken_own_allowed[post(pair(_spender,msg.sender))].getSubValue())
25+
block.timestamp == orig(block.timestamp)
26+
orig(msg.value) == orig(this.StandardToken_own_allowed[post(pair(_spender,msg.sender))].getSubValue())
27+
sum(this.StandardToken_own_allowed[].getSubLength()) == sum(orig(this.StandardToken_own_allowed[].getSubLength()))
28+
this.ERC20Basic_own_totalSupply == 0
29+
this.BasicToken_own_balances has only one value
30+
this.StandardToken_own_allowed has only one value
31+
this.Pausable_own_paused == false
32+
this.decimals == 0
33+
_value one of { 8000000000000000000, 18000000000000000000 }
34+
msg.value == 0
35+
block.timestamp one of { 1519325045, 1519325875, 1519459085 }
36+
orig(this) has only one value
37+
orig(_value) one of { 8000000000000000000, 18000000000000000000 }
38+
orig(msg.value) == 0
39+
orig(block.timestamp) one of { 1519325045, 1519325875, 1519459085 }
40+
sum(this.StandardToken_own_allowed[].getSubLength()) == 0
41+
orig(this.StandardToken_own_allowed[post(pair(_spender,msg.sender))].getSubValue()) == 0
42+
===========================================================================
43+
BecToken.batchTransfer(address[],uint256):::EXIT2
44+
this == orig(this)
45+
this.ERC20Basic_own_totalSupply == this.decimals
46+
this.ERC20Basic_own_totalSupply == msg.value
47+
this.ERC20Basic_own_totalSupply == orig(this.ERC20Basic_own_totalSupply)
48+
this.ERC20Basic_own_totalSupply == orig(this.decimals)
49+
this.ERC20Basic_own_totalSupply == orig(msg.value)
50+
this.ERC20Basic_own_totalSupply == sum(this.BasicToken_own_balances[].getValue())
51+
this.BasicToken_own_balances == orig(this.BasicToken_own_balances)
52+
this.StandardToken_own_allowed == orig(this.StandardToken_own_allowed)
53+
this.StandardToken_own_allowed[].getSubLength() == orig(this.StandardToken_own_allowed[].getSubLength())
54+
this.Ownable_own_owner == orig(this.Ownable_own_owner)
55+
this.Pausable_own_paused == orig(this.Pausable_own_paused)
56+
this.decimals == msg.value
57+
this.decimals == orig(this.ERC20Basic_own_totalSupply)
58+
this.decimals == orig(this.decimals)
59+
this.decimals == orig(msg.value)
60+
this.decimals == sum(this.BasicToken_own_balances[].getValue())
61+
_receivers == orig(_receivers)
62+
_value == orig(_value)
63+
msg.sender == orig(msg.sender)
64+
msg.value == orig(this.ERC20Basic_own_totalSupply)
65+
msg.value == orig(this.decimals)
66+
msg.value == orig(msg.value)
67+
msg.value == sum(this.BasicToken_own_balances[].getValue())
68+
block.timestamp == orig(block.timestamp)
69+
orig(this.ERC20Basic_own_totalSupply) == orig(this.decimals)
70+
orig(this.ERC20Basic_own_totalSupply) == orig(msg.value)
71+
orig(this.ERC20Basic_own_totalSupply) == sum(this.BasicToken_own_balances[].getValue())
72+
orig(this.decimals) == orig(msg.value)
73+
orig(this.decimals) == sum(this.BasicToken_own_balances[].getValue())
74+
orig(msg.value) == sum(this.BasicToken_own_balances[].getValue())
75+
sum(this.StandardToken_own_allowed[].getSubLength()) == sum(orig(this.StandardToken_own_allowed[].getSubLength()))
76+
this.ERC20Basic_own_totalSupply == 0
77+
this.BasicToken_own_balances has only one value
78+
this.StandardToken_own_allowed has only one value
79+
this.Pausable_own_paused == false
80+
this.decimals == 0
81+
msg.value == 0
82+
orig(this) has only one value
83+
orig(this) != null
84+
orig(this.ERC20Basic_own_totalSupply) == 0
85+
orig(this.decimals) == 0
86+
orig(_receivers) has only one value
87+
orig(msg.value) == 0
88+
sum(this.BasicToken_own_balances[].getValue()) == 0
89+
sum(this.StandardToken_own_allowed[].getSubLength()) == 0
90+
this.ERC20Basic_own_totalSupply <= _value
91+
this.ERC20Basic_own_totalSupply < block.timestamp
92+
this.ERC20Basic_own_totalSupply <= orig(_value)
93+
this.ERC20Basic_own_totalSupply < orig(block.timestamp)
94+
this.Ownable_own_owner != orig(msg.sender)
95+
this.decimals <= _value
96+
this.decimals < block.timestamp
97+
this.decimals <= orig(_value)
98+
this.decimals < orig(block.timestamp)
99+
msg.value < block.timestamp
100+
msg.value <= orig(_value)
101+
msg.value < orig(block.timestamp)
102+
orig(this.ERC20Basic_own_totalSupply) <= orig(_value)
103+
orig(this.ERC20Basic_own_totalSupply) < orig(block.timestamp)
104+
orig(this.decimals) <= orig(_value)
105+
orig(this.decimals) < orig(block.timestamp)
106+
orig(msg.value) < orig(block.timestamp)
107+
===========================================================================
108+
BecToken.transfer(address,uint256):::EXIT2
109+
this == orig(this)
110+
this.ERC20Basic_own_totalSupply == this.decimals
111+
this.ERC20Basic_own_totalSupply == msg.value
112+
this.ERC20Basic_own_totalSupply == orig(this.ERC20Basic_own_totalSupply)
113+
this.ERC20Basic_own_totalSupply == orig(this.decimals)
114+
this.ERC20Basic_own_totalSupply == orig(msg.value)
115+
this.ERC20Basic_own_totalSupply == sum(this.BasicToken_own_balances[].getValue())
116+
this.ERC20Basic_own_totalSupply == orig(this.StandardToken_own_allowed[post(pair(_to,msg.sender))].getSubValue())
117+
this.BasicToken_own_balances == orig(this.BasicToken_own_balances)
118+
this.StandardToken_own_allowed == orig(this.StandardToken_own_allowed)
119+
this.StandardToken_own_allowed[].getSubLength() == orig(this.StandardToken_own_allowed[].getSubLength())
120+
this.Ownable_own_owner == orig(this.Ownable_own_owner)
121+
this.Pausable_own_paused == orig(this.Pausable_own_paused)
122+
this.decimals == msg.value
123+
this.decimals == orig(this.ERC20Basic_own_totalSupply)
124+
this.decimals == orig(this.decimals)
125+
this.decimals == orig(msg.value)
126+
this.decimals == sum(this.BasicToken_own_balances[].getValue())
127+
this.decimals == orig(this.StandardToken_own_allowed[post(pair(_to,msg.sender))].getSubValue())
128+
_to == orig(_to)
129+
_value == orig(_value)
130+
msg.sender == orig(msg.sender)
131+
msg.value == orig(this.ERC20Basic_own_totalSupply)
132+
msg.value == orig(this.decimals)
133+
msg.value == orig(msg.value)
134+
msg.value == sum(this.BasicToken_own_balances[].getValue())
135+
msg.value == orig(this.StandardToken_own_allowed[post(pair(_to,msg.sender))].getSubValue())
136+
block.timestamp == orig(block.timestamp)
137+
orig(this.ERC20Basic_own_totalSupply) == orig(this.decimals)
138+
orig(this.ERC20Basic_own_totalSupply) == orig(msg.value)
139+
orig(this.ERC20Basic_own_totalSupply) == sum(this.BasicToken_own_balances[].getValue())
140+
orig(this.ERC20Basic_own_totalSupply) == orig(this.StandardToken_own_allowed[post(pair(_to,msg.sender))].getSubValue())
141+
orig(this.decimals) == orig(msg.value)
142+
orig(this.decimals) == sum(this.BasicToken_own_balances[].getValue())
143+
orig(this.decimals) == orig(this.StandardToken_own_allowed[post(pair(_to,msg.sender))].getSubValue())
144+
orig(msg.value) == sum(this.BasicToken_own_balances[].getValue())
145+
orig(msg.value) == orig(this.StandardToken_own_allowed[post(pair(_to,msg.sender))].getSubValue())
146+
sum(this.BasicToken_own_balances[].getValue()) == orig(this.StandardToken_own_allowed[post(pair(_to,msg.sender))].getSubValue())
147+
sum(this.StandardToken_own_allowed[].getSubLength()) == sum(orig(this.StandardToken_own_allowed[].getSubLength()))
148+
this.ERC20Basic_own_totalSupply == 0
149+
this.BasicToken_own_balances has only one value
150+
this.StandardToken_own_allowed has only one value
151+
this.Pausable_own_paused == false
152+
this.decimals == 0
153+
msg.value == 0
154+
orig(this) has only one value
155+
orig(this) != null
156+
orig(this.ERC20Basic_own_totalSupply) == 0
157+
orig(this.decimals) == 0
158+
orig(msg.value) == 0
159+
sum(this.BasicToken_own_balances[].getValue()) == 0
160+
sum(this.StandardToken_own_allowed[].getSubLength()) == 0
161+
orig(this.StandardToken_own_allowed[post(pair(_to,msg.sender))].getSubValue()) == 0
162+
this.ERC20Basic_own_totalSupply < _value
163+
this.ERC20Basic_own_totalSupply < block.timestamp
164+
this.ERC20Basic_own_totalSupply < orig(_value)
165+
this.ERC20Basic_own_totalSupply < orig(block.timestamp)
166+
this.Ownable_own_owner != orig(_to)
167+
this.Ownable_own_owner != orig(msg.sender)
168+
this.decimals < _value
169+
this.decimals < block.timestamp
170+
this.decimals < orig(_value)
171+
this.decimals < orig(block.timestamp)
172+
msg.value < block.timestamp
173+
msg.value < orig(_value)
174+
msg.value < orig(block.timestamp)
175+
block.timestamp < orig(_value)
176+
orig(this.ERC20Basic_own_totalSupply) < orig(_value)
177+
orig(this.ERC20Basic_own_totalSupply) < orig(block.timestamp)
178+
orig(this.decimals) < orig(_value)
179+
orig(this.decimals) < orig(block.timestamp)
180+
orig(msg.value) < orig(block.timestamp)
181+
Exiting Daikon.

0 commit comments

Comments
 (0)