diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 83668a50c..87217aec7 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -149,7 +149,7 @@ jobs: docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry' - name: 'Run end-to-end tests' run: | - TEST_ARGS='--numprocesses=8 -vv -k "test_kontrol_end_to_end"' + TEST_ARGS='--numprocesses=6 -vv --force-sequential -k "test_kontrol_end_to_end"' docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}" - name: 'Tear down Docker' if: always() diff --git a/.github/workflows/update-expected-output.yml b/.github/workflows/update-expected-output.yml index af8655e5d..94a561b16 100644 --- a/.github/workflows/update-expected-output.yml +++ b/.github/workflows/update-expected-output.yml @@ -28,9 +28,10 @@ jobs: docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry' - name: 'Run integration tests' run: | - TEST_ARGS="--maxfail=1000 --numprocesses=6 --update-expected-output --force-sequential -vv" + TEST_ARGS="--maxfail=1000 --numprocesses=4 --update-expected-output --force-sequential -vv" docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"not (test_kontrol_cse or test_foundry_minimize_proof or test_kontrol_end_to_end)\"' || true" docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"test_kontrol_cse or test_foundry_minimize_proof\"' || true" + docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"test_kontrol_end_to_end\"' || true" - name: 'Copy updated files to host' run: | docker cp kontrol-ci-integration-${GITHUB_SHA}:/home/github-user/workspace/src/tests/integration/test-data/show ./src/tests/integration/test-data/ diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md index 15da6c2a9..4e1270a7e 100644 --- a/src/kontrol/kdist/cheatcodes.md +++ b/src/kontrol/kdist/cheatcodes.md @@ -76,8 +76,8 @@ module FOUNDRY-CHEAT-CODES false + .List false - .List .List @@ -946,7 +946,8 @@ A `StorageSlot` pair is formed from an address and a storage index. ```k syntax StorageSlot ::= "{" Int "|" Int "}" - // ------------------------------------------ + syntax CallToAddress ::= "{" Int "|" Bytes "}" + // ---------------------------------------------- ``` We define two new status codes: @@ -965,15 +966,14 @@ If the address is not in the whitelist `WLIST` then `KEVM` goes into an error st ```k rule [foundry.catchNonWhitelistedCalls]: - (#call _ ACCTTO _ _ _ _ false - ~> #popCallStack - ~> #popWorldState) => #end KONTROL_WHITELISTCALL ... + (#call _ ACCTTO _ _ _ CALLDATA false + ~> #return _ _) => #end KONTROL_WHITELISTCALL ... true - WLIST + WLIST ... - requires notBool ACCTTO in WLIST + requires notBool ({ACCTTO|CALLDATA} in WLIST orBool {ACCTTO|.Bytes} in WLIST) [priority(40)] ``` @@ -1003,9 +1003,32 @@ function allowCallsToAddress(address) external; Adds an account address to the whitelist. The execution of the modified KEVM will stop when a call has been made to an address which is not in the whitelist. ```k - rule [foundry.allowCallsToAddress]: - #cheatcode_call SELECTOR ARGS => #loadAccount #asWord(ARGS) ~> #addAddressToWhitelist #asWord(ARGS) ... - requires SELECTOR ==Int selector ( "allowCallsToAddress(address)" ) + rule [foundry.allowAllCallsToAddress]: + #cheatcode_call SELECTOR ARGS + => #loadAccount #asWord(ARGS) + ~> #setAllowedCall #asWord(ARGS) .Bytes ... + requires SELECTOR ==Int selector("allowCallsToAddress(address)") +``` + +#### `allowCalls` - Add an account address and calldata prefix to a whitelist. + +``` +function allowCalls(address, bytes calldata data) external; +``` + +Adds an account address and calldata prefix to the whitelist. The execution of the modified KEVM will stop when a call has been made to an address and/or with calldata which are not in the whitelist. + +```k + rule [foundry.allowCalls]: + #cheatcode_call SELECTOR ARGS + => #loadAccount #asWord(#range(ARGS, 0, 32)) + ~> #etchAccountIfEmpty #asWord(#range(ARGS, 0, 32)) + ~> #setAllowedCall + #asWord(#range(ARGS, 0, 32)) + #range(ARGS, #asWord(#range(ARGS, 32, 32)) +Int 32, #asWord(#range(ARGS, #asWord(#range(ARGS, 32, 32)), 32))) + ... + + requires SELECTOR ==Int selector ( "allowCalls(address,bytes)" ) ``` #### `allowChangesToStorage` - Add an account address and a storage slot to a whitelist. @@ -1608,19 +1631,6 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa rule #checkTopics(ListItem(CHECK) CHECKS, ListItem(V1) L1, ListItem(V2) L2) => #checkTopic(CHECK, V1, V2) andBool #checkTopics(CHECKS, L1, L2) requires size(L1) ==Int size(L2) ``` -- `#addAddressToWhitelist` enables the whitelist restriction for calls and adds an address to the whitelist. - -```k - syntax KItem ::= "#addAddressToWhitelist" Int [symbol(foundry_addAddressToWhitelist)] - // ------------------------------------------------------------------------------------- - rule #addAddressToWhitelist ACCT => .K ... - - _ => true - WLIST => WLIST ListItem(ACCT) - ... - -``` - - `#addStorageSlotToWhitelist` enables the whitelist restriction for storage chagnes and adds a `StorageSlot` item to the whitelist. ```k @@ -1652,6 +1662,19 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa rule #etchAccountIfEmpty _ => .K ... [owise] ``` +- `#setAllowedCall ALLOWEDACCOUNT ALLOWEDCALLDATA` and `setAllowedAllCalls ALLOWEDACCOUNT` will update the `` list with the given account and calldata. + +```k + syntax KItem ::= "#setAllowedCall" Account Bytes [symbol(foundry_setAllowedCall)] + // ----------------------------------------------------------------------------------- + rule #setAllowedCall ALLOWEDACCOUNT ALLOWEDCALLDATA => .K ... + + _ => true + ALLOWEDCALLS => ALLOWEDCALLS ListItem({ALLOWEDACCOUNT|ALLOWEDCALLDATA}) + ... + +``` + - `#setMockCall MOCKADDRESS MOCKCALLDATA MOCKRETURN` will update the `` mapping for the given account. ```k @@ -1765,6 +1788,7 @@ Selectors for **implemented** cheat code functions. rule ( selector ( "prank(address)" ) => 3395723175 ) rule ( selector ( "prank(address,address)" ) => 1206193358 ) rule ( selector ( "allowCallsToAddress(address)" ) => 1850795572 ) + rule ( selector ( "allowCalls(address,bytes)" ) => 1808051021 ) rule ( selector ( "allowChangesToStorage(address,uint256)" ) => 4207417100 ) rule ( selector ( "infiniteGas()" ) => 3986649939 ) rule ( selector ( "setGas(uint256)" ) => 3713137314 ) diff --git a/src/kontrol/kdist/kontrol_lemmas.md b/src/kontrol/kdist/kontrol_lemmas.md index 8e965c2fc..f4aeeb343 100644 --- a/src/kontrol/kdist/kontrol_lemmas.md +++ b/src/kontrol/kdist/kontrol_lemmas.md @@ -188,5 +188,18 @@ module KONTROL-AUX-LEMMAS requires 0 true [simplification] + rule KI:KItem in ListItem(KJ:KItem) => KI ==K KJ [simplification] + + // Recursive list membership check for lists with multiple elements + rule KI:KItem in (ListItem(KI) Rest) => true [simplification] + rule KI:KItem in (ListItem(KJ) Rest) => KI in Rest [simplification] + rule KI:KItem in .List => false [simplification] + endmodule ``` \ No newline at end of file diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 5f5e346cd..9aed3db62 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -1038,8 +1038,8 @@ def _init_cterm( 'ISEVENTEXPECTED_CELL': FALSE, 'ISCALLWHITELISTACTIVE_CELL': FALSE, 'ISSTORAGEWHITELISTACTIVE_CELL': FALSE, - 'ADDRESSLIST_CELL': list_empty(), 'STORAGESLOTLIST_CELL': list_empty(), + 'ALLOWEDCALLSLIST_CELL': list_empty(), 'MOCKCALLS_CELL': KApply('.MockCallCellMap'), 'MOCKFUNCTIONS_CELL': KApply('.MockFunctionCellMap'), 'ACTIVETRACING_CELL': TRUE if trace_options.active_tracing else FALSE, @@ -1425,7 +1425,7 @@ def _final_term( 'ISEVENTEXPECTED_CELL': KVariable('ISEVENTEXPECTED_FINAL'), 'ISCALLWHITELISTACTIVE_CELL': KVariable('ISCALLWHITELISTACTIVE_FINAL'), 'ISSTORAGEWHITELISTACTIVE_CELL': KVariable('ISSTORAGEWHITELISTACTIVE_FINAL'), - 'ADDRESSLIST_CELL': KVariable('ADDRESSLIST_FINAL'), + 'ALLOWEDCALLSLIST_CELL': KVariable('ALLOWEDCALLSLIST_FINAL'), 'STORAGESLOTLIST_CELL': KVariable('STORAGESLOTLIST_FINAL'), } diff --git a/src/tests/integration/test-data/end-to-end-prove-all b/src/tests/integration/test-data/end-to-end-prove-all index 749effdd8..76cb04fcd 100644 --- a/src/tests/integration/test-data/end-to-end-prove-all +++ b/src/tests/integration/test-data/end-to-end-prove-all @@ -1,3 +1,5 @@ +AllowChangesTest.testAllowCalls(uint256) +AllowChangesTest.testFailAllowCalls_ifNotWhitelisted(uint256) CounterTest.test_Increment() ForgetBranchTest.test_forgetBranch(uint256) RandomVarTest.test_custom_names() diff --git a/src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol b/src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol index 918e5c68d..6745a87f7 100644 --- a/src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol +++ b/src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol @@ -42,13 +42,11 @@ contract AllowChangesTest is Test, KontrolCheats { } function testFailAllowCallsToAddress() public { kevm.allowCallsToAddress(address(canChange)); - kevm.allowChangesToStorage(address(canChange), 0); cannotChange.changeSlot0(10245); } function testFailAllowChangesToStorage() public { - kevm.allowCallsToAddress(address(canChange)); kevm.allowChangesToStorage(address(canChange), 0); canChange.changeSlot1(23452); 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 8ce6adf4e..16aa4144f 100644 --- a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected +++ b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected @@ -258,12 +258,12 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected index 88a2bcc1c..98074b446 100644 --- a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected +++ b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected @@ -189,12 +189,12 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0 false + + .List + false - - .List - .List @@ -368,12 +368,12 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0 false + + .List + false - - .List - .List 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 224231d75..741731886 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 @@ -218,12 +218,12 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected index 07bc9ad96..b9db89f79 100644 --- a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected @@ -450,12 +450,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -859,12 +859,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1250,12 +1250,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1643,12 +1643,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -2037,12 +2037,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 false + + .List + false - - .List - .List 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 c626a4c93..a9ad932fb 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 @@ -499,12 +499,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 false + + .List + false - - .List - .List @@ -908,12 +908,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 false + + .List + false - - .List - .List @@ -1299,12 +1299,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 false + + .List + false - - .List - .List @@ -1692,12 +1692,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 false + + .List + false - - .List - .List @@ -2086,12 +2086,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 false + + .List + false - - .List - .List @@ -2484,12 +2484,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 false + + .List + false - - .List - .List @@ -2884,12 +2884,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 false + + .List + false - - .List - .List 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 e46057596..925f154e1 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 @@ -503,12 +503,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT false + + .List + false - - .List - .List @@ -896,12 +896,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT false + + .List + false - - .List - .List @@ -1308,12 +1308,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT false + + .List + false - - .List - .List @@ -1701,12 +1701,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT false + + .List + false - - .List - .List @@ -2099,12 +2099,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT false + + .List + false - - .List - .List @@ -2498,12 +2498,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT false + + .List + false - - .List - .List @@ -2898,12 +2898,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT false + + .List + false - - .List - .List 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 a197790ee..e73f1e15c 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 @@ -186,12 +186,12 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -364,12 +364,12 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0 false + + .List + false - - .List - .List 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 c43cfb883..01d3133ec 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 @@ -261,12 +261,12 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): false + + .List + false - - .List - .List @@ -450,12 +450,12 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): false + + .List + false - - .List - .List @@ -640,12 +640,12 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): false + + .List + false - - .List - .List @@ -831,12 +831,12 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): false + + .List + false - - .List - .List 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 b26bc102c..ee6e3c0a6 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 @@ -251,12 +251,12 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 false + + .List + false - - .List - .List @@ -493,12 +493,12 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 false + + .List + false - - .List - .List @@ -734,12 +734,12 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 false + + .List + false - - .List - .List @@ -977,12 +977,12 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 false + + .List + false - - .List - .List @@ -1220,12 +1220,12 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 false + + .List + false - - .List - .List 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 65ed17e16..61736953f 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 @@ -251,12 +251,12 @@ Node 10: false + + .List + false - - .List - .List @@ -497,12 +497,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 false + + .List + false - - .List - .List @@ -739,12 +739,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 false + + .List + false - - .List - .List @@ -980,12 +980,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 false + + .List + false - - .List - .List @@ -1223,12 +1223,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 false + + .List + false - - .List - .List @@ -1466,12 +1466,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 false + + .List + false - - .List - .List 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 0a01fc323..fc6f28c99 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 @@ -342,12 +342,12 @@ Node 20: false + + .List + false - - .List - .List @@ -588,12 +588,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List @@ -830,12 +830,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List @@ -1071,12 +1071,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List @@ -1314,12 +1314,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List @@ -1565,12 +1565,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List @@ -1815,12 +1815,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List @@ -2162,12 +2162,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List @@ -2507,12 +2507,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List @@ -2853,12 +2853,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List @@ -3202,12 +3202,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List @@ -3551,12 +3551,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List @@ -3903,12 +3903,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List @@ -4255,12 +4255,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List @@ -4503,12 +4503,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List @@ -4751,12 +4751,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List 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 5b1b2aa09..ed6e56bd4 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 @@ -248,12 +248,12 @@ Node 10: false + + .List + false - - .List - .List @@ -494,12 +494,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 false + + .List + false - - .List - .List @@ -736,12 +736,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 false + + .List + false - - .List - .List @@ -977,12 +977,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 false + + .List + false - - .List - .List @@ -1220,12 +1220,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 false + + .List + false - - .List - .List @@ -1463,12 +1463,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 false + + .List + false - - .List - .List 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 87272be20..796e86b4c 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 @@ -254,12 +254,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 false + + .List + false - - .List - .List @@ -496,12 +496,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 false + + .List + false - - .List - .List @@ -737,12 +737,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 false + + .List + false - - .List - .List @@ -980,12 +980,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 false + + .List + false - - .List - .List @@ -1223,12 +1223,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 false + + .List + false - - .List - .List 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 840b6226b..098aaf6db 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 @@ -311,12 +311,12 @@ Node 16: false + + .List + false - - .List - .List @@ -560,12 +560,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 false + + .List + false - - .List - .List @@ -802,12 +802,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 false + + .List + false - - .List - .List @@ -1046,12 +1046,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 false + + .List + false - - .List - .List @@ -1289,12 +1289,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 false + + .List + false - - .List - .List @@ -1533,12 +1533,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 false + + .List + false - - .List - .List @@ -1779,12 +1779,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 false + + .List + false - - .List - .List @@ -2025,12 +2025,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 false + + .List + false - - .List - .List @@ -2271,12 +2271,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 false + + .List + false - - .List - .List @@ -2517,12 +2517,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 false + + .List + false - - .List - .List 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 501b0437f..48ade8e10 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 @@ -309,12 +309,12 @@ Node 16: false + + .List + false - - .List - .List @@ -560,12 +560,12 @@ Node 15: false + + .List + false - - .List - .List @@ -811,12 +811,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1053,12 +1053,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1299,12 +1299,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1544,12 +1544,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1790,12 +1790,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -2038,12 +2038,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -2286,12 +2286,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -2534,12 +2534,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -2782,12 +2782,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 false + + .List + false - - .List - .List 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 280fa7784..70afb3a06 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 @@ -249,12 +249,12 @@ Node 7: false + + .List + false - - .List - .List @@ -498,12 +498,12 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -746,12 +746,12 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -995,12 +995,12 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1244,12 +1244,12 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1491,12 +1491,12 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected index 3523dee1c..a85992525 100644 --- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected @@ -275,12 +275,12 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -523,12 +523,12 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -771,12 +771,12 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1017,12 +1017,12 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1266,12 +1266,12 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1516,12 +1516,12 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1765,12 +1765,12 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -2014,12 +2014,12 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected index ce05552be..e4b35fa99 100644 --- a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected @@ -273,12 +273,12 @@ Node 10: false + + .List + false - - .List - .List @@ -524,12 +524,12 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -772,12 +772,12 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1020,12 +1020,12 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1266,12 +1266,12 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1515,12 +1515,12 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1765,12 +1765,12 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -2014,12 +2014,12 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -2263,12 +2263,12 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected b/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected index be99cdcd3..e769cb5e5 100644 --- a/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected +++ b/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected @@ -421,12 +421,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 false + + .List + false - - .List - .List @@ -668,12 +668,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 false + + .List + false - - .List - .List @@ -915,12 +915,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 false + + .List + false - - .List - .List @@ -1163,12 +1163,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 false + + .List + false - - .List - .List @@ -1412,12 +1412,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 false + + .List + false - - .List - .List @@ -1659,12 +1659,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 false + + .List + false - - .List - .List @@ -1907,12 +1907,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 false + + .List + false - - .List - .List @@ -2152,12 +2152,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 false + + .List + false - - .List - .List @@ -2398,12 +2398,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 false + + .List + false - - .List - .List @@ -2645,12 +2645,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 false + + .List + false - - .List - .List @@ -2893,12 +2893,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 false + + .List + false - - .List - .List @@ -3137,12 +3137,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 false + + .List + false - - .List - .List @@ -3382,12 +3382,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 false + + .List + false - - .List - .List @@ -3628,12 +3628,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 false + + .List + false - - .List - .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 1d41c4f6a..3e20437f4 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 @@ -218,12 +218,12 @@ module SUMMARY-TEST%BLOCKPARAMSTEST.TESTWARP(UINT256):0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected index d06771942..9c2c67d65 100644 --- a/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected @@ -329,12 +329,12 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -644,12 +644,12 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -980,12 +980,12 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected index 770f255b2..65f472402 100644 --- a/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected +++ b/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected @@ -325,12 +325,12 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -640,12 +640,12 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -974,12 +974,12 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected b/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected index be56a06a0..44bbcf2e0 100644 --- a/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected +++ b/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected @@ -192,12 +192,12 @@ module SUMMARY-TEST%CALLABLESTORAGECONTRACT.STR():0 false + + .List + false - - .List - .List @@ -374,12 +374,12 @@ module SUMMARY-TEST%CALLABLESTORAGECONTRACT.STR():0 false + + .List + false - - .List - .List 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 da90bd342..fa0e7bb64 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 @@ -259,12 +259,12 @@ module SUMMARY-TEST%CALLABLESTORAGETEST.TEST-STR():0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected b/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected index be60ac85b..c39467ecb 100644 --- a/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected +++ b/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected @@ -259,12 +259,12 @@ module SUMMARY-TEST%CONSTRUCTORTEST.INIT:0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected b/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected index 74e12608a..343379509 100644 --- a/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected +++ b/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected @@ -284,12 +284,12 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 false + + .List + false - - .List - .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 c5f847603..d5fe993fe 100644 --- a/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected +++ b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected @@ -284,12 +284,12 @@ module SUMMARY-TEST%CONTRACTFIELDTEST.TESTESCROWTOKEN():0 false + + .List + false - - .List - .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 457f40149..1439a1183 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 @@ -165,12 +165,12 @@ module SUMMARY-TEST%ENUM.ENUM-ARGUMENT-RANGE(UINT8):0 false + + .List + false - - .List - .List 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 be30d1984..f613cfc2b 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 @@ -224,12 +224,12 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0 false + + .List + false - - .List - .List @@ -437,12 +437,12 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0 false + + .List + false - - .List - .List 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 f9d23f769..56d628e59 100644 --- a/src/tests/integration/test-data/show/Enum.init.cse.expected +++ b/src/tests/integration/test-data/show/Enum.init.cse.expected @@ -140,12 +140,12 @@ module SUMMARY-TEST%ENUM.INIT:0 false + + .List + false - - .List - .List 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 cc93e77bf..a37f93c51 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 @@ -287,12 +287,12 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0 false + + .List + false - - .List - .List @@ -532,12 +532,12 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0 false + + .List + false - - .List - .List @@ -777,12 +777,12 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0 false + + .List + false - - .List - .List @@ -1023,12 +1023,12 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0 false + + .List + false - - .List - .List @@ -1270,12 +1270,12 @@ module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/Identity.applyOp(uint256).cse.expected b/src/tests/integration/test-data/show/Identity.applyOp(uint256).cse.expected index 6d930cc74..45a4fa68f 100644 --- a/src/tests/integration/test-data/show/Identity.applyOp(uint256).cse.expected +++ b/src/tests/integration/test-data/show/Identity.applyOp(uint256).cse.expected @@ -195,12 +195,12 @@ module SUMMARY-SRC%CSE%IDENTITY.APPLYOP(UINT256):0 false + + .List + false - - .List - .List @@ -377,12 +377,12 @@ module SUMMARY-SRC%CSE%IDENTITY.APPLYOP(UINT256):0 false + + .List + false - - .List - .List 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 e22911dcd..3b1432480 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 @@ -141,12 +141,12 @@ module SUMMARY-SRC%CSE%IDENTITY.IDENTITY(UINT256):0 false + + .List + false - - .List - .List 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 38800ad8e..22474e7af 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 @@ -192,12 +192,12 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0 false + + .List + false - - .List - .List @@ -376,12 +376,12 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0 false + + .List + false - - .List - .List 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 5ff629d20..16901224e 100644 --- a/src/tests/integration/test-data/show/ImportedContract.count().cse.expected +++ b/src/tests/integration/test-data/show/ImportedContract.count().cse.expected @@ -144,12 +144,12 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.COUNT():0 false + + .List + false - - .List - .List 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 33ba21ca1..9d378a6aa 100644 --- a/src/tests/integration/test-data/show/ImportedContract.init.cse.expected +++ b/src/tests/integration/test-data/show/ImportedContract.init.cse.expected @@ -145,12 +145,12 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.INIT:0 false + + .List + false - - .List - .List 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 b64266145..5b83e4233 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 @@ -192,12 +192,12 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 false + + .List + false - - .List - .List @@ -374,12 +374,12 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 false + + .List + false - - .List - .List 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 8acabefa5..2fd6f3f60 100644 --- a/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected +++ b/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected @@ -283,12 +283,12 @@ module SUMMARY-TEST%INTERFACETAGTEST.TESTINTERFACE():0 false + + .List + false - - .List - .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 5003ca484..70109f148 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 @@ -345,12 +345,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List @@ -590,12 +590,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List @@ -837,12 +837,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List @@ -1084,12 +1084,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List @@ -1332,12 +1332,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List @@ -1581,12 +1581,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List @@ -1828,12 +1828,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List @@ -2077,12 +2077,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List @@ -2328,12 +2328,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List @@ -2625,12 +2625,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List @@ -2896,12 +2896,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List @@ -3168,12 +3168,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List @@ -3440,12 +3440,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List @@ -3713,12 +3713,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List @@ -3987,12 +3987,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 false + + .List + false - - .List - .List 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 31410769a..c35b56268 100644 --- a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected +++ b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected @@ -295,12 +295,12 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 false + + .List + false - - .List - .List @@ -558,12 +558,12 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 false + + .List + false - - .List - .List @@ -820,12 +820,12 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 false + + .List + false - - .List - .List @@ -1084,12 +1084,12 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 false + + .List + false - - .List - .List @@ -1348,12 +1348,12 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 false + + .List + false - - .List - .List 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 74936941a..afd95e844 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 @@ -147,12 +147,12 @@ module SUMMARY-TEST%STATICCALLCONTRACT.SET(UINT256):0 false + + .List + false - - .List - .List 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 ebc024faa..6d59a2ec9 100644 --- a/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected +++ b/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected @@ -294,12 +294,12 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 false + + .List + false - - .List - .List @@ -544,12 +544,12 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 false + + .List + false - - .List - .List @@ -792,12 +792,12 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/gas-abstraction.expected b/src/tests/integration/test-data/show/gas-abstraction.expected index 82e14cbe8..b6e1f172a 100644 --- a/src/tests/integration/test-data/show/gas-abstraction.expected +++ b/src/tests/integration/test-data/show/gas-abstraction.expected @@ -354,12 +354,12 @@ Node 6: false + + .List + false - - .List - .List @@ -596,12 +596,12 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 false + + .List + false - - .List - .List @@ -834,12 +834,12 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 false + + .List + false - - .List - .List @@ -1072,12 +1072,12 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/merge-loop-heads.expected b/src/tests/integration/test-data/show/merge-loop-heads.expected index f4a18cd2d..a72cb6221 100644 --- a/src/tests/integration/test-data/show/merge-loop-heads.expected +++ b/src/tests/integration/test-data/show/merge-loop-heads.expected @@ -391,12 +391,12 @@ Node 21: false + + .List + false - - .List - .List @@ -643,12 +643,12 @@ Node 22: false + + .List + false - - .List - .List @@ -895,12 +895,12 @@ Node 23: false + + .List + false - - .List - .List @@ -1144,12 +1144,12 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 false + + .List + false - - .List - .List @@ -1387,12 +1387,12 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 false + + .List + false - - .List - .List @@ -1631,12 +1631,12 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 false + + .List + false - - .List - .List @@ -1876,12 +1876,12 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 false + + .List + false - - .List - .List @@ -2123,12 +2123,12 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 false + + .List + false - - .List - .List 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 95193f315..21fd3eb19 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 @@ -220,12 +220,12 @@ Node 20: false + + .List + false - - .List - .List @@ -471,12 +471,12 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected b/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected index 99970257b..b5aff030d 100644 --- a/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected +++ b/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected @@ -214,12 +214,12 @@ Node 10: false + + .List + false - - .List - .List @@ -460,12 +460,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected b/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected index d80948109..af24ed28c 100644 --- a/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected +++ b/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected @@ -259,12 +259,12 @@ Node 16: false + + .List + false - - .List - .List @@ -507,12 +507,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 false + + .List + false - - .List - .List @@ -754,12 +754,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 false + + .List + false - - .List - .List @@ -1000,12 +1000,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 false + + .List + false - - .List - .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 3725f3ba5..2bf757504 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 @@ -257,12 +257,12 @@ Node 16: false + + .List + false - - .List - .List @@ -508,12 +508,12 @@ Node 15: false + + .List + false - - .List - .List @@ -758,12 +758,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1007,12 +1007,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 false + + .List + false - - .List - .List @@ -1255,12 +1255,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 false + + .List + false - - .List - .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 2dc187d85..e00be6d20 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 @@ -461,12 +461,12 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 false + + .List + false - - .List - .List @@ -854,12 +854,12 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 false + + .List + false - - .List - .List @@ -1246,12 +1246,12 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 false + + .List + false - - .List - .List @@ -1639,12 +1639,12 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/node-refutation.expected b/src/tests/integration/test-data/show/node-refutation.expected index af5c290bc..4884089e0 100644 --- a/src/tests/integration/test-data/show/node-refutation.expected +++ b/src/tests/integration/test-data/show/node-refutation.expected @@ -269,12 +269,12 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 false + + .List + false - - .List - .List @@ -513,12 +513,12 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 false + + .List + false - - .List - .List @@ -760,12 +760,12 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 false + + .List + false - - .List - .List @@ -1007,12 +1007,12 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/show/split-node.expected b/src/tests/integration/test-data/show/split-node.expected index 67fb12c6a..e7cec3058 100644 --- a/src/tests/integration/test-data/show/split-node.expected +++ b/src/tests/integration/test-data/show/split-node.expected @@ -885,12 +885,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -1148,12 +1148,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -1413,12 +1413,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -1679,12 +1679,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -1947,12 +1947,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -2230,12 +2230,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -2513,12 +2513,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -2796,12 +2796,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -3121,12 +3121,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -3407,12 +3407,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -3690,12 +3690,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -3973,12 +3973,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -4277,12 +4277,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -4681,12 +4681,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -5082,12 +5082,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -5483,12 +5483,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -5926,12 +5926,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -6328,12 +6328,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -6727,12 +6727,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -7126,12 +7126,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -7567,12 +7567,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -7970,12 +7970,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -8370,12 +8370,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -8770,12 +8770,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -9212,12 +9212,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -9618,12 +9618,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -10021,12 +10021,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -10424,12 +10424,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -10869,12 +10869,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -11275,12 +11275,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -11678,12 +11678,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -12081,12 +12081,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -12526,12 +12526,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -12935,12 +12935,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -13341,12 +13341,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -13747,12 +13747,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -14195,12 +14195,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -14604,12 +14604,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -15010,12 +15010,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -15416,12 +15416,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -15864,12 +15864,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -16153,12 +16153,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -16438,12 +16438,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -16723,12 +16723,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -17029,12 +17029,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -17319,12 +17319,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -17605,12 +17605,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -17891,12 +17891,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -18198,12 +18198,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -18484,12 +18484,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -18766,12 +18766,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -19048,12 +19048,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -19351,12 +19351,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -19637,12 +19637,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -19919,12 +19919,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -20201,12 +20201,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List @@ -20504,12 +20504,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 false + + .List + false - - .List - .List diff --git a/src/tests/integration/test-data/src/AllowCalls.t.sol b/src/tests/integration/test-data/src/AllowCalls.t.sol new file mode 100644 index 000000000..f45ae6dea --- /dev/null +++ b/src/tests/integration/test-data/src/AllowCalls.t.sol @@ -0,0 +1,58 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import "forge-std/Test.sol"; +import "kontrol-cheatcodes/KontrolCheats.sol"; + +contract ValueStore { + uint256 public slot0; + uint256 public slot1; + + function changeSlot0(uint256 newValue) public { + slot0 = newValue; + } + + function changeSlot1(uint256 newValue) public { + slot1 = newValue; + } +} + +contract AllowChangesTest is Test, KontrolCheats { + ValueStore canChange; + ValueStore cannotChange; + + function setUp() public { + canChange = new ValueStore(); + cannotChange = new ValueStore(); + } + + function testAllowCalls(uint256 value) public { + /* Whitelisting two calls to ensure that `allowCalls` is working + for whitelist with > 1 elements */ + bytes memory changeCallDataOne = abi.encodeWithSelector( + ValueStore.changeSlot0.selector, + value + ); + + bytes memory changeCallDataTwo = abi.encodeWithSelector( + ValueStore.changeSlot1.selector, + value + ); + + kevm.allowCalls(address(canChange), changeCallDataOne); + kevm.allowCalls(address(canChange), changeCallDataTwo); + + canChange.changeSlot0(value); + } + + function testFailAllowCalls_ifNotWhitelisted(uint256 value) public { + bytes memory changeCallData = abi.encodeWithSelector( + ValueStore.changeSlot0.selector, + value + ); + + kevm.allowCalls(address(canChange), changeCallData); + + canChange.changeSlot1(value); + } +} \ No newline at end of file diff --git a/src/tests/integration/test_kontrol.py b/src/tests/integration/test_kontrol.py index 14d1c68d7..5e4ea717d 100644 --- a/src/tests/integration/test_kontrol.py +++ b/src/tests/integration/test_kontrol.py @@ -68,6 +68,7 @@ def foundry_end_to_end(foundry_root_dir: Path | None, tmp_path_factory: TempPath 'require': str(foundry_root / 'lemmas.k'), 'module-import': 'TestBase:KONTROL-LEMMAS', 'metadata': False, + 'auxiliary_lemmas': True, } ), foundry=Foundry(foundry_root), diff --git a/src/tests/integration/utils.py b/src/tests/integration/utils.py index 010fda208..b2340466a 100644 --- a/src/tests/integration/utils.py +++ b/src/tests/integration/utils.py @@ -1,5 +1,6 @@ from __future__ import annotations +from difflib import unified_diff from pathlib import Path from typing import TYPE_CHECKING @@ -47,7 +48,17 @@ def assert_or_update_show_output(actual_text: str, expected_file: Path, *, updat else: assert expected_file.is_file() expected_text = expected_file.read_text() - assert actual_text == expected_text + if actual_text != expected_text: + diff = '\n'.join( + unified_diff( + expected_text.splitlines(), + actual_text.splitlines(), + fromfile=str(expected_file), + tofile='actual_text', + lineterm='', + ) + ) + raise AssertionError(f'The actual output does not match the expected output:\n{diff}') def assert_pass(test: str, proof: Proof) -> None: