Skip to content

Commit

Permalink
update expected output
Browse files Browse the repository at this point in the history
  • Loading branch information
anvacaru committed Jan 27, 2025
1 parent f9fb172 commit dfb1a6f
Show file tree
Hide file tree
Showing 51 changed files with 695 additions and 695 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0
<kevm>
<k>
( #execute => #halt )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -50,7 +50,7 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0
b""
</output>
<statusCode>
( _STATUSCODE => EVMC_SUCCESS )
( _STATUSCODE:StatusCode => EVMC_SUCCESS )
</statusCode>
<callStack>
.List
Expand Down Expand Up @@ -304,7 +304,7 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
andBool ( _C_ACCOUNTPARAMSTEST_ID =/=Int 645326474426547203313410069153905908525362434349
andBool ( _C_ACCOUNTPARAMSTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349
andBool ( CALLER_ID:Int <Int pow160
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
<kevm>
<k>
( #execute => #halt )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -96,10 +96,10 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
<ethereum>
<evm>
<output>
( _OUTPUT_CELL => #buf ( 32 , ( KV0_x:Int +Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) ) )
( _OUTPUT_CELL:Bytes => #buf ( 32 , ( KV0_x:Int +Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) ) )
</output>
<statusCode>
( _STATUSCODE => EVMC_SUCCESS )
( _STATUSCODE:StatusCode => EVMC_SUCCESS )
</statusCode>
<callState>
<id>
Expand Down Expand Up @@ -261,7 +261,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
<kevm>
<k>
( #execute => #halt )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -275,10 +275,10 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
<ethereum>
<evm>
<output>
( _OUTPUT_CELL => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" )
( _OUTPUT_CELL:Bytes => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" )
</output>
<statusCode>
( _STATUSCODE => EVMC_REVERT )
( _STATUSCODE:StatusCode => EVMC_REVERT )
</statusCode>
<callState>
<id>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0
<kevm>
<k>
( #execute => #halt )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -51,7 +51,7 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0
b""
</output>
<statusCode>
( _STATUSCODE => EVMC_SUCCESS )
( _STATUSCODE:StatusCode => EVMC_SUCCESS )
</statusCode>
<callStack>
.List
Expand Down Expand Up @@ -264,7 +264,7 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
andBool ( _C_ADDRTEST_ID =/=Int 645326474426547203313410069153905908525362434349
andBool ( _C_ADDRTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349
andBool ( CALLER_ID:Int <Int pow160
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
~> #return 128 32
~> #pc [ STATICCALL ]
~> #execute => #halt ~> .K )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -141,7 +141,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" )
</output>
<statusCode>
( _STATUSCODE => EVMC_REVERT )
( _STATUSCODE:StatusCode => EVMC_REVERT )
</statusCode>
<callStack>
( ListItem ( <callState>
Expand Down Expand Up @@ -515,7 +515,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
~> ( .K => #return 128 32
~> #pc [ STATICCALL ]
~> #execute )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -540,16 +540,16 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
CALLER_ID:Int
</caller>
<callData>
b"\xdf\xb7\xfe\xd0" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y )
b"\xdf\xb7\xfe\xd0" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int )
</callData>
<callValue>
0
</callValue>
<wordStack>
( 196 : ( selector ( "add(uint256,uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( ?KV1_y : ( ?KV0_x : ( 247 : ( selector ( "test_double_add(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) )
( 196 : ( selector ( "add(uint256,uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( ?KV1_y:Int : ( ?KV0_x:Int : ( 247 : ( selector ( "test_double_add(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) )
</wordStack>
<localMem>
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y )
b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int )
</localMem>
<memoryUsed>
0
Expand Down Expand Up @@ -665,7 +665,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 )
</caller>
<callData>
( b"\n\x92T\xe4" => b"w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) )
( b"\n\x92T\xe4" => b"w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) )
</callData>
<callValue>
0
Expand Down Expand Up @@ -910,10 +910,10 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))))
ensures ( 0 <=Int ?KV0_x
andBool ( 0 <=Int ?KV1_y
andBool ( ?KV0_x <Int pow256
andBool ( ?KV1_y <Int pow256
ensures ( 0 <=Int ?KV0_x:Int
andBool ( 0 <=Int ?KV1_y:Int
andBool ( ?KV0_x:Int <Int pow256
andBool ( ?KV1_y:Int <Int pow256
))))
[priority(20), label(BASIC-BLOCK-1-TO-7)]

Expand All @@ -924,7 +924,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
~> #return 128 32
~> #pc [ STATICCALL ]
~> #execute => #halt ~> .K )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -941,7 +941,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" )
</output>
<statusCode>
( _STATUSCODE => EVMC_REVERT )
( _STATUSCODE:StatusCode => EVMC_REVERT )
</statusCode>
<callStack>
( ListItem ( <callState>
Expand Down Expand Up @@ -1317,7 +1317,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
~> #return 128 32
~> #pc [ STATICCALL ]
~> #execute => #halt ~> .K )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -1334,7 +1334,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
b""
</output>
<statusCode>
( _STATUSCODE => EVMC_SUCCESS )
( _STATUSCODE:StatusCode => EVMC_SUCCESS )
</statusCode>
<callStack>
( ListItem ( <callState>
Expand Down Expand Up @@ -1711,7 +1711,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
~> #return 128 32
~> #pc [ STATICCALL ]
~> #execute => #halt ~> .K )
~> _CONTINUATION
~> _CONTINUATION:K
</k>
<mode>
NORMAL
Expand All @@ -1728,7 +1728,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" )
</output>
<statusCode>
( _STATUSCODE => EVMC_REVERT )
( _STATUSCODE:StatusCode => EVMC_REVERT )
</statusCode>
<callStack>
( ListItem ( <callState>
Expand Down
Loading

0 comments on commit dfb1a6f

Please sign in to comment.