Fix test_jumpdest_analysis which was previously not meaningful, as it only verified that jumpdest_analysis never aborted though that can't happen. Now, it verifies the correctness of SEGMENT_JUMPDEST_BITS and of jumpdest_table.
Introduce test_packed_verification.
The PR addresses the bugs uncovered during these tests, primarily:
Utilizing the current context instead of the one in the stack in PROVER_INPUT(jumpdest_table::).
Correcting the prefix computation in the packed verification of write_table_if_jumpdest.
This PR incorporates the following changes:
test_jumpdest_analysis
which was previously not meaningful, as it only verified thatjumpdest_analysis
never aborted though that can't happen. Now, it verifies the correctness ofSEGMENT_JUMPDEST_BITS
and ofjumpdest_table
.test_packed_verification
.The PR addresses the bugs uncovered during these tests, primarily:
PROVER_INPUT(jumpdest_table::)
.write_table_if_jumpdest
.