From 13c0f97d313913202f9a79bdd796b15915959bab Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Mon, 10 Jul 2023 20:45:40 +0800 Subject: [PATCH] Minor code refactor; update tests w/new output --- kevm-pyk/src/kevm_pyk/foundry.py | 3 +- kevm-pyk/src/kevm_pyk/utils.py | 6 +- .../test-data/contracts.k.expected | 390 +++++++++--------- .../integration/test-data/foundry.k.expected | 60 +-- .../AssertTest.testFail_assert_false.expected | 2 + .../AssertTest.testFail_assert_true.expected | 6 +- ...AssertTest.testFail_expect_revert.expected | 6 +- .../AssertTest.test_assert_false.expected | 6 +- .../show/AssertTest.test_assert_true.expected | 2 + .../AssertTest.test_failing_branch.expected | 7 +- .../AssertTest.test_revert_branch.expected | 8 +- .../AssumeTest.testFail_assume_false.expected | 8 +- .../AssumeTest.testFail_assume_true.expected | 2 + .../AssumeTest.test_assume_false.expected | 8 +- .../test-data/show/LoopsTest.sum_N.expected | 2 + .../SetUpDeployTest.test_extcodesize.expected | 2 + 16 files changed, 280 insertions(+), 238 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/foundry.py b/kevm-pyk/src/kevm_pyk/foundry.py index 87eb2a4083..2a3fd98195 100644 --- a/kevm-pyk/src/kevm_pyk/foundry.py +++ b/kevm-pyk/src/kevm_pyk/foundry.py @@ -828,8 +828,7 @@ def foundry_get_model( res_lines.append('') res_lines.append(f'Node id: {node_id}') node = proof.kcfg.node(node_id) - model_info = print_model(node, kcfg_explore) - res_lines.extend(model_info) + res_lines.extend(print_model(node, kcfg_explore)) return '\n'.join(res_lines) diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index 967f88616e..616d7a2c95 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -193,8 +193,7 @@ def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore) -> list[str]: for node in proof.pending: res_lines.append('') res_lines.append(f'ID: {node.id}:') - counterexample = print_model(node, kcfg_explore) - res_lines.extend(counterexample) + res_lines.extend(print_model(node, kcfg_explore)) if num_failing > 0: res_lines.append('') res_lines.append('Failing nodes:') @@ -215,8 +214,7 @@ def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore) -> list[str]: res_lines.append(' Path condition:') res_lines += [f' {kcfg_explore.kprint.pretty_print(proof.path_constraints(node.id))}'] - counterexample = print_model(node, kcfg_explore) - res_lines.extend(counterexample) + res_lines.extend(print_model(node, kcfg_explore)) res_lines.append('') res_lines.append( diff --git a/kevm-pyk/src/tests/integration/test-data/contracts.k.expected b/kevm-pyk/src/tests/integration/test-data/contracts.k.expected index df4bcba21f..6df82cb5ff 100644 --- a/kevm-pyk/src/tests/integration/test-data/contracts.k.expected +++ b/kevm-pyk/src/tests/integration/test-data/contracts.k.expected @@ -5170,201 +5170,6 @@ module SYMBOLICSTORE-CONTRACT rule ( #loc ( SymbolicStore . testNumber ) => 0 ) -endmodule - -module TEST-CONTRACT - imports public FOUNDRY - - syntax Contract ::= TestContract - - syntax TestContract ::= "Test" [symbol(), klabel(contract_Test)] - - - - syntax Field ::= TestField - - syntax TestField ::= "IS_TEST" [symbol(), klabel(field_Test_IS_TEST)] - - syntax TestField ::= "_failed" [symbol(), klabel(field_Test__failed)] - - syntax TestField ::= "IS_SCRIPT" [symbol(), klabel(field_Test_IS_SCRIPT)] - - syntax TestField ::= "stdstore" [symbol(), klabel(field_Test_stdstore)] - - rule ( #loc ( Test . IS_TEST ) => 0 ) - - - rule ( #loc ( Test . _failed ) => 0 ) - - - rule ( #loc ( Test . IS_SCRIPT ) => 0 ) - - - rule ( #loc ( Test . stdstore ) => 1 ) - - - syntax Bytes ::= TestContract "." TestMethod [function(), symbol(), klabel(method_Test)] - - syntax TestMethod ::= "IS_SCRIPT" "(" ")" [symbol(), klabel(method_Test_IS_SCRIPT_)] - - syntax TestMethod ::= "IS_TEST" "(" ")" [symbol(), klabel(method_Test_IS_TEST_)] - - syntax TestMethod ::= "failed" "(" ")" [symbol(), klabel(method_Test_failed_)] - - syntax TestMethod ::= "vm" "(" ")" [symbol(), klabel(method_Test_vm_)] - - rule ( Test . IS_SCRIPT ( ) => #abiCallData ( "IS_SCRIPT" , .TypedArgs ) ) - - - rule ( Test . IS_TEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) ) - - - rule ( Test . failed ( ) => #abiCallData ( "failed" , .TypedArgs ) ) - - - rule ( Test . vm ( ) => #abiCallData ( "vm" , .TypedArgs ) ) - - - rule ( selector ( "IS_SCRIPT()" ) => 4174167879 ) - - - rule ( selector ( "IS_TEST()" ) => 4202047188 ) - - - rule ( selector ( "failed()" ) => 3124842406 ) - - - rule ( selector ( "vm()" ) => 980845667 ) - - -endmodule - -module STDERROR-CONTRACT - imports public FOUNDRY - - syntax Contract ::= StdErrorContract - - syntax StdErrorContract ::= "stdError" [symbol(), klabel(contract_stdError)] - - - - syntax Bytes ::= StdErrorContract "." StdErrorMethod [function(), symbol(), klabel(method_stdError)] - - syntax StdErrorMethod ::= "arithmeticError" "(" ")" [symbol(), klabel(method_stdError_arithmeticError_)] - - syntax StdErrorMethod ::= "assertionError" "(" ")" [symbol(), klabel(method_stdError_assertionError_)] - - syntax StdErrorMethod ::= "divisionError" "(" ")" [symbol(), klabel(method_stdError_divisionError_)] - - syntax StdErrorMethod ::= "encodeStorageError" "(" ")" [symbol(), klabel(method_stdError_encodeStorageError_)] - - syntax StdErrorMethod ::= "enumConversionError" "(" ")" [symbol(), klabel(method_stdError_enumConversionError_)] - - syntax StdErrorMethod ::= "indexOOBError" "(" ")" [symbol(), klabel(method_stdError_indexOOBError_)] - - syntax StdErrorMethod ::= "lowLevelError" "(" ")" [symbol(), klabel(method_stdError_lowLevelError_)] - - syntax StdErrorMethod ::= "memOverflowError" "(" ")" [symbol(), klabel(method_stdError_memOverflowError_)] - - syntax StdErrorMethod ::= "popError" "(" ")" [symbol(), klabel(method_stdError_popError_)] - - syntax StdErrorMethod ::= "zeroVarError" "(" ")" [symbol(), klabel(method_stdError_zeroVarError_)] - - rule ( stdError . arithmeticError ( ) => #abiCallData ( "arithmeticError" , .TypedArgs ) ) - - - rule ( stdError . assertionError ( ) => #abiCallData ( "assertionError" , .TypedArgs ) ) - - - rule ( stdError . divisionError ( ) => #abiCallData ( "divisionError" , .TypedArgs ) ) - - - rule ( stdError . encodeStorageError ( ) => #abiCallData ( "encodeStorageError" , .TypedArgs ) ) - - - rule ( stdError . enumConversionError ( ) => #abiCallData ( "enumConversionError" , .TypedArgs ) ) - - - rule ( stdError . indexOOBError ( ) => #abiCallData ( "indexOOBError" , .TypedArgs ) ) - - - rule ( stdError . lowLevelError ( ) => #abiCallData ( "lowLevelError" , .TypedArgs ) ) - - - rule ( stdError . memOverflowError ( ) => #abiCallData ( "memOverflowError" , .TypedArgs ) ) - - - rule ( stdError . popError ( ) => #abiCallData ( "popError" , .TypedArgs ) ) - - - rule ( stdError . zeroVarError ( ) => #abiCallData ( "zeroVarError" , .TypedArgs ) ) - - - rule ( selector ( "arithmeticError()" ) => 2308253967 ) - - - rule ( selector ( "assertionError()" ) => 271788407 ) - - - rule ( selector ( "divisionError()" ) => 4202187332 ) - - - rule ( selector ( "encodeStorageError()" ) => 3512788190 ) - - - rule ( selector ( "enumConversionError()" ) => 501503328 ) - - - rule ( selector ( "indexOOBError()" ) => 99517970 ) - - - rule ( selector ( "lowLevelError()" ) => 2889716422 ) - - - rule ( selector ( "memOverflowError()" ) => 2557239144 ) - - - rule ( selector ( "popError()" ) => 2989344077 ) - - - rule ( selector ( "zeroVarError()" ) => 3061221850 ) - - -endmodule - -module STDMATH-CONTRACT - imports public FOUNDRY - - syntax Contract ::= StdMathContract - - syntax StdMathContract ::= "stdMath" [symbol(), klabel(contract_stdMath)] - - - -endmodule - -module STDSTORAGE-CONTRACT - imports public FOUNDRY - - syntax Contract ::= StdStorageContract - - syntax StdStorageContract ::= "stdStorage" [symbol(), klabel(contract_stdStorage)] - - - - syntax Bytes ::= StdStorageContract "." StdStorageMethod [function(), symbol(), klabel(method_stdStorage)] - - syntax StdStorageMethod ::= "bytesToBytes32" "(" Bytes ":" "bytes" "," Int ":" "uint256" ")" [symbol(), klabel(method_stdStorage_bytesToBytes32_bytes_uint256)] - - rule ( stdStorage . bytesToBytes32 ( V0_b : bytes , V1_offset : uint256 ) => #abiCallData ( "bytesToBytes32" , #bytes ( V0_b ) , #uint256 ( V1_offset ) , .TypedArgs ) ) - ensures ( #rangeUInt ( 128 , lengthBytes ( V0_b ) ) - andBool ( #rangeUInt ( 256 , V1_offset ) - )) - - - rule ( selector ( "bytesToBytes32(bytes,uint256)" ) => 1398294841 ) - - endmodule module TESTNUMBER-CONTRACT @@ -7367,3 +7172,198 @@ module DSTEST-CONTRACT endmodule + +module TEST-CONTRACT + imports public FOUNDRY + + syntax Contract ::= TestContract + + syntax TestContract ::= "Test" [symbol(), klabel(contract_Test)] + + + + syntax Field ::= TestField + + syntax TestField ::= "IS_TEST" [symbol(), klabel(field_Test_IS_TEST)] + + syntax TestField ::= "_failed" [symbol(), klabel(field_Test__failed)] + + syntax TestField ::= "IS_SCRIPT" [symbol(), klabel(field_Test_IS_SCRIPT)] + + syntax TestField ::= "stdstore" [symbol(), klabel(field_Test_stdstore)] + + rule ( #loc ( Test . IS_TEST ) => 0 ) + + + rule ( #loc ( Test . _failed ) => 0 ) + + + rule ( #loc ( Test . IS_SCRIPT ) => 0 ) + + + rule ( #loc ( Test . stdstore ) => 1 ) + + + syntax Bytes ::= TestContract "." TestMethod [function(), symbol(), klabel(method_Test)] + + syntax TestMethod ::= "IS_SCRIPT" "(" ")" [symbol(), klabel(method_Test_IS_SCRIPT_)] + + syntax TestMethod ::= "IS_TEST" "(" ")" [symbol(), klabel(method_Test_IS_TEST_)] + + syntax TestMethod ::= "failed" "(" ")" [symbol(), klabel(method_Test_failed_)] + + syntax TestMethod ::= "vm" "(" ")" [symbol(), klabel(method_Test_vm_)] + + rule ( Test . IS_SCRIPT ( ) => #abiCallData ( "IS_SCRIPT" , .TypedArgs ) ) + + + rule ( Test . IS_TEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) ) + + + rule ( Test . failed ( ) => #abiCallData ( "failed" , .TypedArgs ) ) + + + rule ( Test . vm ( ) => #abiCallData ( "vm" , .TypedArgs ) ) + + + rule ( selector ( "IS_SCRIPT()" ) => 4174167879 ) + + + rule ( selector ( "IS_TEST()" ) => 4202047188 ) + + + rule ( selector ( "failed()" ) => 3124842406 ) + + + rule ( selector ( "vm()" ) => 980845667 ) + + +endmodule + +module STDERROR-CONTRACT + imports public FOUNDRY + + syntax Contract ::= StdErrorContract + + syntax StdErrorContract ::= "stdError" [symbol(), klabel(contract_stdError)] + + + + syntax Bytes ::= StdErrorContract "." StdErrorMethod [function(), symbol(), klabel(method_stdError)] + + syntax StdErrorMethod ::= "arithmeticError" "(" ")" [symbol(), klabel(method_stdError_arithmeticError_)] + + syntax StdErrorMethod ::= "assertionError" "(" ")" [symbol(), klabel(method_stdError_assertionError_)] + + syntax StdErrorMethod ::= "divisionError" "(" ")" [symbol(), klabel(method_stdError_divisionError_)] + + syntax StdErrorMethod ::= "encodeStorageError" "(" ")" [symbol(), klabel(method_stdError_encodeStorageError_)] + + syntax StdErrorMethod ::= "enumConversionError" "(" ")" [symbol(), klabel(method_stdError_enumConversionError_)] + + syntax StdErrorMethod ::= "indexOOBError" "(" ")" [symbol(), klabel(method_stdError_indexOOBError_)] + + syntax StdErrorMethod ::= "lowLevelError" "(" ")" [symbol(), klabel(method_stdError_lowLevelError_)] + + syntax StdErrorMethod ::= "memOverflowError" "(" ")" [symbol(), klabel(method_stdError_memOverflowError_)] + + syntax StdErrorMethod ::= "popError" "(" ")" [symbol(), klabel(method_stdError_popError_)] + + syntax StdErrorMethod ::= "zeroVarError" "(" ")" [symbol(), klabel(method_stdError_zeroVarError_)] + + rule ( stdError . arithmeticError ( ) => #abiCallData ( "arithmeticError" , .TypedArgs ) ) + + + rule ( stdError . assertionError ( ) => #abiCallData ( "assertionError" , .TypedArgs ) ) + + + rule ( stdError . divisionError ( ) => #abiCallData ( "divisionError" , .TypedArgs ) ) + + + rule ( stdError . encodeStorageError ( ) => #abiCallData ( "encodeStorageError" , .TypedArgs ) ) + + + rule ( stdError . enumConversionError ( ) => #abiCallData ( "enumConversionError" , .TypedArgs ) ) + + + rule ( stdError . indexOOBError ( ) => #abiCallData ( "indexOOBError" , .TypedArgs ) ) + + + rule ( stdError . lowLevelError ( ) => #abiCallData ( "lowLevelError" , .TypedArgs ) ) + + + rule ( stdError . memOverflowError ( ) => #abiCallData ( "memOverflowError" , .TypedArgs ) ) + + + rule ( stdError . popError ( ) => #abiCallData ( "popError" , .TypedArgs ) ) + + + rule ( stdError . zeroVarError ( ) => #abiCallData ( "zeroVarError" , .TypedArgs ) ) + + + rule ( selector ( "arithmeticError()" ) => 2308253967 ) + + + rule ( selector ( "assertionError()" ) => 271788407 ) + + + rule ( selector ( "divisionError()" ) => 4202187332 ) + + + rule ( selector ( "encodeStorageError()" ) => 3512788190 ) + + + rule ( selector ( "enumConversionError()" ) => 501503328 ) + + + rule ( selector ( "indexOOBError()" ) => 99517970 ) + + + rule ( selector ( "lowLevelError()" ) => 2889716422 ) + + + rule ( selector ( "memOverflowError()" ) => 2557239144 ) + + + rule ( selector ( "popError()" ) => 2989344077 ) + + + rule ( selector ( "zeroVarError()" ) => 3061221850 ) + + +endmodule + +module STDMATH-CONTRACT + imports public FOUNDRY + + syntax Contract ::= StdMathContract + + syntax StdMathContract ::= "stdMath" [symbol(), klabel(contract_stdMath)] + + + +endmodule + +module STDSTORAGE-CONTRACT + imports public FOUNDRY + + syntax Contract ::= StdStorageContract + + syntax StdStorageContract ::= "stdStorage" [symbol(), klabel(contract_stdStorage)] + + + + syntax Bytes ::= StdStorageContract "." StdStorageMethod [function(), symbol(), klabel(method_stdStorage)] + + syntax StdStorageMethod ::= "bytesToBytes32" "(" Bytes ":" "bytes" "," Int ":" "uint256" ")" [symbol(), klabel(method_stdStorage_bytesToBytes32_bytes_uint256)] + + rule ( stdStorage . bytesToBytes32 ( V0_b : bytes , V1_offset : uint256 ) => #abiCallData ( "bytesToBytes32" , #bytes ( V0_b ) , #uint256 ( V1_offset ) , .TypedArgs ) ) + ensures ( #rangeUInt ( 128 , lengthBytes ( V0_b ) ) + andBool ( #rangeUInt ( 256 , V1_offset ) + )) + + + rule ( selector ( "bytesToBytes32(bytes,uint256)" ) => 1398294841 ) + + +endmodule diff --git a/kevm-pyk/src/tests/integration/test-data/foundry.k.expected b/kevm-pyk/src/tests/integration/test-data/foundry.k.expected index 973b6cca25..4bf6dace98 100644 --- a/kevm-pyk/src/tests/integration/test-data/foundry.k.expected +++ b/kevm-pyk/src/tests/integration/test-data/foundry.k.expected @@ -61,10 +61,6 @@ module FOUNDRY-MAIN imports public STORETEST-VERIFICATION imports public SYMBOLICSTORAGETEST-VERIFICATION imports public SYMBOLICSTORE-VERIFICATION - imports public TEST-VERIFICATION - imports public STDERROR-VERIFICATION - imports public STDMATH-VERIFICATION - imports public STDSTORAGE-VERIFICATION imports public TESTNUMBER-VERIFICATION imports public TOSTRINGTEST-VERIFICATION imports public TOKEN-VERIFICATION @@ -74,6 +70,10 @@ module FOUNDRY-MAIN imports public CONSOLE-VERIFICATION imports public CONSOLE2-VERIFICATION imports public DSTEST-VERIFICATION + imports public TEST-VERIFICATION + imports public STDERROR-VERIFICATION + imports public STDMATH-VERIFICATION + imports public STDSTORAGE-VERIFICATION @@ -493,92 +493,92 @@ module SYMBOLICSTORE-VERIFICATION endmodule -module TEST-VERIFICATION - imports public TEST-CONTRACT +module TESTNUMBER-VERIFICATION + imports public TESTNUMBER-CONTRACT endmodule -module STDERROR-VERIFICATION - imports public STDERROR-CONTRACT +module TOSTRINGTEST-VERIFICATION + imports public TOSTRINGTEST-CONTRACT endmodule -module STDMATH-VERIFICATION - imports public STDMATH-CONTRACT +module TOKEN-VERIFICATION + imports public TOKEN-CONTRACT endmodule -module STDSTORAGE-VERIFICATION - imports public STDSTORAGE-CONTRACT +module BYTESTYPETEST-VERIFICATION + imports public BYTESTYPETEST-CONTRACT endmodule -module TESTNUMBER-VERIFICATION - imports public TESTNUMBER-CONTRACT +module UINTTYPETEST-VERIFICATION + imports public UINTTYPETEST-CONTRACT endmodule -module TOSTRINGTEST-VERIFICATION - imports public TOSTRINGTEST-CONTRACT +module VM-VERIFICATION + imports public VM-CONTRACT endmodule -module TOKEN-VERIFICATION - imports public TOKEN-CONTRACT +module CONSOLE-VERIFICATION + imports public CONSOLE-CONTRACT endmodule -module BYTESTYPETEST-VERIFICATION - imports public BYTESTYPETEST-CONTRACT +module CONSOLE2-VERIFICATION + imports public CONSOLE2-CONTRACT endmodule -module UINTTYPETEST-VERIFICATION - imports public UINTTYPETEST-CONTRACT +module DSTEST-VERIFICATION + imports public DSTEST-CONTRACT endmodule -module VM-VERIFICATION - imports public VM-CONTRACT +module TEST-VERIFICATION + imports public TEST-CONTRACT endmodule -module CONSOLE-VERIFICATION - imports public CONSOLE-CONTRACT +module STDERROR-VERIFICATION + imports public STDERROR-CONTRACT endmodule -module CONSOLE2-VERIFICATION - imports public CONSOLE2-CONTRACT +module STDMATH-VERIFICATION + imports public STDMATH-CONTRACT endmodule -module DSTEST-VERIFICATION - imports public DSTEST-CONTRACT +module STDSTORAGE-VERIFICATION + imports public STDSTORAGE-CONTRACT diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_false.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_false.expected index 0dd76ca495..43bc247e68 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_false.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_false.expected @@ -677,4 +677,6 @@ module SUMMARY-ASSERTTEST.TESTFAIL-ASSERT-FALSE:D9767505A49B578A77DD3E9B8A9FE01E endmodule 0 Failure nodes. (0 pending and 0 failing) +Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN + Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/ diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_true.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_true.expected index 57751dde23..1fdfa7533c 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_true.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_true.expected @@ -894,7 +894,11 @@ Failing nodes: #And { true #Equals NUMBER_CELL:Int <=Int maxSInt256 } ) ) ) ) ) #Implies { false #Equals foundry_success ( ... statusCode: EVMC_SUCCESS , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } ) Path condition: #Top + Model: + CALLER_ID = 0 + NUMBER_CELL = 0 + ORIGIN_ID = 0 -Join the Runtime Verification Discord server for support: https://discord.gg/GHvFbRDD +Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/ diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert.expected index 2e29e14284..e00aaefd38 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert.expected @@ -1350,7 +1350,11 @@ Failing nodes: #And { true #Equals NUMBER_CELL:Int <=Int maxSInt256 } ) ) ) ) ) #Implies { false #Equals foundry_success ( ... statusCode: EVMC_SUCCESS , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } ) Path condition: #Top + Model: + CALLER_ID = 0 + NUMBER_CELL = 0 + ORIGIN_ID = 0 -Join the Runtime Verification Discord server for support: https://discord.gg/GHvFbRDD +Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/ diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_false.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_false.expected index 53da19d3b0..5e96fc6a4c 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_false.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_false.expected @@ -894,7 +894,11 @@ Failing nodes: #And { true #Equals NUMBER_CELL:Int <=Int maxSInt256 } ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_REVERT , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } ) Path condition: #Top + Model: + CALLER_ID = 0 + NUMBER_CELL = 0 + ORIGIN_ID = 0 -Join the Runtime Verification Discord server for support: https://discord.gg/GHvFbRDD +Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/ diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_true.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_true.expected index b215c638a6..c208d49b13 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_true.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_true.expected @@ -677,4 +677,6 @@ module SUMMARY-ASSERTTEST.TEST-ASSERT-TRUE:E200EADD2408C03C6CCDB315095224AC1D58D endmodule 0 Failure nodes. (0 pending and 0 failing) +Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN + Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/ diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_failing_branch.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_failing_branch.expected index c446c45780..face631f8b 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_failing_branch.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_failing_branch.expected @@ -1793,7 +1793,12 @@ Failing nodes: #And { true #Equals VV0_x_114b9705:Int 1 ) , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } ) Path condition: #Top + Model: + CALLER_ID = 0 + NUMBER_CELL = 0 + ORIGIN_ID = 0 + VV0_a_114b9705 = 1 + VV1_b_114b9705 = 0 -Join the Runtime Verification Discord server for support: https://discord.gg/GHvFbRDD +Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/ diff --git a/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N.expected b/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N.expected index 4f70655352..706ade2e5c 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N.expected @@ -2102,4 +2102,6 @@ module SUMMARY-LOOPSTEST.SUM-N:062CC914DAA13A8EAF189DADDC9178CE923938A59F8855C3A endmodule 0 Failure nodes. (0 pending and 0 failing) +Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN + Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/ diff --git a/kevm-pyk/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize.expected b/kevm-pyk/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize.expected index a5088bf6bd..cc7b6297ef 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize.expected @@ -731,4 +731,6 @@ module SUMMARY-SETUPDEPLOYTEST.TEST-EXTCODESIZE:F212E6B5B768844563A8F6DD11A90162 endmodule 0 Failure nodes. (0 pending and 0 failing) +Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN + Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/