@@ -214,8 +214,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
214214 return new EVMAbstractState (result , memory , storage , mu_i );
215215 }
216216 case "OriginOperator" : { // ORIGIN
217- // At the moment, we do not handle ORIGIN
218-
219217 for (AbstractStack stack : stacks ) {
220218 AbstractStack resultStack = stack .clone ();
221219 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -225,8 +223,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
225223 return new EVMAbstractState (result , memory , storage , mu_i );
226224 }
227225 case "CallerOperator" : { // CALLER
228- // At the moment, we do not handle CALLER
229-
230226 for (AbstractStack stack : stacks ) {
231227 AbstractStack resultStack = stack .clone ();
232228 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -236,8 +232,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
236232 return new EVMAbstractState (result , memory , storage , mu_i );
237233 }
238234 case "CallvalueOperator" : { // CALLVALUE
239- // At the moment, we do not handle CALLVALUE
240-
241235 for (AbstractStack stack : stacks ) {
242236 AbstractStack resultStack = stack .clone ();
243237 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -247,8 +241,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
247241 return new EVMAbstractState (result , memory , storage , mu_i );
248242 }
249243 case "CalldatasizeOperator" : { // CALLDATASIZE
250- // At the moment, we do not handle CALLDATASIZE
251-
252244 for (AbstractStack stack : stacks ) {
253245 AbstractStack resultStack = stack .clone ();
254246 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -258,8 +250,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
258250 return new EVMAbstractState (result , memory , storage , mu_i );
259251 }
260252 case "CodesizeOperator" : { // CODESIZE
261- // At the moment, we do not handle CODESIZE
262-
263253 for (AbstractStack stack : stacks ) {
264254 AbstractStack resultStack = stack .clone ();
265255 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -269,8 +259,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
269259 return new EVMAbstractState (result , memory , storage , mu_i );
270260 }
271261 case "GaspriceOperator" : { // GASPRICE
272- // At the moment, we do not handle GASPRIZE
273-
274262 for (AbstractStack stack : stacks ) {
275263 AbstractStack resultStack = stack .clone ();
276264 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -280,8 +268,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
280268 return new EVMAbstractState (result , memory , storage , mu_i );
281269 }
282270 case "ReturndatasizeOperator" : { // RETURNDATASIZE
283- // At the moment, we do not handle RETURNDATASIZE
284-
285271 for (AbstractStack stack : stacks ) {
286272 AbstractStack resultStack = stack .clone ();
287273 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -291,8 +277,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
291277 return new EVMAbstractState (result , memory , storage , mu_i );
292278 }
293279 case "CoinbaseOperator" : { // COINBASE
294- // At the moment, we do not handle COINBASE
295-
296280 for (AbstractStack stack : stacks ) {
297281 AbstractStack resultStack = stack .clone ();
298282 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -302,8 +286,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
302286 return new EVMAbstractState (result , memory , storage , mu_i );
303287 }
304288 case "TimestampOperator" : { // TIMESTAMP
305- // At the moment, we do not handle TIMESTAMP
306-
307289 for (AbstractStack stack : stacks ) {
308290 AbstractStack resultStack = stack .clone ();
309291 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -313,8 +295,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
313295 return new EVMAbstractState (result , memory , storage , mu_i );
314296 }
315297 case "NumberOperator" : { // NUMBER
316- // At the moment, we do not handle NUMBER
317-
318298 for (AbstractStack stack : stacks ) {
319299 AbstractStack resultStack = stack .clone ();
320300 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -324,8 +304,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
324304 return new EVMAbstractState (result , memory , storage , mu_i );
325305 }
326306 case "DifficultyOperator" : { // DIFFICULTY
327- // At the moment, we do not handle DIFFICULTY
328-
329307 for (AbstractStack stack : stacks ) {
330308 AbstractStack resultStack = stack .clone ();
331309 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -335,8 +313,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
335313 return new EVMAbstractState (result , memory , storage , mu_i );
336314 }
337315 case "GaslimitOperator" : { // GASLIMIT
338- // At the moment, we do not handle GASLIMIT
339-
340316 for (AbstractStack stack : stacks ) {
341317 AbstractStack resultStack = stack .clone ();
342318 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -346,8 +322,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
346322 return new EVMAbstractState (result , memory , storage , mu_i );
347323 }
348324 case "ChainidOperator" : { // CHAINID
349- // At the moment, we do not handle CHAINID
350-
351325 for (AbstractStack stack : stacks ) {
352326 AbstractStack resultStack = stack .clone ();
353327 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -357,8 +331,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
357331 return new EVMAbstractState (result , memory , storage , mu_i );
358332 }
359333 case "SelfbalanceOperator" : { // SELFBALANCE
360- // At the moment, we do not handle SELFBALANCE
361-
362334 for (AbstractStack stack : stacks ) {
363335 AbstractStack resultStack = stack .clone ();
364336 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -368,7 +340,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
368340 return new EVMAbstractState (result , memory , storage , mu_i );
369341 }
370342 case "PcOperator" : { // PC
371-
372343 for (AbstractStack stack : stacks ) {
373344 AbstractStack resultStack = stack .clone ();
374345 Integer i = (Integer ) ((Constant ) un .getExpression ()).getValue ();
@@ -379,8 +350,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
379350 return new EVMAbstractState (result , memory , storage , mu_i );
380351 }
381352 case "GasOperator" : { // GAS
382- // At the moment, we do not handle GAS
383-
384353 for (AbstractStack stack : stacks ) {
385354 AbstractStack resultStack = stack .clone ();
386355 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -390,8 +359,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
390359 return new EVMAbstractState (result , memory , storage , mu_i );
391360 }
392361 case "MsizeOperator" : { // MSIZE
393- // At the moment, we do not handle MSIZE
394-
395362 for (AbstractStack stack : stacks ) {
396363 AbstractStack resultStack = stack .clone ();
397364 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -401,8 +368,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
401368 return new EVMAbstractState (result , memory , storage , mu_i );
402369 }
403370 case "BasefeeOperator" : { // BASEFEE
404- // At the moment, we do not handle BASEFEE
405-
406371 for (AbstractStack stack : stacks ) {
407372 AbstractStack resultStack = stack .clone ();
408373 resultStack .push (StackElement .NOT_JUMPDEST_TOP );
@@ -942,8 +907,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
942907 return new EVMAbstractState (result , memory , storage , mu_i );
943908 }
944909 case "Sha3Operator" : { // SHA3
945- // At the moment, we do not handle SHA3
946-
947910 for (AbstractStack stack : stacks ) {
948911 if (stack .hasBottomUntil (2 ))
949912 continue ;
@@ -961,8 +924,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
961924 return new EVMAbstractState (result , memory , storage , mu_i );
962925 }
963926 case "BalanceOperator" : { // BALANCE
964- // At the moment, we do not handle BALANCE
965-
966927 for (AbstractStack stack : stacks ) {
967928 if (stack .hasBottomUntil (1 ))
968929 continue ;
@@ -979,8 +940,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
979940 return new EVMAbstractState (result , memory , storage , mu_i );
980941 }
981942 case "CalldataloadOperator" : { // CALLDATALOAD
982- // At the moment, we do not handle CALLDATALOAD
983-
984943 for (AbstractStack stack : stacks ) {
985944 if (stack .hasBottomUntil (1 ))
986945 continue ;
@@ -997,8 +956,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
997956 return new EVMAbstractState (result , memory , storage , mu_i );
998957 }
999958 case "CalldatacopyOperator" : { // CALLDATACOPY
1000- // At the moment, we do not handle CALLDATACOPY
1001-
1002959 for (AbstractStack stack : stacks ) {
1003960 if (stack .hasBottomUntil (3 ))
1004961 continue ;
@@ -1016,8 +973,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
1016973 return new EVMAbstractState (result , memory , storage , mu_i );
1017974 }
1018975 case "CodecopyOperator" : { // CODECOPY
1019- // At the moment, we do not handle CODECOPY
1020-
1021976 for (AbstractStack stack : stacks ) {
1022977 if (stack .hasBottomUntil (3 ))
1023978 continue ;
@@ -1035,8 +990,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
1035990 return new EVMAbstractState (result , memory , storage , mu_i );
1036991 }
1037992 case "ExtcodesizeOperator" : { // EXTCODESIZE
1038- // At the moment, we do not handle EXTCODESIZE
1039-
1040993 for (AbstractStack stack : stacks ) {
1041994 if (stack .hasBottomUntil (1 ))
1042995 continue ;
@@ -1053,8 +1006,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
10531006 return new EVMAbstractState (result , memory , storage , mu_i );
10541007 }
10551008 case "ExtcodecopyOperator" : { // EXTCODECOPY
1056- // At the moment, we do not handle EXTCODECOPY
1057-
10581009 for (AbstractStack stack : stacks ) {
10591010 if (stack .hasBottomUntil (4 ))
10601011 continue ;
@@ -1073,8 +1024,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
10731024 return new EVMAbstractState (result , memory , storage , mu_i );
10741025 }
10751026 case "ReturndatacopyOperator" : { // RETURNDATACOPY
1076- // At the moment, we do not handle RETURNDATACOPY
1077-
10781027 for (AbstractStack stack : stacks ) {
10791028 if (stack .hasBottomUntil (3 ))
10801029 continue ;
@@ -1092,8 +1041,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
10921041 return new EVMAbstractState (result , memory , storage , mu_i );
10931042 }
10941043 case "ExtcodehashOperator" : { // EXTCODEHASH
1095- // At the moment, we do not handle EXTCODEHASH
1096-
10971044 for (AbstractStack stack : stacks ) {
10981045 if (stack .hasBottomUntil (1 ))
10991046 continue ;
@@ -1110,8 +1057,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
11101057 return new EVMAbstractState (result , memory , storage , mu_i );
11111058 }
11121059 case "BlockhashOperator" : { // BLOCKHASH
1113- // At the moment, we do not handle BLOCKHASH
1114-
11151060 for (AbstractStack stack : stacks ) {
11161061 if (stack .hasBottomUntil (1 ))
11171062 continue ;
@@ -1769,8 +1714,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
17691714 return new EVMAbstractState (result , memory , storage , mu_i );
17701715 }
17711716 case "Log0Operator" : { // LOG0
1772- // At the moment, we do not handle LOG0
1773-
17741717 for (AbstractStack stack : stacks ) {
17751718 if (stack .hasBottomUntil (2 ))
17761719 continue ;
@@ -1787,8 +1730,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
17871730 return new EVMAbstractState (result , memory , storage , mu_i );
17881731 }
17891732 case "Log1Operator" : { // LOG1
1790- // At the moment, we do not handle LOG1
1791-
17921733 for (AbstractStack stack : stacks ) {
17931734 if (stack .hasBottomUntil (3 ))
17941735 continue ;
@@ -1806,8 +1747,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
18061747 return new EVMAbstractState (result , memory , storage , mu_i );
18071748 }
18081749 case "Log2Operator" : { // LOG2
1809- // At the moment, we do not handle LOG2
1810-
18111750 for (AbstractStack stack : stacks ) {
18121751 if (stack .hasBottomUntil (4 ))
18131752 continue ;
@@ -1826,8 +1765,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
18261765 return new EVMAbstractState (result , memory , storage , mu_i );
18271766 }
18281767 case "Log3Operator" : { // LOG3
1829- // At the moment, we do not handle LOG3
1830-
18311768 for (AbstractStack stack : stacks ) {
18321769 if (stack .hasBottomUntil (5 ))
18331770 continue ;
@@ -1847,8 +1784,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
18471784 return new EVMAbstractState (result , memory , storage , mu_i );
18481785 }
18491786 case "Log4Operator" : { // LOG4
1850- // At the moment, we do not handle LOG4
1851-
18521787 for (AbstractStack stack : stacks ) {
18531788 if (stack .hasBottomUntil (6 ))
18541789 continue ;
@@ -1869,8 +1804,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
18691804 return new EVMAbstractState (result , memory , storage , mu_i );
18701805 }
18711806 case "CreateOperator" : { // CREATE
1872- // At the moment, we do not handle CREATE
1873-
18741807 for (AbstractStack stack : stacks ) {
18751808 if (stack .hasBottomUntil (3 ))
18761809 continue ;
@@ -1889,8 +1822,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
18891822 return new EVMAbstractState (result , memory , storage , mu_i );
18901823 }
18911824 case "Create2Operator" : { // CREATE2
1892- // At the moment, we do not handle CREATE2
1893-
18941825 for (AbstractStack stack : stacks ) {
18951826 if (stack .hasBottomUntil (4 ))
18961827 continue ;
@@ -1910,8 +1841,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
19101841 return new EVMAbstractState (result , memory , storage , mu_i );
19111842 }
19121843 case "CallOperator" : { // CALL
1913- // At the moment, we do not handle CALL
1914-
19151844 for (AbstractStack stack : stacks ) {
19161845 if (stack .hasBottomUntil (7 ))
19171846 continue ;
@@ -1934,8 +1863,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
19341863 return new EVMAbstractState (result , memory , storage , mu_i );
19351864 }
19361865 case "CallcodeOperator" : { // CALLCODE
1937- // At the moment, we do not handle CALLCODE
1938-
19391866 for (AbstractStack stack : stacks ) {
19401867 if (stack .hasBottomUntil (7 ))
19411868 continue ;
@@ -1958,8 +1885,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
19581885 return new EVMAbstractState (result , memory , storage , mu_i );
19591886 }
19601887 case "ReturnOperator" : { // RETURN
1961- // At the moment, we do not handle RETURN
1962-
19631888 for (AbstractStack stack : stacks ) {
19641889 if (stack .hasBottomUntil (2 ))
19651890 continue ;
@@ -1976,8 +1901,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
19761901 return new EVMAbstractState (result , memory , storage , mu_i );
19771902 }
19781903 case "DelegatecallOperator" : { // DELEGATECALL
1979- // At the moment, we do not handle DELEGATECALL
1980-
19811904 for (AbstractStack stack : stacks ) {
19821905 if (stack .hasBottomUntil (6 ))
19831906 continue ;
@@ -1999,8 +1922,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
19991922 return new EVMAbstractState (result , memory , storage , mu_i );
20001923 }
20011924 case "StaticcallOperator" : { // STATICCALL
2002- // At the moment, we do not handle STATICCALL
2003-
20041925 for (AbstractStack stack : stacks ) {
20051926 if (stack .hasBottomUntil (6 ))
20061927 continue ;
@@ -2022,8 +1943,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
20221943 return new EVMAbstractState (result , memory , storage , mu_i );
20231944 }
20241945 case "RevertOperator" : { // REVERT
2025- // At the moment, we do not handle REVERT
2026-
20271946 for (AbstractStack stack : stacks ) {
20281947 if (stack .hasBottomUntil (2 ))
20291948 continue ;
@@ -2043,8 +1962,6 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
20431962 return this ;
20441963 }
20451964 case "SelfdestructOperator" : { // SELFDESTRUCT
2046- // At the moment, we do not handle SELFDESTRUCT
2047-
20481965 for (AbstractStack stack : stacks ) {
20491966 if (stack .hasBottomUntil (1 ))
20501967 continue ;
0 commit comments