Skip to content

Better results printing, WARNING-s make the check FAIL now. #645

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 5 commits into from
Feb 10, 2025
Merged

Better results printing, WARNING-s make the check FAIL now. #645

merged 5 commits into from
Feb 10, 2025

Conversation

msooseth
Copy link
Collaborator

@msooseth msooseth commented Feb 3, 2025 •
edited
Loading

Description

Cleaner, better results printing. Should fix #644 I believe.

We promotes all warnings to FAIL and also collect all warnings into a single place. We also strip away some of the detail of the warnings, so as to be able to collect them. This should give a better overview to the user. Functions also return more details about what happened -- only Cex or and/or also warnings.

With the use of --debug, all information should still be present, although that also turns on other data printing. Also, --verbose 2 increases the amount of data printed.

Example output:

cabal run exe:hevm test -- --solver bitwuzla --root tmp
Checking 1 function(s) in contract src/array.sol:ArrayTest
[RUNNING] prove_initial_values(address)
   [PASS] prove_initial_values

Checking 1 function(s) in contract src/bail.sol:CounterTest
   [BAIL] setUp()
   Failure: setUp

Checking 1 function(s) in contract src/contract-allrevert-expected.sol:MyContract
[RUNNING] proveFail_allrevert_expected(uint256)
   [PASS] proveFail_allrevert_expected

Checking 2 function(s) in contract src/contract-allrevert-somenot.sol:MyContract
[RUNNING] prove_allrevert_somenot_thisrevert(uint256)
   [FAIL] prove_allrevert_somenot_thisrevert
   No reachable assertion violations, but all branches reverted

[RUNNING] prove_allrevert_somenot_thisok(uint256)
   [PASS] prove_allrevert_somenot_thisok

Checking 1 function(s) in contract src/contract-allrevert.sol:MyContract
[RUNNING] prove_allrevert(uint256)
   [FAIL] prove_allrevert
   No reachable assertion violations, but all branches reverted

Checking 2 function(s) in contract src/contract-dual-diff-func-fail.sol:MyContract
[RUNNING] prove_dual_diff_func1(address,uint256)
   [FAIL] prove_dual_diff_func1
   Counterexample:
     calldata: prove_dual_diff_func1(0x0000000000000000000000000000000000001312,0)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001

[RUNNING] prove_dual_diff_func2(address,uint256)
   [FAIL] prove_dual_diff_func2
   Counterexample:
     calldata: prove_dual_diff_func2(0x68ff998EA2Af224dF43739204600c7b1c22CF173,0)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001

Checking 1 function(s) in contract src/contract-dualfail.sol:MyContract
[RUNNING] prove_dualfail(address,uint256,bool)
   [FAIL] prove_dualfail
   Counterexample:
     calldata: prove_dualfail(0x68ff998EA2Af224dF43739204600c7b1c22CF173,0,false)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
   Counterexample:
     calldata: prove_dualfail(0x1Fc75cE88bBfA0Cf8ED7895D06bC9bD7c10446D0,100,true)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001

Checking 1 function(s) in contract src/contract-fail.sol:MyContract
[RUNNING] prove_single_fail(address,uint256)
   [FAIL] prove_single_fail
   Counterexample:
     calldata: prove_single_fail(0x68ff998EA2Af224dF43739204600c7b1c22CF173,100)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001

Checking 2 function(s) in contract src/contract-maxiters.sol:MyContract
[RUNNING] prove_maxiters_fail(uint256)
   [FAIL] prove_maxiters_fail
   Counterexample:
     calldata: prove_maxiters_fail(1)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
   Counterexample:
     calldata: prove_maxiters_fail(2)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
   Counterexample:
     calldata: prove_maxiters_fail(3)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
   Counterexample:
     calldata: prove_maxiters_fail(4)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
   Counterexample:
     calldata: prove_maxiters_fail(5)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
   [WARNING] hevm was only able to partially explore the test prove_maxiters_fail due to:
      1x -> Max iterations reached

[RUNNING] prove_maxiters_pass(uint256)
   [FAIL] prove_maxiters_pass
   [WARNING] hevm was only able to partially explore the test prove_maxiters_pass due to:
      1x -> Max iterations reached

Checking 3 function(s) in contract src/contract-tuple.sol:TupleTest
[RUNNING] prove_tuple_pass((uint256,uint256))
   [PASS] prove_tuple_pass

[RUNNING] prove_tuple_pass2(uint256)
   [FAIL] prove_tuple_pass2
   Counterexample:
     calldata: prove_tuple_pass2(0)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001

[RUNNING] prove_tuple_pass1(uint256[5])
   [FAIL] prove_tuple_pass1
   [WARNING] hevm was only able to partially explore the test prove_tuple_pass1 due to:
      1x -> Max iterations reached

Checking 7 function(s) in contract src/contract-warning-test.sol:WarningTest
[RUNNING] prove_pass(address,uint256)
   [PASS] prove_pass

[RUNNING] prove_error(uint256,uint256)
   [FAIL] prove_error
   Counterexample:
     calldata: prove_error(25173922555380183645638385500893615303049966126758775732690850302391767811982,0)
     result:   Revert: 0x08c379a000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000010617373657274696f6e206661696c656400000000000000000000000000000000

[RUNNING] prove_nowarning(uint256,uint256)
   [PASS] prove_nowarning

[RUNNING] prove_neq_err(uint256,uint256,uint256)
   [FAIL] prove_neq_err
   Counterexample:
     calldata: prove_neq_err(83069967174038281357423878005237569229684958459579057752419642306348332631750,5397595266073016138606877540314514970882693664868321159911210053934947991075,0)
     result:   Revert: 0x08c379a0000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000000000000000005de617373657274696f6e206661696c65643a20416464202852656164576f726420284c69742030783429202857726974654279746520284c6974203078302920284c6974427974652031383029202857726974654279746520284c6974203078312920284c69744279746520363429202857726974654279746520284c6974203078322920284c69744279746520363529202857726974654279746520284c6974203078332920284c697442797465203138302920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c69742030783434292028566172202261726733222920284162737472616374427566202274786461746122292929292929292929202852656164576f726420284c6974203078323429202857726974654279746520284c6974203078302920284c6974427974652031383029202857726974654279746520284c6974203078312920284c69744279746520363429202857726974654279746520284c6974203078322920284c69744279746520363529202857726974654279746520284c6974203078332920284c697442797465203138302920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c69742030783434292028566172202261726733222920284162737472616374427566202274786461746122292929292929292929203d3d204164642028416464202852656164576f726420284c69742030783429202857726974654279746520284c6974203078302920284c6974427974652031383029202857726974654279746520284c6974203078312920284c69744279746520363429202857726974654279746520284c6974203078322920284c69744279746520363529202857726974654279746520284c6974203078332920284c697442797465203138302920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c69742030783434292028566172202261726733222920284162737472616374427566202274786461746122292929292929292929202852656164576f726420284c6974203078323429202857726974654279746520284c6974203078302920284c6974427974652031383029202857726974654279746520284c6974203078312920284c69744279746520363429202857726974654279746520284c6974203078322920284c69744279746520363529202857726974654279746520284c6974203078332920284c697442797465203138302920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c6974203078343429202856617220226172673322292028416273747261637442756620227478646174612229292929292929292929202852656164576f726420284c6974203078343429202857726974654279746520284c6974203078302920284c6974427974652031383029202857726974654279746520284c6974203078312920284c69744279746520363429202857726974654279746520284c6974203078322920284c69744279746520363529202857726974654279746520284c6974203078332920284c697442797465203138302920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c697420307834342920285661722022617267332229202841627374726163744275662022747864617461222929292929292929290000

[RUNNING] prove_warning(uint256,uint256)
   [FAIL] prove_warning
   [WARNING] hevm was only able to partially explore the test prove_warning due to:
      1x -> Cheat code not recognized: 0xa34edc03

[RUNNING] prove_eq_err(uint256,uint256,uint256)
   [FAIL] prove_eq_err
   Counterexample:
     calldata: prove_eq_err(6001462241313440279023509686965327350052394016037884181451393767007176329987,100683714417225924436450220748851770471552383019376852689494373071001143153056,5397595266073016138606877540314514970882693664868321159911210053934947991075)
     result:   Revert: 0x08c379a0000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000000000000000005d9617373657274696f6e206661696c65643a20416464202852656164576f726420284c69742030783429202857726974654279746520284c6974203078302920284c6974427974652032353029202857726974654279746520284c6974203078312920284c69744279746520353829202857726974654279746520284c6974203078322920284c69744279746520313029202857726974654279746520284c6974203078332920284c6974427974652038362920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c69742030783434292028566172202261726733222920284162737472616374427566202274786461746122292929292929292929202852656164576f726420284c6974203078323429202857726974654279746520284c6974203078302920284c6974427974652032353029202857726974654279746520284c6974203078312920284c69744279746520353829202857726974654279746520284c6974203078322920284c69744279746520313029202857726974654279746520284c6974203078332920284c6974427974652038362920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c6974203078343429202856617220226172673322292028416273747261637442756620227478646174612229292929292929292920213d204164642028416464202852656164576f726420284c69742030783429202857726974654279746520284c6974203078302920284c6974427974652032353029202857726974654279746520284c6974203078312920284c69744279746520353829202857726974654279746520284c6974203078322920284c69744279746520313029202857726974654279746520284c6974203078332920284c6974427974652038362920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c69742030783434292028566172202261726733222920284162737472616374427566202274786461746122292929292929292929202852656164576f726420284c6974203078323429202857726974654279746520284c6974203078302920284c6974427974652032353029202857726974654279746520284c6974203078312920284c69744279746520353829202857726974654279746520284c6974203078322920284c69744279746520313029202857726974654279746520284c6974203078332920284c6974427974652038362920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c6974203078343429202856617220226172673322292028416273747261637442756620227478646174612229292929292929292929202852656164576f726420284c6974203078343429202857726974654279746520284c6974203078302920284c6974427974652032353029202857726974654279746520284c6974203078312920284c69744279746520353829202857726974654279746520284c6974203078322920284c69744279746520313029202857726974654279746520284c6974203078332920284c6974427974652038362920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c6974203078343429202856617220226172673322292028416273747261637442756620227478646174612229292929292929292900000000000000

[RUNNING] prove_gt_err(uint256,uint256,uint256)
   [FAIL] prove_gt_err
   Counterexample:
     calldata: prove_gt_err(5397595266073016138606877540314514970882693664868321159911210053934947991075,108970859186521381540973502124676709860296732671658764050925208989247680527467,0)
     result:   Revert: 0x08c379a0000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000000000000000005de617373657274696f6e206661696c65643a20416464202852656164576f726420284c69742030783429202857726974654279746520284c6974203078302920284c6974427974652032353429202857726974654279746520284c6974203078312920284c69744279746520373229202857726974654279746520284c6974203078322920284c6974427974652031363429202857726974654279746520284c6974203078332920284c6974427974652038382920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c69742030783434292028566172202261726733222920284162737472616374427566202274786461746122292929292929292929202852656164576f726420284c6974203078323429202857726974654279746520284c6974203078302920284c6974427974652032353429202857726974654279746520284c6974203078312920284c69744279746520373229202857726974654279746520284c6974203078322920284c6974427974652031363429202857726974654279746520284c6974203078332920284c6974427974652038382920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c69742030783434292028566172202261726733222920284162737472616374427566202274786461746122292929292929292929203c3d204164642028416464202852656164576f726420284c69742030783429202857726974654279746520284c6974203078302920284c6974427974652032353429202857726974654279746520284c6974203078312920284c69744279746520373229202857726974654279746520284c6974203078322920284c6974427974652031363429202857726974654279746520284c6974203078332920284c6974427974652038382920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c69742030783434292028566172202261726733222920284162737472616374427566202274786461746122292929292929292929202852656164576f726420284c6974203078323429202857726974654279746520284c6974203078302920284c6974427974652032353429202857726974654279746520284c6974203078312920284c69744279746520373229202857726974654279746520284c6974203078322920284c6974427974652031363429202857726974654279746520284c6974203078332920284c6974427974652038382920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c6974203078343429202856617220226172673322292028416273747261637442756620227478646174612229292929292929292929202852656164576f726420284c6974203078343429202857726974654279746520284c6974203078302920284c6974427974652032353429202857726974654279746520284c6974203078312920284c69744279746520373229202857726974654279746520284c6974203078322920284c6974427974652031363429202857726974654279746520284c6974203078332920284c6974427974652038382920285772697465576f726420284c697420307834292028566172202261726731222920285772697465576f726420284c69742030783234292028566172202261726732222920285772697465576f726420284c697420307834342920285661722022617267332229202841627374726163744275662022747864617461222929292929292929290000

Checking 1 function(s) in contract src/karmacoma-loop.sol:TestLoop
[RUNNING] prove_loopBound(uint256)
   [FAIL] prove_loopBound
   [WARNING] hevm was only able to partially explore the test prove_loopBound due to:
      1x -> Max iterations reached

Checking 1 function(s) in contract src/maxloop-thing.sol:MaxLoopTokenTest
[RUNNING] prove_maxloop_transfer(address,uint256)
   [FAIL] prove_maxloop_transfer
   Counterexample:
     calldata: prove_maxloop_transfer(0x0000000000FFFFFffFfFffFfFFFfFFFfffffFffF,42)
     result:   Revert: 0x08c379a000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000b86617373657274696f6e206661696c65643a20537562202852656164576f726420284c6974203078302920285772697465576f726420284c697420307830292028534c6f616420284b656363616b20285772697465576f726420284c6974203078302920285741646472202853796d41646472202263616c6c65722229292028436f6e637265746542756620225c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c222929292028436f6e637265746553746f7265202866726f6d4c697374205b283078616433323238623637366637643363643432383461353434336631376631393632623336653439316233306134306232343035383439653539376261356662352c3078336538295d2929292028436f6e6372657465427566202222292929202852656164576f726420284c6974203078323429202857726974654279746520284c6974203078302920284c6974427974652031333529202857726974654279746520284c6974203078312920284c69744279746520393529202857726974654279746520284c6974203078322920284c6974427974652031323929202857726974654279746520284c6974203078332920284c6974427974652036362920285772697465576f726420284c6974203078342920285741646472202853796d4164647220226172673122292920285772697465576f726420284c69742030783234292028566172202261726732222920284162737472616374427566202274786461746122292929292929292920213d2052656164576f726420284c6974203078302920285772697465576f726420284c697420307830292028534c6f616420284b656363616b20285772697465576f726420284c6974203078302920285741646472202853796d41646472202263616c6c65722229292028436f6e637265746542756620225c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c2229292920285353746f726520284b656363616b2028436f7079536c69636520284c6974203078302920284c6974203078302920284c697420307834302920285772697465576f726420284c697420307830292028416e6420284c697420307866666666666666666666666666666666666666666666666666666666666666666666666666666666292028416e6420284c697420307866666666666666666666666666666666666666666666666666666666666666666666666666666666292028416e6420284c69742030786666666666666666666666666666666666666666666666666666666666666666666666666666666629202852656164576f726420284c69742030783429202857726974654279746520284c6974203078302920284c6974427974652031333529202857726974654279746520284c6974203078312920284c69744279746520393529202857726974654279746520284c6974203078322920284c6974427974652031323929202857726974654279746520284c6974203078332920284c6974427974652036362920285772697465576f726420284c6974203078342920285741646472202853796d4164647220226172673122292920285772697465576f726420284c6974203078323429202856617220226172673222292028416273747261637442756620227478646174612229292929292929292929292028436f6e637265746542756620225c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c3132382229292028436f6e637265746542756620222229292920284164642028534c6f616420284b656363616b20285772697465576f726420284c6974203078302920285741646472202853796d416464722022617267312229292028436f6e637265746542756620225c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c5c4e554c222929292028436f6e637265746553746f7265202866726f6d4c697374205b283078616433323238623637366637643363643432383461353434336631376631393632623336653439316233306134306232343035383439653539376261356662352c3078336538295d292929202852656164576f726420284c6974203078323429202857726974654279746520284c6974203078302920284c6974427974652031333529202857726974654279746520284c6974203078312920284c69744279746520393529202857726974654279746520284c6974203078322920284c6974427974652031323929202857726974654279746520284c6974203078332920284c6974427974652036362920285772697465576f726420284c6974203078342920285741646472202853796d4164647220226172673122292920285772697465576f726420284c697420307832342920285661722022617267322229202841627374726163744275662022747864617461222929292929292929292028436f6e637265746553746f7265202866726f6d4c697374205b283078616433323238623637366637643363643432383461353434336631376631393632623336653439316233306134306232343035383439653539376261356662352c3078336538295d292929292028436f6e637265746542756620222229290000000000000000000000000000000000000000000000000000

Checking 1 function(s) in contract src/minivat.sol:MiniVatTest
[RUNNING] prove_invariant_fixed()
   [FAIL] prove_invariant_fixed
   Counterexample:
     calldata: prove_invariant_fixed()
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001

Checking 1 function(s) in contract src/out-of-bounds.sol:OutOfBounds
[RUNNING] prove_fun(uint8)
   [PASS] prove_fun

Checking 1 function(s) in contract src/symbolic-copyslice.sol:CopySlice
[RUNNING] prove_copyslice(uint256,uint256)
   [FAIL] prove_copyslice
   [WARNING] hevm was only able to partially explore the test prove_copyslice due to:
      2x -> CopySlice with a symbolically sized region not currently implemented, cannot execute SMT solver on this query

Checklist

  • tested locally
  • added automated tests
  • updated the docs
  • updated the changelog

@msooseth msooseth mentioned this pull request Feb 3, 2025
Closed
@msooseth msooseth force-pushed the better-results-printing branch from e7326c9 to 13ecf37 Compare February 3, 2025 17:50
@msooseth msooseth force-pushed the better-results-printing branch from 646f09b to 588ad21 Compare February 3, 2025 18:13
@msooseth msooseth force-pushed the better-results-printing branch from 69afe44 to e405cdc Compare February 4, 2025 14:18
@msooseth msooseth changed the title [DRAFT] Better results printing Better results printing Feb 4, 2025
@msooseth msooseth marked this pull request as ready for review February 4, 2025 14:45
@msooseth msooseth requested a review from blishko February 4, 2025 14:46
blishko
blishko approved these changes Feb 6, 2025
View reviewed changes
Copy link
Collaborator

@blishko blishko left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems OK to me. Maybe feedback from the users would be helpful here.

@msooseth
Copy link
Collaborator Author

msooseth commented Feb 6, 2025

Hmm.... I think I'll update the docs regarding this and then merge. I see your point about users. This is in fact in response to a user-reported issue. But it might better to ask more users.... I'll do that in a sec.

@msooseth msooseth changed the title Better results printing Better results printing, WARNING-s make the check FAIL now. Feb 6, 2025
@msooseth
Copy link
Collaborator Author

I got positive feedback from another user, so I'm merging. Let's see how it goes... :)

@msooseth msooseth merged commit 1bd1ba4 into main Feb 10, 2025
9 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@blishko blishko blishko approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

add way to promote warnings to errors
2 participants
@msooseth @blishko