From dfb1a6f0099931b6626a31a31aaa4f60f65d9955 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Mon, 27 Jan 2025 12:57:38 +0200 Subject: [PATCH] update expected output --- ...ramsTest.testDealConcrete().trace.expected | 6 +- .../AddConst.applyOp(uint256).cse.expected | 12 +- .../AddrTest.test_addr_true().trace.expected | 6 +- ...t_double_add(uint256,uint256).cse.expected | 34 +-- ...d_double_sub(uint256,uint256).cse.expected | 42 +-- ...rnal(uint256,uint256,uint256).cse.expected | 46 ++-- ...Contract.add(uint256,uint256).cse.expected | 12 +- ...rnal(uint256,uint256,uint256).cse.expected | 24 +- ...sertTest.checkFail_assert_false().expected | 20 +- ...AssertTest.testFail_assert_true().expected | 20 +- ...sertTest.testFail_expect_revert().expected | 44 +-- .../AssertTest.test_assert_false().expected | 20 +- .../AssertTest.test_assert_true().expected | 20 +- ...Test.test_failing_branch(uint256).expected | 36 +-- ...st_revert_branch(uint256,uint256).expected | 40 +-- ...ail_assume_false(uint256,uint256).expected | 26 +- ...Fail_assume_true(uint256,uint256).expected | 34 +-- ...est_assume_false(uint256,uint256).expected | 34 +-- .../show/BMCBoundTest.testBound().expected | 84 +++--- ...aramsTest.testWarp(uint256).trace.expected | 6 +- ...st_add_const(uint256,uint256).cse.expected | 22 +- ...est_identity(uint256,uint256).cse.expected | 22 +- ...CallableStorageContract.str().cse.expected | 12 +- ...allableStorageTest.test_str().cse.expected | 8 +- .../show/ConstructorTest.init.cse.expected | 6 +- ...ctorTest.test_contract_call().cse.expected | 4 +- ...ctFieldTest.testEscrowToken().cse.expected | 4 +- ...um.enum_argument_range(uint8).cse.expected | 6 +- .../Enum.enum_storage_range().cse.expected | 12 +- .../test-data/show/Enum.init.cse.expected | 6 +- ...chTest.test_forgetBranch(uint256).expected | 24 +- .../Identity.applyOp(uint256).cse.expected | 12 +- .../Identity.identity(uint256).cse.expected | 6 +- ...ImportedContract.add(uint256).cse.expected | 12 +- .../ImportedContract.count().cse.expected | 6 +- .../show/ImportedContract.init.cse.expected | 6 +- ...ImportedContract.set(uint256).cse.expected | 12 +- ...erfaceTagTest.testInterface().cse.expected | 4 +- ...RandomVarTest.test_custom_names().expected | 186 ++++++------- ...etUpDeployTest.test_extcodesize().expected | 20 +- ...aticCallContract.set(uint256).cse.expected | 6 +- ...e.getEscrowTokenTotalSupply().cse.expected | 18 +- .../test-data/show/gas-abstraction.expected | 14 +- .../test-data/show/merge-loop-heads.expected | 18 +- ...sertTest.testFail_expect_revert().expected | 10 +- .../AssertTest.test_assert_false().expected | 6 +- ...Test.test_failing_branch(uint256).expected | 22 +- ...st_revert_branch(uint256,uint256).expected | 26 +- ...ranch_merge(uint256,uint256,bool).expected | 42 +-- .../test-data/show/node-refutation.expected | 18 +- .../test-data/show/split-node.expected | 254 +++++++++--------- 51 files changed, 695 insertions(+), 695 deletions(-) diff --git a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected index 30ef0fb59..8ce6adf4e 100644 --- a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected +++ b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected @@ -33,7 +33,7 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -50,7 +50,7 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -304,7 +304,7 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0 andBool ( TIMESTAMP_CELL:Int ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -96,10 +96,10 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0 - ( _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 ) ) ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) @@ -261,7 +261,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -275,10 +275,10 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0 - ( _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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) diff --git a/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected b/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected index 3509a9af7..224231d75 100644 --- a/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected +++ b/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected @@ -34,7 +34,7 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,7 +51,7 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -264,7 +264,7 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0 andBool ( TIMESTAMP_CELL:Int #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -515,7 +515,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 ~> ( .K => #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -540,16 +540,16 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 CALLER_ID:Int - 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 ) 0 - ( 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 ) ) ) ) ) ) ) ) - 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 ) 0 @@ -665,7 +665,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 ( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 ) - ( 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 ) ) 0 @@ -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 #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -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 NORMAL @@ -1334,7 +1334,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( ListItem ( @@ -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 NORMAL @@ -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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( diff --git a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected index 6199594f2..c626a4c93 100644 --- a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected @@ -173,7 +173,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -190,7 +190,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ( 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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -564,7 +564,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ~> ( .K => #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -589,16 +589,16 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 CALLER_ID:Int - b"\xe1\xc3j\x8c" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) + b"\xe1\xc3j\x8c" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) 0 - ( 196 : ( selector ( "add(uint256,uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( ?KV1_y : ( ?KV0_x : ( 247 : ( selector ( "test_double_add_double_sub(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) + ( 196 : ( selector ( "add(uint256,uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( ?KV1_y:Int : ( ?KV0_x:Int : ( 247 : ( selector ( "test_double_add_double_sub(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) - 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 ) 0 @@ -714,7 +714,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 ) - ( 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 ) ) 0 @@ -959,10 +959,10 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 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 #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -990,7 +990,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ( 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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -1366,7 +1366,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1383,7 +1383,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ( 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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -1760,7 +1760,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1777,7 +1777,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ( 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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -2158,7 +2158,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2175,7 +2175,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( ListItem ( @@ -2558,7 +2558,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2575,7 +2575,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ( 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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( diff --git a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected index 4d632dbd9..e46057596 100644 --- a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected @@ -177,7 +177,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -194,7 +194,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ( 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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -570,7 +570,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -587,7 +587,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ( 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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -964,7 +964,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ~> ( .K => #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -989,16 +989,16 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT CALLER_ID:Int - b"\x922\xed\x8c" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) +Bytes #buf ( 32 , ?KV2_z ) + b"\x922\xed\x8c" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) +Bytes #buf ( 32 , ?KV2_z:Int ) 0 - ( 228 : ( selector ( "add_sub_external(uint256,uint256,uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( ?KV2_z : ( ?KV1_y : ( ?KV0_x : ( 247 : ( selector ( "test_double_add_sub_external(uint256,uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) + ( 228 : ( selector ( "add_sub_external(uint256,uint256,uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( ?KV2_z:Int : ( ?KV1_y:Int : ( ?KV0_x:Int : ( 247 : ( selector ( "test_double_add_sub_external(uint256,uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) - 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\x00\x9c&\xe07" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) +Bytes #buf ( 32 , ?KV2_z ) + 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\x00\x9c&\xe07" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) +Bytes #buf ( 32 , ?KV2_z:Int ) 0 @@ -1114,7 +1114,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 ) - ( b"\n\x92T\xe4" => b"\x9c&\xe07" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) +Bytes #buf ( 32 , ?KV2_z ) ) + ( b"\n\x92T\xe4" => b"\x9c&\xe07" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) +Bytes #buf ( 32 , ?KV2_z:Int ) ) 0 @@ -1359,12 +1359,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT 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 ( 0 <=Int ?KV2_z - andBool ( ?KV0_x #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1392,7 +1392,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ( 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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -1773,7 +1773,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1790,7 +1790,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ( 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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -2172,7 +2172,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2189,7 +2189,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( ListItem ( @@ -2572,7 +2572,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2589,7 +2589,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ( 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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( diff --git a/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected index 2907a5dc0..a197790ee 100644 --- a/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected @@ -82,7 +82,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -96,10 +96,10 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0 - ( _OUTPUT_CELL => #buf ( 32 , ( KV0_x:Int +Int KV1_y:Int ) ) ) + ( _OUTPUT_CELL:Bytes => #buf ( 32 , ( KV0_x:Int +Int KV1_y:Int ) ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) @@ -260,7 +260,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -274,10 +274,10 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0 - ( _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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) diff --git a/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected index f615ee2fe..c43cfb883 100644 --- a/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected @@ -151,7 +151,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -165,10 +165,10 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) @@ -337,7 +337,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -351,10 +351,10 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): - ( _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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( C_ARITHMETICCONTRACT_ID:Int ) ) @@ -527,7 +527,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -541,10 +541,10 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): - ( _OUTPUT_CELL => #buf ( 32 , ( ( KV0_x:Int +Int KV1_y:Int ) -Int KV2_z:Int ) ) ) + ( _OUTPUT_CELL:Bytes => #buf ( 32 , ( ( KV0_x:Int +Int KV1_y:Int ) -Int KV2_z:Int ) ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( C_ARITHMETICCONTRACT_ID:Int ) ) @@ -718,7 +718,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -732,10 +732,10 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): - ( _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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( C_ARITHMETICCONTRACT_ID:Int ) ) diff --git a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected index 0f4005130..b26bc102c 100644 --- a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected @@ -67,7 +67,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -84,7 +84,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -297,7 +297,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -326,7 +326,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -541,7 +541,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 andBool ( ORIGIN_ID:Int #end EVMC_REVERT ~> #pc [ REVERT ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -793,7 +793,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 ( #end EVMC_REVERT => #halt ) ~> #pc [ REVERT ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -810,7 +810,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 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" - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List @@ -1036,7 +1036,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 #halt ~> ( #pc [ REVERT ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected index cad3904ce..65ed17e16 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected @@ -313,7 +313,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -330,7 +330,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -543,7 +543,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -572,7 +572,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -787,7 +787,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 andBool ( ORIGIN_ID:Int #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1039,7 +1039,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 ( #end EVMC_SUCCESS => #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1056,7 +1056,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1282,7 +1282,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 #halt ~> ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected index c059452a2..0a01fc323 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected @@ -404,7 +404,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -421,7 +421,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -634,7 +634,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -663,7 +663,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -878,7 +878,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 andBool ( ORIGIN_ID:Int CALL 0 645326474426547203313410069153905908525362434349 0 128 4 128 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1133,7 +1133,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #return 128 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1379,7 +1379,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1540,10 +1540,10 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ( false => true ) - ( _EXPECTEDREASON_CELL => b"" ) + ( _EXPECTEDREASON_CELL:Bytes => b"" ) - ( _EXPECTEDDEPTH_CELL => 0 ) + ( _EXPECTEDDEPTH_CELL:Int => 0 ) @@ -1629,7 +1629,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1880,7 +1880,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2225,7 +2225,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2571,7 +2571,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2917,7 +2917,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2934,7 +2934,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 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" - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ListItem ( @@ -3266,7 +3266,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3618,7 +3618,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3970,7 +3970,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #updateRevertOutput 128 0 => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -4314,7 +4314,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ( #end EVMC_SUCCESS => #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -4562,7 +4562,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 #halt ~> ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected index e1d963a32..5b1b2aa09 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected @@ -310,7 +310,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -327,7 +327,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -540,7 +540,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -569,7 +569,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -784,7 +784,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 andBool ( ORIGIN_ID:Int #end EVMC_REVERT ~> #pc [ REVERT ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1036,7 +1036,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 ( #end EVMC_REVERT => #halt ) ~> #pc [ REVERT ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1053,7 +1053,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 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" - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List @@ -1279,7 +1279,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 #halt ~> ( #pc [ REVERT ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected index 60c34dd20..87272be20 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected +++ b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected @@ -70,7 +70,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -87,7 +87,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -300,7 +300,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -329,7 +329,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -544,7 +544,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 andBool ( ORIGIN_ID:Int #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -796,7 +796,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 ( #end EVMC_SUCCESS => #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -813,7 +813,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1039,7 +1039,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 #halt ~> ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL diff --git a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected index 91b8973a1..840b6226b 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected +++ b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected @@ -376,7 +376,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -393,7 +393,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -606,7 +606,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -635,7 +635,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -654,7 +654,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 CALLER_ID:Int - ( b"\n\x92T\xe4" => b"F\"\xb1U" +Bytes #buf ( 32 , ?KV0_x ) ) + ( b"\n\x92T\xe4" => b"F\"\xb1U" +Bytes #buf ( 32 , ?KV0_x:Int ) ) 0 @@ -850,12 +850,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 andBool ( ORIGIN_ID:Int JUMPI 1124 bool2Word ( 100 <=Int KV0_x:Int ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1108,7 +1108,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ~> #pc [ JUMPI ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1352,7 +1352,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ~> #pc [ JUMPI ] => #end EVMC_REVERT ~> #pc [ REVERT ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1595,7 +1595,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ( #end EVMC_SUCCESS => #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1612,7 +1612,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1841,7 +1841,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ( #end EVMC_REVERT => #halt ) ~> #pc [ REVERT ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1858,7 +1858,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 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" - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List @@ -2087,7 +2087,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 #halt ~> ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2333,7 +2333,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 #halt ~> ( #pc [ REVERT ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL diff --git a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected index 6b41bfd24..501b0437f 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected @@ -627,7 +627,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -644,7 +644,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -857,7 +857,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -886,7 +886,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -905,7 +905,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 CALLER_ID:Int - ( b"\n\x92T\xe4" => b"\x8c\x0e\xdd\x8b" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) ) + ( b"\n\x92T\xe4" => b"\x8c\x0e\xdd\x8b" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) ) 0 @@ -1101,14 +1101,14 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 andBool ( ORIGIN_ID:Int JUMPI 1594 bool2Word ( KV1_y:Int <=Int KV0_x:Int ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1363,7 +1363,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ~> #pc [ JUMPI ] => #end EVMC_REVERT ~> #pc [ REVERT ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1609,7 +1609,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ~> #pc [ JUMPI ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1854,7 +1854,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ( #end EVMC_REVERT => #halt ) ~> #pc [ REVERT ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1871,7 +1871,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 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" - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List @@ -2102,7 +2102,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ( #end EVMC_SUCCESS => #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2119,7 +2119,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -2350,7 +2350,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 #halt ~> ( #pc [ REVERT ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2598,7 +2598,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 #halt ~> ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected index 4e7c3f7ae..280fa7784 100644 --- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected @@ -317,7 +317,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 ( .K => STATICCALL 0 645326474426547203313410069153905908525362434349 128 36 128 0 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -546,7 +546,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 andBool ( TIMESTAMP_CELL:Int #return 128 0 ) ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -798,7 +798,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int #pc [ STATICCALL ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1047,7 +1047,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1077,7 +1077,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1282,7 +1282,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 - requires ( _KV0_a ==Int KV1_b:Int + requires ( _KV0_a:Int ==Int KV1_b:Int andBool ( 0 <=Int KV1_b:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -1295,7 +1295,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1529,7 +1529,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 - requires ( _KV0_a ==Int KV1_b:Int + requires ( _KV0_a:Int ==Int KV1_b:Int andBool ( 0 <=Int KV1_b:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -1542,7 +1542,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int STATICCALL 0 645326474426547203313410069153905908525362434349 128 36 128 0 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -323,7 +323,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( TIMESTAMP_CELL:Int #return 128 0 ) ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -575,7 +575,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( KV1_b:Int #return 128 0 ~> #pc [ STATICCALL ] => .K ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -823,7 +823,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( KV1_b:Int CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1070,7 +1070,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( KV1_b:Int #return 388 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1319,7 +1319,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( KV1_b:Int #pc [ CALL ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1569,7 +1569,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( KV1_b:Int #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1598,7 +1598,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1818,7 +1818,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( KV1_b:Int ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2067,7 +2067,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( KV1_b:Int STATICCALL 0 645326474426547203313410069153905908525362434349 128 36 128 0 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -572,7 +572,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( TIMESTAMP_CELL:Int #return 128 0 ) ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -824,7 +824,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int #return 128 0 ~> #pc [ STATICCALL ] => .K ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1072,7 +1072,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1319,7 +1319,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int #return 388 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1568,7 +1568,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int #pc [ CALL ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1818,7 +1818,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1847,7 +1847,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -2067,7 +2067,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2316,7 +2316,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int - ( .K => JUMPI 508 bool2Word ( ??WORD <=Int 0 ) + ( .K => JUMPI 508 bool2Word ( ??WORD:Int <=Int 0 ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -254,7 +254,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 - ( b"" => #buf ( 32 , ??WORD ) ) + ( b"" => #buf ( 32 , ??WORD:Int ) ) .List @@ -279,10 +279,10 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 0 - ( .WordStack => ( 0 : ( ??WORD : ( 220 : ( selector ( "setUp()" ) : .WordStack ) ) ) ) ) + ( .WordStack => ( 0 : ( ??WORD:Int : ( 220 : ( selector ( "setUp()" ) : .WordStack ) ) ) ) ) - ( b"" => 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\xa0\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" +Bytes #buf ( 32 , ??WORD ) +Bytes b"\x00\x00\x00 " ) + ( b"" => 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\xa0\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" +Bytes #buf ( 32 , ??WORD:Int ) +Bytes b"\x00\x00\x00 " ) 0 @@ -467,14 +467,14 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( TIMESTAMP_CELL:Int #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -501,7 +501,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ( #buf ( 32 , ?WORD:Int ) => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -719,7 +719,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -748,7 +748,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ( #buf ( 32 , ?WORD:Int ) => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -967,7 +967,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -996,7 +996,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ( #buf ( 32 , ?WORD:Int ) => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1216,7 +1216,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1245,7 +1245,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ( #buf ( 32 , ?WORD:Int ) => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1466,7 +1466,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int 4 ) ) ~> #pc [ JUMPI ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1713,7 +1713,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1740,7 +1740,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -1958,7 +1958,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1985,7 +1985,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -2204,7 +2204,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2231,7 +2231,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -2451,7 +2451,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2478,7 +2478,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -2699,7 +2699,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2726,7 +2726,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -2953,7 +2953,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2970,7 +2970,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -3198,7 +3198,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3215,7 +3215,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -3444,7 +3444,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3461,7 +3461,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List diff --git a/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected b/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected index cb918e8fe..1d41c4f6a 100644 --- a/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected +++ b/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected @@ -34,7 +34,7 @@ module SUMMARY-TEST%BLOCKPARAMSTEST.TESTWARP(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,7 +51,7 @@ module SUMMARY-TEST%BLOCKPARAMSTEST.TESTWARP(UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -265,7 +265,7 @@ module SUMMARY-TEST%BLOCKPARAMSTEST.TESTWARP(UINT256):0 andBool ( TIMESTAMP_CELL:Int #cheatcode_return 128 0 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -393,7 +393,7 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 ( JUMPI 678 bool2Word ( pow64 <=Int KV0_x:Int ) ~> #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -410,7 +410,7 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -708,10 +708,10 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 rule [BASIC-BLOCK-1-TO-9]: - ( .K => JUMPI 678 bool2Word ( pow64 <=Int ?KV0_x ) + ( .K => JUMPI 678 bool2Word ( pow64 <=Int ?KV0_x:Int ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -744,13 +744,13 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 CALLER_ID:Int - ( b"\n\x92T\xe4" => b"\x0f\xee)\xd1" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) ) + ( b"\n\x92T\xe4" => b"\x0f\xee)\xd1" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) ) 0 - ( .WordStack => ( bool2Word ( ?KV0_x ( bool2Word ( ?KV0_x:Int ( b"" => 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" ) @@ -1031,10 +1031,10 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(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 #cheatcode_return 128 0 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -389,7 +389,7 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 ( JUMPI 2519 bool2Word ( pow64 <=Int KV0_x:Int ) ~> #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -406,7 +406,7 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -702,10 +702,10 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 rule [BASIC-BLOCK-1-TO-9]: - ( .K => JUMPI 2519 bool2Word ( pow64 <=Int ?KV0_x ) + ( .K => JUMPI 2519 bool2Word ( pow64 <=Int ?KV0_x:Int ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -738,13 +738,13 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 CALLER_ID:Int - ( b"\n\x92T\xe4" => b"\xc0\xbd\x83$" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) ) + ( b"\n\x92T\xe4" => b"\xc0\xbd\x83$" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) ) 0 - ( .WordStack => ( bool2Word ( ?KV0_x ( bool2Word ( ?KV0_x:Int ( b"" => 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" ) @@ -1025,10 +1025,10 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(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 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -98,10 +98,10 @@ module SUMMARY-TEST%CALLABLESTORAGECONTRACT.STR():0 - ( _OUTPUT_CELL => 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" ) + ( _OUTPUT_CELL:Bytes => 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" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) @@ -266,7 +266,7 @@ module SUMMARY-TEST%CALLABLESTORAGECONTRACT.STR():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -280,10 +280,10 @@ module SUMMARY-TEST%CALLABLESTORAGECONTRACT.STR():0 - ( _OUTPUT_CELL => #range ( 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 " +Bytes #buf ( 32 , C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int ) +Bytes #range ( C_CALLABLESTORAGECONTRACT_STR_S_CONTENTS:Bytes , 0 , ( ( ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) +Int C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int ) +Int -32 ) ) +Bytes 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" , ( ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) +Int -32 ) , chop ( ( ( chop ( ( ( ( notMaxUInt5 &Int ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) ) +Int ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) ) +Int 224 ) ) -Int ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) ) +Int -160 ) ) ) ) + ( _OUTPUT_CELL:Bytes => #range ( 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 " +Bytes #buf ( 32 , C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int ) +Bytes #range ( C_CALLABLESTORAGECONTRACT_STR_S_CONTENTS:Bytes , 0 , ( ( ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) +Int C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int ) +Int -32 ) ) +Bytes 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" , ( ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) +Int -32 ) , chop ( ( ( chop ( ( ( ( notMaxUInt5 &Int ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) ) +Int ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) ) +Int 224 ) ) -Int ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) ) +Int -160 ) ) ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) diff --git a/src/tests/integration/test-data/show/CallableStorageTest.test_str().cse.expected b/src/tests/integration/test-data/show/CallableStorageTest.test_str().cse.expected index f919fac25..da90bd342 100644 --- a/src/tests/integration/test-data/show/CallableStorageTest.test_str().cse.expected +++ b/src/tests/integration/test-data/show/CallableStorageTest.test_str().cse.expected @@ -34,7 +34,7 @@ module SUMMARY-TEST%CALLABLESTORAGETEST.TEST-STR():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,7 +51,7 @@ module SUMMARY-TEST%CALLABLESTORAGETEST.TEST-STR():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -305,13 +305,13 @@ module SUMMARY-TEST%CALLABLESTORAGETEST.TEST-STR():0 andBool ( TIMESTAMP_CELL:Int ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -49,7 +49,7 @@ module SUMMARY-TEST%CONSTRUCTORTEST.INIT:0 ( b"" => b"`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x00\xeaW`\x005`\xe0\x1c\x80c\x92\xdfO\xbd\x11a\x00\x8cW\x80c\xe0\x18\x0b\x0b\x11a\x00fW\x80c\xe0\x18\x0b\x0b\x14a\x01\x81W\x80c\xe2\f\x9fq\x14a\x01\x89W\x80c\xe9\x9bk1\x14a\x01\x81W\x80c\xfav&\xd4\x14a\x01\x91W`\x00\x80\xfd[\x80c\x92\xdfO\xbd\x14a\x01YW\x80c\xb5P\x8a\xa9\x14a\x01aW\x80c\xbaAO\xa6\x14a\x01iW`\x00\x80\xfd[\x80c?r\x86\xf4\x11a\x00\xc8W\x80c?r\x86\xf4\x14a\x01\x1fW\x80cf\xd9\xa9\xa0\x14a\x01'W\x80c\x85\"l\x81\x14a\x01^<#\x14a\x01\x17W[`\x00\x80\xfd[a\x00\xf7a\x01\x9eV[`@Qa\x01\x04\x91\x90a\fvV[`@Q\x80\x91\x03\x90\xf3[a\x01\x15a\x02\x00V[\x00[a\x00\xf7a\x04IV[a\x00\xf7a\x04\xa9V[a\x01/a\x05\tV[`@Qa\x01\x04\x91\x90a\f\xc3V[a\x01Da\x05\xf8V[`@Qa\x01\x04\x91\x90a\r\xa6V[a\x01/a\x06\xc8V[a\x01\x15a\x07\xaeV[a\x01Da\x07\xc3V[a\x01qa\x08\x93V[`@Q\x90\x15\x15\x81R` \x01a\x01\x04V[a\x01\x15a\t\xc0V[a\x00\xf7a\t\xd2V[`\x07Ta\x01q\x90`\xff\x16\x81V[```\x14\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01\x82\x80T\x80\x15a\x01\xf6W` \x02\x82\x01\x91\x90`\x00R` `\x00 \x90[\x81T`\x01`\x01`\xa0\x1b\x03\x16\x81R`\x01\x90\x91\x01\x90` \x01\x80\x83\x11a\x01\xd8W[PPPPP\x90P\x90V[`\x1bT`\xff\x16a\x02\x12Wa\x02\x12a\x0e V[`\x00`@Qa\x02 \x90a\fiV[`@Q\x80\x91\x03\x90`\x00\xf0\x80\x15\x80\x15a\x02=`\x00\xfd[P`@Qc`\xfeG\xb1`\xe0\x1b\x81Ra\x158`\x04\x82\x01R\x90\x91P`\x01`\x01`\xa0\x1b\x03\x82\x16\x90c`\xfeG\xb1\x90`$\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x02\x83W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x02\x97W=`\x00\x80>=`\x00\xfd[PP`\x1bT`@Qc\x08\x01\xf1i`\xe1\x1b\x81R`\x03`\x04\x82\x01Ra\x01\x00\x90\x91\x04`\x01`\x01`\xa0\x1b\x03\x16\x92Pc\x10\x03\xe2\xd2\x91P`$\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x02\xe5W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x02\xf9W=`\x00\x80>=`\x00\xfd[PPPPa\x03\x7f`\x1b`\x01\x90T\x90a\x01\x00\n\x90\x04`\x01`\x01`\xa0\x1b\x03\x16`\x01`\x01`\xa0\x1b\x03\x16c\x06f\x1a\xbd`@Q\x81c\xff\xff\xff\xff\x16`\xe0\x1b\x81R`\x04\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x03SW=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x03w\x91\x90a\x0e6V[a\x10\xe4a\n2V[`@Qc\x08\x01\xf1i`\xe1\x1b\x81R`\x05`\x04\x82\x01R`\x01`\x01`\xa0\x1b\x03\x82\x16\x90c\x10\x03\xe2\xd2\x90`$\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x03\xc1W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x03\xd5W=`\x00\x80>=`\x00\xfd[PPPPa\x04F\x81`\x01`\x01`\xa0\x1b\x03\x16c\x06f\x1a\xbd`@Q\x81c\xff\xff\xff\xff\x16`\xe0\x1b\x81R`\x04\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x04\x1aW=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x04>\x91\x90a\x0e6V[a\x15=a\n2V[PV[```\x16\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01\x82\x80T\x80\x15a\x01\xf6W` \x02\x82\x01\x91\x90`\x00R` `\x00 \x90\x81T`\x01`\x01`\xa0\x1b\x03\x16\x81R`\x01\x90\x91\x01\x90` \x01\x80\x83\x11a\x01\xd8WPPPPP\x90P\x90V[```\x15\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01\x82\x80T\x80\x15a\x01\xf6W` \x02\x82\x01\x91\x90`\x00R` `\x00 \x90\x81T`\x01`\x01`\xa0\x1b\x03\x16\x81R`\x01\x90\x91\x01\x90` \x01\x80\x83\x11a\x01\xd8WPPPPP\x90P\x90V[```\x19\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01`\x00\x90[\x82\x82\x10\x15a\x05\xefW`\x00\x84\x81R` \x90\x81\x90 `@\x80Q\x80\x82\x01\x82R`\x02\x86\x02\x90\x92\x01\x80T`\x01`\x01`\xa0\x1b\x03\x16\x83R`\x01\x81\x01\x80T\x83Q\x81\x87\x02\x81\x01\x87\x01\x90\x94R\x80\x84R\x93\x94\x91\x93\x85\x83\x01\x93\x92\x83\x01\x82\x82\x80\x15a\x05\xd7W` \x02\x82\x01\x91\x90`\x00R` `\x00 \x90`\x00\x90[\x82\x82\x90T\x90a\x01\x00\n\x90\x04`\xe0\x1b`\x01`\x01`\xe0\x1b\x03\x19\x16\x81R` \x01\x90`\x04\x01\x90` \x82`\x03\x01\x04\x92\x83\x01\x92`\x01\x03\x82\x02\x91P\x80\x84\x11a\x05\x99W\x90P[PPPPP\x81RPP\x81R` \x01\x90`\x01\x01\x90a\x05-V[PPPP\x90P\x90V[```\x18\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01`\x00\x90[\x82\x82\x10\x15a\x05\xefW\x83\x82\x90`\x00R` `\x00 \x01\x80Ta\x06;\x90a\x0eOV[\x80`\x1f\x01` \x80\x91\x04\x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01\x82\x80Ta\x06g\x90a\x0eOV[\x80\x15a\x06\xb4W\x80`\x1f\x10a\x06\x89Wa\x01\x00\x80\x83T\x04\x02\x83R\x91` \x01\x91a\x06\xb4V[\x82\x01\x91\x90`\x00R` `\x00 \x90[\x81T\x81R\x90`\x01\x01\x90` \x01\x80\x83\x11a\x06\x97W\x82\x90\x03`\x1f\x16\x82\x01\x91[PPPPP\x81R` \x01\x90`\x01\x01\x90a\x06\x1cV[```\x1a\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01`\x00\x90[\x82\x82\x10\x15a\x05\xefW`\x00\x84\x81R` \x90\x81\x90 `@\x80Q\x80\x82\x01\x82R`\x02\x86\x02\x90\x92\x01\x80T`\x01`\x01`\xa0\x1b\x03\x16\x83R`\x01\x81\x01\x80T\x83Q\x81\x87\x02\x81\x01\x87\x01\x90\x94R\x80\x84R\x93\x94\x91\x93\x85\x83\x01\x93\x92\x83\x01\x82\x82\x80\x15a\x07\x96W` \x02\x82\x01\x91\x90`\x00R` `\x00 \x90`\x00\x90[\x82\x82\x90T\x90a\x01\x00\n\x90\x04`\xe0\x1b`\x01`\x01`\xe0\x1b\x03\x19\x16\x81R` \x01\x90`\x04\x01\x90` \x82`\x03\x01\x04\x92\x83\x01\x92`\x01\x03\x82\x02\x91P\x80\x84\x11a\x07XW\x90P[PPPPP\x81RPP\x81R` \x01\x90`\x01\x01\x90a\x06\xecV[`\x1bT`\xff\x16\x15a\x07\xc1Wa\x07\xc1a\x0e V[V[```\x17\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01`\x00\x90[\x82\x82\x10\x15a\x05\xefW\x83\x82\x90`\x00R` `\x00 \x01\x80Ta\x08\x06\x90a\x0eOV[\x80`\x1f\x01` \x80\x91\x04\x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01\x82\x80Ta\x082\x90a\x0eOV[\x80\x15a\x08\x7fW\x80`\x1f\x10a\x08TWa\x01\x00\x80\x83T\x04\x02\x83R\x91` \x01\x91a\x08\x7fV[\x82\x01\x91\x90`\x00R` `\x00 \x90[\x81T\x81R\x90`\x01\x01\x90` \x01\x80\x83\x11a\x08bW\x82\x90\x03`\x1f\x16\x82\x01\x91[PPPPP\x81R` \x01\x90`\x01\x01\x90a\x07\xe7V[`\x07T`\x00\x90a\x01\x00\x90\x04`\xff\x16\x15a\x08\xb5WP`\x07Ta\x01\x00\x90\x04`\xff\x16\x90V[`\x00sq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-;\x15a\t\xbbW`@\x80Qsq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-` \x82\x01\x81\x90Re\x19\x98Z[\x19Y`\xd2\x1b\x82\x84\x01R\x82Q\x80\x83\x03\x84\x01\x81R``\x83\x01\x90\x93R`\x00\x92\x90\x91a\tC\x91\x7ff\x7f\x9dp\xcaA\x1dp\xea\xd5\r\x8d\\\"\x07\r\xaf\xc3j\xd7_=\xcf^r7\xb2*\xde\x9a\xec\xc4\x91`\x80\x01a\x0e\x89V[`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\t]\x91a\x0e\xbaV[`\x00`@Q\x80\x83\x03\x81`\x00\x86Z\xf1\x91PP=\x80`\x00\x81\x14a\t\x9aW`@Q\x91P`\x1f\x19`?=\x01\x16\x82\x01`@R=\x82R=`\x00` \x84\x01>a\t\x9fV[``\x91P[P\x91PP\x80\x80` \x01\x90Q\x81\x01\x90a\t\xb7\x91\x90a\x0e\xd6V[\x91PP[\x91\x90PV[`\x1bT`\xff\x16a\x07\xc1Wa\x07\xc1a\x0e V[```\x13\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01\x82\x80T\x80\x15a\x01\xf6W` \x02\x82\x01\x91\x90`\x00R` `\x00 \x90\x81T`\x01`\x01`\xa0\x1b\x03\x16\x81R`\x01\x90\x91\x01\x90` \x01\x80\x83\x11a\x01\xd8WPPPPP\x90P\x90V[\x80\x82\x14a\x0bYW\x7fA0O\xac\xd92=u\xb1\x1b\xcd\xd6\t\xcb8\xef\xff\xfd\xb0W\x10\xf7\xca\xf0\xe9\xb1lm\x9dp\x9fP`@Qa\n\xa3\x90` \x80\x82R`\"\x90\x82\x01R\x7fError: a == b not satisfied [uin`@\x82\x01Rat]`\xf0\x1b``\x82\x01R`\x80\x01\x90V[`@Q\x80\x91\x03\x90\xa1`@\x80Q\x81\x81R`\n\x81\x83\x01Ri\x08\x08\x08\x08\x08\x08\x13\x19Y\x9d`\xb2\x1b``\x82\x01R` \x81\x01\x84\x90R\x90Q\x7f\xb2\xde/\xbe\x80\x1a\r\xf6\xc0\xcb\xdd\xfdD\x8b\xa3\xc4\x1dH\xa0@\xca5\xc5l\x81\x96\xef\x0f\xca\xe7!\xa8\x91\x81\x90\x03`\x80\x01\x90\xa1`@\x80Q\x81\x81R`\n\x81\x83\x01Ri\x08\x08\x08\x08\x08\x14\x9aY\xda\x1d`\xb2\x1b``\x82\x01R` \x81\x01\x83\x90R\x90Q\x7f\xb2\xde/\xbe\x80\x1a\r\xf6\xc0\xcb\xdd\xfdD\x8b\xa3\xc4\x1dH\xa0@\xca5\xc5l\x81\x96\xef\x0f\xca\xe7!\xa8\x91\x81\x90\x03`\x80\x01\x90\xa1a\x0bYa\x0b]V[PPV[sq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-;\x15a\fXW`@\x80Qsq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-` \x82\x01\x81\x90Re\x19\x98Z[\x19Y`\xd2\x1b\x92\x82\x01\x92\x90\x92R`\x01``\x82\x01R`\x00\x91\x90\x7fp\xca\x10\xbb\xd0\xdb\xfd\x90 \xa9\xf4\xb14\x02\xc1l\xb1 p^\r\x1c\n\xea\xb1\x0f\xa3S\xaeXo\xc4\x90`\x80\x01`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\x0b\xf7\x92\x91` \x01a\x0e\x89V[`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\f\x11\x91a\x0e\xbaV[`\x00`@Q\x80\x83\x03\x81`\x00\x86Z\xf1\x91PP=\x80`\x00\x81\x14a\fNW`@Q\x91P`\x1f\x19`?=\x01\x16\x82\x01`@R=\x82R=`\x00` \x84\x01>a\fSV[``\x91P[PPPP[`\x07\x80Ta\xff\x00\x19\x16a\x01\x00\x17\x90UV[a\x01\f\x80a\x0f\x00\x839\x01\x90V[` \x80\x82R\x82Q\x82\x82\x01\x81\x90R`\x00\x91\x90\x84\x82\x01\x90`@\x85\x01\x90\x84[\x81\x81\x10\x15a\f\xb7W\x83Q`\x01`\x01`\xa0\x1b\x03\x16\x83R\x92\x84\x01\x92\x91\x84\x01\x91`\x01\x01a\f\x92V[P\x90\x96\x95PPPPPPV[`\x00` \x80\x83\x01\x81\x84R\x80\x85Q\x80\x83R`@\x92P\x82\x86\x01\x91P\x82\x81`\x05\x1b\x87\x01\x01\x84\x88\x01`\x00\x80[\x84\x81\x10\x15a\rgW\x89\x84\x03`?\x19\x01\x86R\x82Q\x80Q`\x01`\x01`\xa0\x1b\x03\x16\x85R\x88\x01Q\x88\x85\x01\x88\x90R\x80Q\x88\x86\x01\x81\x90R\x90\x89\x01\x90\x83\x90``\x87\x01\x90[\x80\x83\x10\x15a\rRW\x83Q`\x01`\x01`\xe0\x1b\x03\x19\x16\x82R\x92\x8b\x01\x92`\x01\x92\x90\x92\x01\x91\x90\x8b\x01\x90a\r(V[P\x97\x8a\x01\x97\x95PPP\x91\x87\x01\x91`\x01\x01a\f\xebV[P\x91\x99\x98PPPPPPPPPV[`\x00[\x83\x81\x10\x15a\r\x91W\x81\x81\x01Q\x83\x82\x01R` \x01a\ryV[\x83\x81\x11\x15a\r\xa0W`\x00\x84\x84\x01R[PPPPV[`\x00` \x80\x83\x01\x81\x84R\x80\x85Q\x80\x83R`@\x86\x01\x91P`@\x81`\x05\x1b\x87\x01\x01\x92P\x83\x87\x01`\x00[\x82\x81\x10\x15a\x0e\x13W\x87\x85\x03`?\x19\x01\x84R\x81Q\x80Q\x80\x87Ra\r\xf4\x81\x89\x89\x01\x8a\x85\x01a\rvV[`\x1f\x01`\x1f\x19\x16\x95\x90\x95\x01\x86\x01\x94P\x92\x85\x01\x92\x90\x85\x01\x90`\x01\x01a\r\xcdV[P\x92\x97\x96PPPPPPPV[cNH{q`\xe0\x1b`\x00R`\x01`\x04R`$`\x00\xfd[`\x00` \x82\x84\x03\x12\x15a\x0eHW`\x00\x80\xfd[PQ\x91\x90PV[`\x01\x81\x81\x1c\x90\x82\x16\x80a\x0ecW`\x7f\x82\x16\x91P[` \x82\x10\x81\x03a\x0e\x83WcNH{q`\xe0\x1b`\x00R`\"`\x04R`$`\x00\xfd[P\x91\x90PV[`\x01`\x01`\xe0\x1b\x03\x19\x83\x16\x81R\x81Q`\x00\x90a\x0e\xac\x81`\x04\x85\x01` \x87\x01a\rvV[\x91\x90\x91\x01`\x04\x01\x93\x92PPPV[`\x00\x82Qa\x0e\xcc\x81\x84` \x87\x01a\rvV[\x91\x90\x91\x01\x92\x91PPV[`\x00` \x82\x84\x03\x12\x15a\x0e\xe8W`\x00\x80\xfd[\x81Q\x80\x15\x15\x81\x14a\x0e\xf8W`\x00\x80\xfd[\x93\x92PPPV\xfe`\x80`@R`\x05`\x00U`\xf5\x80a\x00\x17`\x009`\x00\xf3\xfe`\x80`@R`\x046\x10`0W`\x005`\xe0\x1c\x80c\x06f\x1a\xbd\x14`5W\x80c\x10\x03\xe2\xd2\x14`[W\x80c`\xfeG\xb1\x14`lW[`\x00\x80\xfd[4\x80\x15`@W`\x00\x80\xfd[P`I`\x00T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`j`f6`\x04`\xabV[`\x87V[\x00[4\x80\x15`wW`\x00\x80\xfd[P`j`\x836`\x04`\xabV[`\x99V[\x80`\x00T`\x93\x91\x90`\xc3V[`\x00UPV[`\x03`\x00T\x10\x15`\xa6WPV[`\x00UV[`\x00` \x82\x84\x03\x12\x15`\xbcW`\x00\x80\xfd[P5\x91\x90PV[`\x00\x82\x19\x82\x11\x15`\xe3WcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa1dsolcC\x00\x08\r\x00\n\xa1dsolcC\x00\x08\r\x00\n" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -305,7 +305,7 @@ module SUMMARY-TEST%CONSTRUCTORTEST.INIT:0 andBool ( TIMESTAMP_CELL:Int ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,7 +51,7 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List diff --git a/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected index eea594a44..c5f847603 100644 --- a/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected +++ b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected @@ -34,7 +34,7 @@ module SUMMARY-TEST%CONTRACTFIELDTEST.TESTESCROWTOKEN():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,7 +51,7 @@ module SUMMARY-TEST%CONTRACTFIELDTEST.TESTESCROWTOKEN():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List diff --git a/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected b/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected index dd61dfb39..457f40149 100644 --- a/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected +++ b/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected @@ -42,7 +42,7 @@ module SUMMARY-TEST%ENUM.ENUM-ARGUMENT-RANGE(UINT8):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -56,10 +56,10 @@ module SUMMARY-TEST%ENUM.ENUM-ARGUMENT-RANGE(UINT8):0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) diff --git a/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected b/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected index f6de1631b..be30d1984 100644 --- a/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected +++ b/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected @@ -92,7 +92,7 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -106,10 +106,10 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( C_ENUM_ID:Int ) |Set SetItem ( C_ENUM_MEMBER_CONTRACT_ID:Int ) ) @@ -308,7 +308,7 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -322,10 +322,10 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) diff --git a/src/tests/integration/test-data/show/Enum.init.cse.expected b/src/tests/integration/test-data/show/Enum.init.cse.expected index 3ef942a8f..f9d23f769 100644 --- a/src/tests/integration/test-data/show/Enum.init.cse.expected +++ b/src/tests/integration/test-data/show/Enum.init.cse.expected @@ -33,7 +33,7 @@ module SUMMARY-TEST%ENUM.INIT:0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -47,10 +47,10 @@ module SUMMARY-TEST%ENUM.INIT:0 - ( _OUTPUT_CELL => b"`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x006W`\x005`\xe0\x1c\x80cc6\xf6\x1e\x14a\x00;W\x80c\x84|7\xfb\x14a\x00EW[`\x00\x80\xfd[a\x00Ca\x00XV[\x00[a\x00Ca\x00S6`\x04a\x01\xd2V[a\x01~V[`\x00T`@\x80Qch\xaf7\xdf`\xe0\x1b\x81R\x90Q`\x05\x92`\x01`\x01`\xa0\x1b\x03\x16\x91ch\xaf7\xdf\x91`\x04\x80\x83\x01\x92` \x92\x91\x90\x82\x90\x03\x01\x81\x86Z\xfa\x15\x80\x15a\x00\xa2W=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x00\xc6\x91\x90a\x01\xf6V[`\x05\x81\x11\x15a\x00\xd7Wa\x00\xd7a\x02\x13V[\x11\x15a\x00\xe5Wa\x00\xe5a\x02)V[`\x00\x80`\x00\x90T\x90a\x01\x00\n\x90\x04`\x01`\x01`\xa0\x1b\x03\x16`\x01`\x01`\xa0\x1b\x03\x16ch\xaf7\xdf`@Q\x81c\xff\xff\xff\xff\x16`\xe0\x1b\x81R`\x04\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x019W=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x01]\x91\x90a\x01\xf6V[`\x05\x81\x11\x15a\x01nWa\x01na\x02\x13V[\x10\x15a\x01|Wa\x01|a\x02)V[V[`\x05\x81`\x05\x81\x11\x15a\x01\x92Wa\x01\x92a\x02\x13V[\x11\x15a\x01\xa0Wa\x01\xa0a\x02)V[`\x00\x81`\x05\x81\x11\x15a\x01\xb4Wa\x01\xb4a\x02\x13V[\x10\x15a\x01\xc2Wa\x01\xc2a\x02)V[PV[`\x06\x81\x10a\x01\xc2W`\x00\x80\xfd[`\x00` \x82\x84\x03\x12\x15a\x01\xe4W`\x00\x80\xfd[\x815a\x01\xef\x81a\x01\xc5V[\x93\x92PPPV[`\x00` \x82\x84\x03\x12\x15a\x02\x08W`\x00\x80\xfd[\x81Qa\x01\xef\x81a\x01\xc5V[cNH{q`\xe0\x1b`\x00R`!`\x04R`$`\x00\xfd[cNH{q`\xe0\x1b`\x00R`\x01`\x04R`$`\x00\xfd\xfe\xa1dsolcC\x00\x08\r\x00\n" ) + ( _OUTPUT_CELL:Bytes => b"`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x006W`\x005`\xe0\x1c\x80cc6\xf6\x1e\x14a\x00;W\x80c\x84|7\xfb\x14a\x00EW[`\x00\x80\xfd[a\x00Ca\x00XV[\x00[a\x00Ca\x00S6`\x04a\x01\xd2V[a\x01~V[`\x00T`@\x80Qch\xaf7\xdf`\xe0\x1b\x81R\x90Q`\x05\x92`\x01`\x01`\xa0\x1b\x03\x16\x91ch\xaf7\xdf\x91`\x04\x80\x83\x01\x92` \x92\x91\x90\x82\x90\x03\x01\x81\x86Z\xfa\x15\x80\x15a\x00\xa2W=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x00\xc6\x91\x90a\x01\xf6V[`\x05\x81\x11\x15a\x00\xd7Wa\x00\xd7a\x02\x13V[\x11\x15a\x00\xe5Wa\x00\xe5a\x02)V[`\x00\x80`\x00\x90T\x90a\x01\x00\n\x90\x04`\x01`\x01`\xa0\x1b\x03\x16`\x01`\x01`\xa0\x1b\x03\x16ch\xaf7\xdf`@Q\x81c\xff\xff\xff\xff\x16`\xe0\x1b\x81R`\x04\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x019W=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x01]\x91\x90a\x01\xf6V[`\x05\x81\x11\x15a\x01nWa\x01na\x02\x13V[\x10\x15a\x01|Wa\x01|a\x02)V[V[`\x05\x81`\x05\x81\x11\x15a\x01\x92Wa\x01\x92a\x02\x13V[\x11\x15a\x01\xa0Wa\x01\xa0a\x02)V[`\x00\x81`\x05\x81\x11\x15a\x01\xb4Wa\x01\xb4a\x02\x13V[\x10\x15a\x01\xc2Wa\x01\xc2a\x02)V[PV[`\x06\x81\x10a\x01\xc2W`\x00\x80\xfd[`\x00` \x82\x84\x03\x12\x15a\x01\xe4W`\x00\x80\xfd[\x815a\x01\xef\x81a\x01\xc5V[\x93\x92PPPV[`\x00` \x82\x84\x03\x12\x15a\x02\x08W`\x00\x80\xfd[\x81Qa\x01\xef\x81a\x01\xc5V[cNH{q`\xe0\x1b`\x00R`!`\x04R`$`\x00\xfd[cNH{q`\xe0\x1b`\x00R`\x01`\x04R`$`\x00\xfd\xfe\xa1dsolcC\x00\x08\r\x00\n" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) diff --git a/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected b/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected index aec40fd4a..cc93e77bf 100644 --- a/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected +++ b/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected @@ -106,7 +106,7 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0 ~> #cheatcode_return 128 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -334,7 +334,7 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0 andBool ( TIMESTAMP_CELL:Int #cheatcode_return 128 0 ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -583,7 +583,7 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0 andBool ( KV0_x:Int #pc [ CALL ] => JUMPI 1326 bool2Word ( KV0_x:Int <=Int 200 ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -827,7 +827,7 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0 andBool ( KV0_x:Int #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -856,7 +856,7 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1074,7 +1074,7 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0 andBool ( KV0_x:Int #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1103,7 +1103,7 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1321,7 +1321,7 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0 andBool ( KV0_x:Int ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -96,10 +96,10 @@ module SUMMARY-SRC%CSE%IDENTITY.APPLYOP(UINT256):0 - ( _OUTPUT_CELL => #buf ( 32 , KV0_x:Int ) ) + ( _OUTPUT_CELL:Bytes => #buf ( 32 , KV0_x:Int ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( C_IDENTITY_ID:Int ) ) @@ -267,7 +267,7 @@ module SUMMARY-SRC%CSE%IDENTITY.APPLYOP(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -281,10 +281,10 @@ module SUMMARY-SRC%CSE%IDENTITY.APPLYOP(UINT256):0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) diff --git a/src/tests/integration/test-data/show/Identity.identity(uint256).cse.expected b/src/tests/integration/test-data/show/Identity.identity(uint256).cse.expected index b46893d41..e22911dcd 100644 --- a/src/tests/integration/test-data/show/Identity.identity(uint256).cse.expected +++ b/src/tests/integration/test-data/show/Identity.identity(uint256).cse.expected @@ -37,7 +37,7 @@ module SUMMARY-SRC%CSE%IDENTITY.IDENTITY(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,10 +51,10 @@ module SUMMARY-SRC%CSE%IDENTITY.IDENTITY(UINT256):0 - ( _OUTPUT_CELL => #buf ( 32 , KV0_x:Int ) ) + ( _OUTPUT_CELL:Bytes => #buf ( 32 , KV0_x:Int ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) diff --git a/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected b/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected index c510e14da..38800ad8e 100644 --- a/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected +++ b/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected @@ -82,7 +82,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -96,10 +96,10 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) @@ -266,7 +266,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -280,10 +280,10 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0 - ( _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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) diff --git a/src/tests/integration/test-data/show/ImportedContract.count().cse.expected b/src/tests/integration/test-data/show/ImportedContract.count().cse.expected index f75a11a5a..5ff629d20 100644 --- a/src/tests/integration/test-data/show/ImportedContract.count().cse.expected +++ b/src/tests/integration/test-data/show/ImportedContract.count().cse.expected @@ -37,7 +37,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.COUNT():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,10 +51,10 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.COUNT():0 - ( _OUTPUT_CELL => #buf ( 32 , #lookup ( C_IMPORTEDCONTRACT_STORAGE:Map , 0 ) ) ) + ( _OUTPUT_CELL:Bytes => #buf ( 32 , #lookup ( C_IMPORTEDCONTRACT_STORAGE:Map , 0 ) ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) diff --git a/src/tests/integration/test-data/show/ImportedContract.init.cse.expected b/src/tests/integration/test-data/show/ImportedContract.init.cse.expected index ed1f0e86c..33ba21ca1 100644 --- a/src/tests/integration/test-data/show/ImportedContract.init.cse.expected +++ b/src/tests/integration/test-data/show/ImportedContract.init.cse.expected @@ -35,7 +35,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.INIT:0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -49,10 +49,10 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.INIT:0 - ( _OUTPUT_CELL => b"`\x80`@R`\x046\x10`0W`\x005`\xe0\x1c\x80c\x06f\x1a\xbd\x14`5W\x80c\x10\x03\xe2\xd2\x14`[W\x80c`\xfeG\xb1\x14`lW[`\x00\x80\xfd[4\x80\x15`@W`\x00\x80\xfd[P`I`\x00T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`j`f6`\x04`\xabV[`\x87V[\x00[4\x80\x15`wW`\x00\x80\xfd[P`j`\x836`\x04`\xabV[`\x99V[\x80`\x00T`\x93\x91\x90`\xc3V[`\x00UPV[`\x03`\x00T\x10\x15`\xa6WPV[`\x00UV[`\x00` \x82\x84\x03\x12\x15`\xbcW`\x00\x80\xfd[P5\x91\x90PV[`\x00\x82\x19\x82\x11\x15`\xe3WcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa1dsolcC\x00\x08\r\x00\n" ) + ( _OUTPUT_CELL:Bytes => b"`\x80`@R`\x046\x10`0W`\x005`\xe0\x1c\x80c\x06f\x1a\xbd\x14`5W\x80c\x10\x03\xe2\xd2\x14`[W\x80c`\xfeG\xb1\x14`lW[`\x00\x80\xfd[4\x80\x15`@W`\x00\x80\xfd[P`I`\x00T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`j`f6`\x04`\xabV[`\x87V[\x00[4\x80\x15`wW`\x00\x80\xfd[P`j`\x836`\x04`\xabV[`\x99V[\x80`\x00T`\x93\x91\x90`\xc3V[`\x00UPV[`\x03`\x00T\x10\x15`\xa6WPV[`\x00UV[`\x00` \x82\x84\x03\x12\x15`\xbcW`\x00\x80\xfd[P5\x91\x90PV[`\x00\x82\x19\x82\x11\x15`\xe3WcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa1dsolcC\x00\x08\r\x00\n" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) diff --git a/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected b/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected index a03695b29..b64266145 100644 --- a/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected +++ b/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected @@ -82,7 +82,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -96,10 +96,10 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) @@ -264,7 +264,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -278,10 +278,10 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) diff --git a/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected b/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected index 3017ecff3..8acabefa5 100644 --- a/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected +++ b/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected @@ -34,7 +34,7 @@ module SUMMARY-TEST%INTERFACETAGTEST.TESTINTERFACE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,7 +51,7 @@ module SUMMARY-TEST%INTERFACETAGTEST.TESTINTERFACE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List diff --git a/src/tests/integration/test-data/show/RandomVarTest.test_custom_names().expected b/src/tests/integration/test-data/show/RandomVarTest.test_custom_names().expected index e5eb08823..5003ca484 100644 --- a/src/tests/integration/test-data/show/RandomVarTest.test_custom_names().expected +++ b/src/tests/integration/test-data/show/RandomVarTest.test_custom_names().expected @@ -160,11 +160,11 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 rule [BASIC-BLOCK-1-TO-3]: - ( .K => #rename ( ??WORD , "BOOLEAN" ) + ( .K => #rename ( ??WORD:Int , "BOOLEAN" ) ~> #cheatcode_return 128 32 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -178,7 +178,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - ( b"" => #buf ( 32 , ??WORD ) ) + ( b"" => #buf ( 32 , ??WORD:Int ) ) .List @@ -391,14 +391,14 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( TIMESTAMP_CELL:Int #cheatcode_return 128 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -423,7 +423,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - #buf ( 32 , ( ?WORD:Int => ?BOOLEAN ) ) + #buf ( 32 , ( ?WORD:Int => ?BOOLEAN:Int ) ) .List @@ -640,23 +640,23 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int - ( #cheatcode_return 128 32 ~> .K => #rename ( ??WORD , "BOOLEAN" ) + ( #cheatcode_return 128 32 ~> .K => #rename ( ??WORD:Int , "BOOLEAN" ) ~> #cheatcode_return 160 32 ) ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -670,7 +670,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - #buf ( 32 , ( BOOLEAN:Int => ??WORD ) ) + #buf ( 32 , ( BOOLEAN:Int => ??WORD:Int ) ) .List @@ -887,12 +887,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int #cheatcode_return 160 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -917,7 +917,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - #buf ( 32 , ( ?WORD:Int => ?BOOLEAN_0 ) ) + #buf ( 32 , ( ?WORD:Int => ?BOOLEAN_0:Int ) ) .List @@ -1136,12 +1136,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int #pc [ STATICCALL ] => .K ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1384,7 +1384,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int - ( .K => #rename ( ??WORD , "NEW_SLOT" ) + ( .K => #rename ( ??WORD:Int , "NEW_SLOT" ) ~> #cheatcode_return 256 32 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1414,7 +1414,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - ( b"" => #buf ( 32 , ??WORD ) ) + ( b"" => #buf ( 32 , ??WORD:Int ) ) .List @@ -1619,8 +1619,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #cheatcode_return 256 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1661,7 +1661,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - #buf ( 32 , ( ?WORD:Int => ?NEW_SLOT ) ) + #buf ( 32 , ( ?WORD:Int => ?NEW_SLOT:Int ) ) .List @@ -1866,8 +1866,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int ?WORD:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -1880,23 +1880,23 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ?WORD:Int - ( #cheatcode_return 256 32 ~> .K => #rename ( ??WORD , "NEW_ACCOUNT" ) + ( #cheatcode_return 256 32 ~> .K => #rename ( ??WORD:Int , "NEW_ACCOUNT" ) ~> #cheatcode_return 288 32 ) ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1910,7 +1910,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - #buf ( 32 , ( NEW_SLOT:Int => ??WORD ) ) + #buf ( 32 , ( NEW_SLOT:Int => ??WORD:Int ) ) .List @@ -2115,8 +2115,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -2129,14 +2129,14 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( NEW_SLOT:Int #cheatcode_return 288 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2161,7 +2161,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - #buf ( 32 , ( ?WORD:Int => ?NEW_ACCOUNT ) ) + #buf ( 32 , ( ?WORD:Int => ?NEW_ACCOUNT:Int ) ) .List @@ -2366,8 +2366,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int ?WORD:Int andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int @@ -2384,14 +2384,14 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ?WORD:Int =/=Int 728815563385977040452943777879061427756277306518 andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349 - andBool ( _C_RANDOMVARTEST_ID =/=Int 645326474426547203313410069153905908525362434349 + andBool ( _C_RANDOMVARTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ))))))))))))))))))))) - ensures ( 0 <=Int ?NEW_ACCOUNT - andBool ( ?NEW_ACCOUNT ( #cheatcode_return 288 32 - ~> #pc [ STATICCALL ] => #rename ( ??STORAGE , "NEW_ACCOUNT_STORAGE" ) + ~> #pc [ STATICCALL ] => #rename ( ??STORAGE:Map , "NEW_ACCOUNT_STORAGE" ) ~> #cheatcode_return 320 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2568,10 +2568,10 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 0 - ??STORAGE + ??STORAGE:Map - ??STORAGE + ??STORAGE:Map .Map @@ -2663,8 +2663,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -2681,7 +2681,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 728815563385977040452943777879061427756277306518 - andBool ( _C_RANDOMVARTEST_ID =/=Int 645326474426547203313410069153905908525362434349 + andBool ( _C_RANDOMVARTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ))))))))))))))))))))) @@ -2694,7 +2694,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 ~> #cheatcode_return 320 0 ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2839,10 +2839,10 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 0 - ( ?STORAGE:Map => ?NEW_ACCOUNT_STORAGE ) + ( ?STORAGE:Map => ?NEW_ACCOUNT_STORAGE:Map ) - ( ?STORAGE:Map => ?NEW_ACCOUNT_STORAGE ) + ( ?STORAGE:Map => ?NEW_ACCOUNT_STORAGE:Map ) .Map @@ -2934,8 +2934,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -2952,7 +2952,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 728815563385977040452943777879061427756277306518 - andBool ( _C_RANDOMVARTEST_ID =/=Int 645326474426547203313410069153905908525362434349 + andBool ( _C_RANDOMVARTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ))))))))))))))))))))) @@ -2962,11 +2962,11 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 ( #cheatcode_return 320 0 - ~> #pc [ CALL ] => #rename ( ??BYTES , "NEW_BYTES" ) + ~> #pc [ CALL ] => #rename ( ??BYTES:Bytes , "NEW_BYTES" ) ~> #cheatcode_return 320 0 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2980,7 +2980,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - ( b"" => 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 " +Bytes ??BYTES ) + ( b"" => 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 " +Bytes ??BYTES:Bytes ) .List @@ -3206,8 +3206,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -3224,11 +3224,11 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 728815563385977040452943777879061427756277306518 - andBool ( _C_RANDOMVARTEST_ID =/=Int 645326474426547203313410069153905908525362434349 + andBool ( _C_RANDOMVARTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ))))))))))))))))))))) - ensures 32 ==Int lengthBytes ( ??BYTES ) + ensures 32 ==Int lengthBytes ( ??BYTES:Bytes ) [priority(20), label(BASIC-BLOCK-13-TO-14)] rule [BASIC-BLOCK-14-TO-15]: @@ -3238,7 +3238,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 ~> #cheatcode_return 320 0 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3252,7 +3252,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - 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 " +Bytes ( ?BYTES:Bytes => ?NEW_BYTES ) + 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 " +Bytes ( ?BYTES:Bytes => ?NEW_BYTES:Bytes ) .List @@ -3478,8 +3478,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -3497,11 +3497,11 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 728815563385977040452943777879061427756277306518 - andBool ( _C_RANDOMVARTEST_ID =/=Int 645326474426547203313410069153905908525362434349 + andBool ( _C_RANDOMVARTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))))))))))))) - ensures 32 ==Int lengthBytes ( ?NEW_BYTES ) + ensures 32 ==Int lengthBytes ( ?NEW_BYTES:Bytes ) [priority(20), label(BASIC-BLOCK-14-TO-15)] rule [BASIC-BLOCK-15-TO-16]: @@ -3511,7 +3511,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 ~> #pc [ STATICCALL ] => POP 1 ~> #pc [ POP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3751,8 +3751,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -3770,7 +3770,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 728815563385977040452943777879061427756277306518 - andBool ( _C_RANDOMVARTEST_ID =/=Int 645326474426547203313410069153905908525362434349 + andBool ( _C_RANDOMVARTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))))))))))))) @@ -3782,7 +3782,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 ( POP 1 ~> #pc [ POP ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3799,7 +3799,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -4025,8 +4025,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -4044,7 +4044,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 728815563385977040452943777879061427756277306518 - andBool ( _C_RANDOMVARTEST_ID =/=Int 645326474426547203313410069153905908525362434349 + andBool ( _C_RANDOMVARTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))))))))))))) diff --git a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected index 74e0c344d..31410769a 100644 --- a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected +++ b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected @@ -70,7 +70,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -87,7 +87,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -341,7 +341,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -370,7 +370,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -606,7 +606,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 andBool ( ORIGIN_ID:Int #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -879,7 +879,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 ( #end EVMC_SUCCESS => #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -896,7 +896,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1143,7 +1143,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 #halt ~> ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL diff --git a/src/tests/integration/test-data/show/StaticCallContract.set(uint256).cse.expected b/src/tests/integration/test-data/show/StaticCallContract.set(uint256).cse.expected index ea7f161c6..74936941a 100644 --- a/src/tests/integration/test-data/show/StaticCallContract.set(uint256).cse.expected +++ b/src/tests/integration/test-data/show/StaticCallContract.set(uint256).cse.expected @@ -37,7 +37,7 @@ module SUMMARY-TEST%STATICCALLCONTRACT.SET(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,10 +51,10 @@ module SUMMARY-TEST%STATICCALLCONTRACT.SET(UINT256):0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) diff --git a/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected b/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected index a869046be..ebc024faa 100644 --- a/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected +++ b/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected @@ -149,7 +149,7 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -163,10 +163,10 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) @@ -393,7 +393,7 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -407,10 +407,10 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 - ( _OUTPUT_CELL => #buf ( 32 , ( #asWord ( #range ( #buf ( 32 , #lookup ( C_TGOVERNANCE_ESCROW_TOKEN_STORAGE:Map , 0 ) ) , 16 , 16 ) ) +Int 45 ) ) ) + ( _OUTPUT_CELL:Bytes => #buf ( 32 , ( #asWord ( #range ( #buf ( 32 , #lookup ( C_TGOVERNANCE_ESCROW_TOKEN_STORAGE:Map , 0 ) ) , 16 , 16 ) ) +Int 45 ) ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( C_TGOVERNANCE_ID:Int ) |Set SetItem ( C_TGOVERNANCE_ESCROW_ID:Int ) |Set SetItem ( C_TGOVERNANCE_ESCROW_TOKEN_ID:Int ) ) @@ -644,7 +644,7 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -658,10 +658,10 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( C_TGOVERNANCE_ID:Int ) |Set SetItem ( C_TGOVERNANCE_ESCROW_ID:Int ) ) diff --git a/src/tests/integration/test-data/show/gas-abstraction.expected b/src/tests/integration/test-data/show/gas-abstraction.expected index 1822c744d..82e14cbe8 100644 --- a/src/tests/integration/test-data/show/gas-abstraction.expected +++ b/src/tests/integration/test-data/show/gas-abstraction.expected @@ -421,7 +421,7 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 ( .K => #end EVMC_REVERT ~> #pc [ REVERT ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -642,7 +642,7 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 andBool ( TIMESTAMP_CELL:Int #halt ) ~> #pc [ REVERT ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -673,7 +673,7 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 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" - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List @@ -882,7 +882,7 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 andBool ( ORIGIN_ID:Int ( #pc [ REVERT ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1120,7 +1120,7 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 andBool ( ORIGIN_ID:Int JUMPI 1478 bool2Word ( KV0_n:Int <=Int 0 ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1191,7 +1191,7 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 andBool ( TIMESTAMP_CELL:Int 1 ) ) ~> #pc [ JUMPI ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1438,7 +1438,7 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 andBool ( KV0_n:Int 2 ) ) ~> #pc [ JUMPI ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1683,7 +1683,7 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 andBool ( KV0_n:Int 3 ) ) ~> #pc [ JUMPI ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1929,7 +1929,7 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 andBool ( KV0_n:Int #pc [ JUMPI ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.testFail_expect_revert().expected b/src/tests/integration/test-data/show/minimized/AssertTest.testFail_expect_revert().expected index 131248867..95193f315 100644 --- a/src/tests/integration/test-data/show/minimized/AssertTest.testFail_expect_revert().expected +++ b/src/tests/integration/test-data/show/minimized/AssertTest.testFail_expect_revert().expected @@ -282,7 +282,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -299,7 +299,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -446,10 +446,10 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false - ( _EXPECTEDREASON_CELL => b"" ) + ( _EXPECTEDREASON_CELL:Bytes => b"" ) - ( _EXPECTEDDEPTH_CELL => 0 ) + ( _EXPECTEDDEPTH_CELL:Int => 0 ) @@ -517,7 +517,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 andBool ( TIMESTAMP_CELL:Int ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -293,7 +293,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List @@ -506,7 +506,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 andBool ( TIMESTAMP_CELL:Int - ( .K => JUMPI 1124 bool2Word ( 100 <=Int ?KV0_x ) + ( .K => JUMPI 1124 bool2Word ( 100 <=Int ?KV0_x:Int ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -359,13 +359,13 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 CALLER_ID:Int - ( b"\n\x92T\xe4" => b"F\"\xb1U" +Bytes #buf ( 32 , ?KV0_x ) ) + ( b"\n\x92T\xe4" => b"F\"\xb1U" +Bytes #buf ( 32 , ?KV0_x:Int ) ) 0 - ( .WordStack => ( ?KV0_x : ( 327 : ( selector ( "test_failing_branch(uint256)" ) : .WordStack ) ) ) ) + ( .WordStack => ( ?KV0_x:Int : ( 327 : ( selector ( "test_failing_branch(uint256)" ) : .WordStack ) ) ) ) ( b"" => 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" ) @@ -553,14 +553,14 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 andBool ( TIMESTAMP_CELL:Int #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -587,7 +587,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -816,7 +816,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ( JUMPI 1124 bool2Word ( 100 <=Int KV0_x:Int ) ~> #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -833,7 +833,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected b/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected index d76f77f4e..3725f3ba5 100644 --- a/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected @@ -574,10 +574,10 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 rule [BASIC-BLOCK-1-TO-8]: - ( .K => JUMPI 1594 bool2Word ( ?KV1_y <=Int ?KV0_x ) + ( .K => JUMPI 1594 bool2Word ( ?KV1_y:Int <=Int ?KV0_x:Int ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -610,13 +610,13 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 CALLER_ID:Int - ( b"\n\x92T\xe4" => b"\x8c\x0e\xdd\x8b" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) ) + ( b"\n\x92T\xe4" => b"\x8c\x0e\xdd\x8b" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) ) 0 - ( .WordStack => ( ?KV1_y : ( ?KV0_x : ( 327 : ( selector ( "test_revert_branch(uint256,uint256)" ) : .WordStack ) ) ) ) ) + ( .WordStack => ( ?KV1_y:Int : ( ?KV0_x:Int : ( 327 : ( selector ( "test_revert_branch(uint256,uint256)" ) : .WordStack ) ) ) ) ) ( b"" => 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" ) @@ -804,16 +804,16 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 andBool ( TIMESTAMP_CELL:Int #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -840,7 +840,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(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" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List @@ -1071,7 +1071,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ( JUMPI 1594 bool2Word ( KV1_y:Int <=Int KV0_x:Int ) ~> #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1088,7 +1088,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List diff --git a/src/tests/integration/test-data/show/minimized/MergeKCFGTest.test_branch_merge(uint256,uint256,bool).expected b/src/tests/integration/test-data/show/minimized/MergeKCFGTest.test_branch_merge(uint256,uint256,bool).expected index 07e47add6..2dc187d85 100644 --- a/src/tests/integration/test-data/show/minimized/MergeKCFGTest.test_branch_merge(uint256,uint256,bool).expected +++ b/src/tests/integration/test-data/show/minimized/MergeKCFGTest.test_branch_merge(uint256,uint256,bool).expected @@ -116,13 +116,13 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 rule [BASIC-BLOCK-1-TO-17]: - ( .K => JUMPI 99 bool2Word ( ?KV2_z ==Int 0 ) + ( .K => JUMPI 99 bool2Word ( ?KV2_z:Int ==Int 0 ) ~> #pc [ JUMPI ] ~> #execute ~> #return 128 32 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -147,16 +147,16 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 CALLER_ID:Int - b"\x15T\xa2\xa4" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) +Bytes #buf ( 32 , ?KV2_z ) + b"\x15T\xa2\xa4" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) +Bytes #buf ( 32 , ?KV2_z:Int ) 0 - ( 228 : ( selector ( "applyOp(uint256,uint256,bool)" ) : ( 491460923342184218035706888008750043977755113263 : ( ?KV2_z : ( ?KV1_y : ( ?KV0_x : ( 193 : ( selector ( "test_branch_merge(uint256,uint256,bool)" ) : .WordStack ) ) ) ) ) ) ) ) + ( 228 : ( selector ( "applyOp(uint256,uint256,bool)" ) : ( 491460923342184218035706888008750043977755113263 : ( ?KV2_z:Int : ( ?KV1_y:Int : ( ?KV0_x:Int : ( 193 : ( selector ( "test_branch_merge(uint256,uint256,bool)" ) : .WordStack ) ) ) ) ) ) ) ) - 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\x00\xe0~\\\x97" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) +Bytes #buf ( 32 , ?KV2_z ) + 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\x00\xe0~\\\x97" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) +Bytes #buf ( 32 , ?KV2_z:Int ) 0 @@ -270,13 +270,13 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 ( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 ) - ( b"\n\x92T\xe4" => b"\xe0~\\\x97" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) +Bytes #buf ( 32 , ?KV2_z ) ) + ( b"\n\x92T\xe4" => b"\xe0~\\\x97" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) +Bytes #buf ( 32 , ?KV2_z:Int ) ) 0 - ( .WordStack => ( 0 : ( ?KV2_z : ( ?KV1_y : ( ?KV0_x : ( 60 : ( selector ( "applyOp(uint256,uint256,bool)" ) : .WordStack ) ) ) ) ) ) ) + ( .WordStack => ( 0 : ( ?KV2_z:Int : ( ?KV1_y:Int : ( ?KV0_x:Int : ( 60 : ( selector ( "applyOp(uint256,uint256,bool)" ) : .WordStack ) ) ) ) ) ) ) ( b"" => 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" ) @@ -507,19 +507,19 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 andBool ( TIMESTAMP_CELL:Int #return 128 32 ~> #pc [ CALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -549,7 +549,7 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( ListItem ( @@ -924,7 +924,7 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 ~> #return 128 32 ~> #pc [ CALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -941,7 +941,7 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( ListItem ( @@ -1317,7 +1317,7 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 ~> #return 128 32 ~> #pc [ CALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1334,7 +1334,7 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( ListItem ( diff --git a/src/tests/integration/test-data/show/node-refutation.expected b/src/tests/integration/test-data/show/node-refutation.expected index 5e67920d3..af5c290bc 100644 --- a/src/tests/integration/test-data/show/node-refutation.expected +++ b/src/tests/integration/test-data/show/node-refutation.expected @@ -88,7 +88,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 ( .K => JUMPI 535 bool2Word ( 10 <=Int KV0_x:Int ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -316,7 +316,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 andBool ( TIMESTAMP_CELL:Int #pc [ JUMPI ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -564,7 +564,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 andBool ( KV0_x:Int #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -593,7 +593,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -811,7 +811,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 andBool ( KV0_x:Int ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1058,7 +1058,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 andBool ( KV0_x:Int ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -677,7 +677,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -931,7 +931,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -960,7 +960,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -979,7 +979,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 CALLER_ID:Int - ( b"\n\x92T\xe4" => b"h\xc6\xc8\x93" +Bytes #buf ( 32 , ?KV0_addr ) ) + ( b"\n\x92T\xe4" => b"h\xc6\xc8\x93" +Bytes #buf ( 32 , ?KV0_addr:Int ) ) 0 @@ -1196,12 +1196,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 andBool ( ORIGIN_ID:Int CALL 0 645326474426547203313410069153905908525362434349 0 128 36 128 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1477,7 +1477,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 128 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1745,7 +1745,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #cheatcode_return 128 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2014,7 +2014,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #pc [ CALL ] => STATICCALL 0 491460923342184218035706888008750043977755113263 128 4 128 32 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2184,22 +2184,22 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - ( _PREVCALLER_CELL => 728815563385977040452943777879061427756277306518 ) + ( _PREVCALLER_CELL:Account => 728815563385977040452943777879061427756277306518 ) - ( _PREVORIGIN_CELL => ORIGIN_ID:Int ) + ( _PREVORIGIN_CELL:Account => ORIGIN_ID:Int ) - ( _NEWCALLER_CELL => 728815563385977040452943777879061427756277306518 ) + ( _NEWCALLER_CELL:Account => 728815563385977040452943777879061427756277306518 ) - ( _NEWORIGIN_CELL => .Account ) + ( _NEWORIGIN_CELL:Account => .Account ) ( false => true ) - ( _DEPTH_CELL => 0 ) + ( _DEPTH_CELL:Int => 0 ) false @@ -2268,7 +2268,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2467,22 +2467,22 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - ( _PREVCALLER_CELL => 728815563385977040452943777879061427756277306518 ) + ( _PREVCALLER_CELL:Account => 728815563385977040452943777879061427756277306518 ) - ( _PREVORIGIN_CELL => ORIGIN_ID:Int ) + ( _PREVORIGIN_CELL:Account => ORIGIN_ID:Int ) - ( _NEWCALLER_CELL => 645326474426547203313410069153905908525362434349 ) + ( _NEWCALLER_CELL:Account => 645326474426547203313410069153905908525362434349 ) - ( _NEWORIGIN_CELL => .Account ) + ( _NEWORIGIN_CELL:Account => .Account ) ( false => true ) - ( _DEPTH_CELL => 0 ) + ( _DEPTH_CELL:Int => 0 ) false @@ -2551,7 +2551,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2750,22 +2750,22 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - ( _PREVCALLER_CELL => 728815563385977040452943777879061427756277306518 ) + ( _PREVCALLER_CELL:Account => 728815563385977040452943777879061427756277306518 ) - ( _PREVORIGIN_CELL => ORIGIN_ID:Int ) + ( _PREVORIGIN_CELL:Account => ORIGIN_ID:Int ) - ( _NEWCALLER_CELL => 491460923342184218035706888008750043977755113263 ) + ( _NEWCALLER_CELL:Account => 491460923342184218035706888008750043977755113263 ) - ( _NEWORIGIN_CELL => .Account ) + ( _NEWORIGIN_CELL:Account => .Account ) ( false => true ) - ( _DEPTH_CELL => 0 ) + ( _DEPTH_CELL:Int => 0 ) false @@ -2834,7 +2834,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3075,22 +3075,22 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - ( _PREVCALLER_CELL => 728815563385977040452943777879061427756277306518 ) + ( _PREVCALLER_CELL:Account => 728815563385977040452943777879061427756277306518 ) - ( _PREVORIGIN_CELL => ORIGIN_ID:Int ) + ( _PREVORIGIN_CELL:Account => ORIGIN_ID:Int ) - ( _NEWCALLER_CELL => KV0_addr:Int ) + ( _NEWCALLER_CELL:Account => KV0_addr:Int ) - ( _NEWORIGIN_CELL => .Account ) + ( _NEWORIGIN_CELL:Account => .Account ) ( false => true ) - ( _DEPTH_CELL => 0 ) + ( _DEPTH_CELL:Int => 0 ) false @@ -3191,7 +3191,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 128 32 ) ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3445,7 +3445,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3728,7 +3728,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -4011,7 +4011,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -4348,7 +4348,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -4719,7 +4719,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -5120,7 +5120,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -5521,7 +5521,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -5995,7 +5995,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -6366,7 +6366,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -6765,7 +6765,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -7164,7 +7164,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -7637,7 +7637,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -8008,7 +8008,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -8408,7 +8408,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -8808,7 +8808,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -9282,7 +9282,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -9299,7 +9299,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xa98[\xe1\x02\xac>\xac)t\x83\xddb3\xd6+>\x14\x96" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ListItem ( @@ -9656,7 +9656,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -9702,7 +9702,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ListItem ( @@ -10059,7 +10059,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -10105,7 +10105,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00V\x15\xde\xb7\x98\xbb>M\xfa\x019\xdf\xa1\xb3\xd43\xcc#\xb7/" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ListItem ( @@ -10462,7 +10462,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -10508,7 +10508,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 #buf ( 32 , KV0_addr:Int ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ListItem ( @@ -10939,7 +10939,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -11313,7 +11313,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -11716,7 +11716,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -12119,7 +12119,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -12599,7 +12599,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #setLocalMem 128 32 b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xa98[\xe1\x02\xac>\xac)t\x83\xddb3\xd6+>\x14\x96" ) ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -12973,7 +12973,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -13379,7 +13379,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -13785,7 +13785,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -14268,7 +14268,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #pc [ STATICCALL ] => CALL 0 645326474426547203313410069153905908525362434349 0 160 4 160 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -14642,7 +14642,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #endPrank => CALL 0 645326474426547203313410069153905908525362434349 0 160 4 160 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -15048,7 +15048,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #endPrank => CALL 0 645326474426547203313410069153905908525362434349 0 160 4 160 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -15454,7 +15454,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #endPrank => CALL 0 645326474426547203313410069153905908525362434349 0 160 4 160 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -15934,7 +15934,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 160 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -16191,7 +16191,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #return 160 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -16476,7 +16476,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #return 160 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -16761,7 +16761,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #return 160 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -17100,7 +17100,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #pc [ CALL ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -17357,7 +17357,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ CALL ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -17643,7 +17643,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ CALL ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -17929,7 +17929,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ CALL ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -18265,7 +18265,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ( #end EVMC_SUCCESS => #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -18522,7 +18522,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -18804,7 +18804,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -19086,7 +19086,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -19418,7 +19418,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 #halt ~> ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -19675,7 +19675,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -19957,7 +19957,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -20239,7 +20239,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL