Daejun Park
Daejun Park
**Problem** Currently, an arbitrary external call can be made using a low-level call, e.g., ``` data = svm.createBytes(1024, "data"); address(target).call(data); ``` However, if the `target` contract contains an external function...
When a call target address may be aliased with multiple existing addresses, or may be non-existent, explicitly branching into multiple paths for each potential alias or non-existent address. Although this...
todo for v0.2.x: - [ ] network state inspection issues: - [ ] #178 - [ ] #180 - [ ] #217 - [ ] #290 - [x] #338 -...
I suggest dropping the `--bytecode` pipeline. It doesn't seem to be used much, but it does increase code maintenance costs. Additionally, considering all the configurations needed to run a given...
Currently, the message generation for calls to known and unknown addresses is inconsistent, with the message for known calls being correct. It would be better to factor out the message...
in the next SMT-LIB version 2.7, [overflow predicates](https://github.com/SMT-LIB/SMT-LIB-2/blob/7ab2e94704fb0de8bb01b44600998303608a4354/Theories/FixedSizeBitVectors.smt2#L206-L216) will be added. use these overflow predicates instead of compiler-generated conditions, e.g., `y != 0 and x * y / y !=...
when a concrete value is required, now it attempts to concretize a given symbolic term by replacing its (sub)terms with their corresponding concrete values, based on the current path condition....
functional correctness test for the withdrawal requests queue contract in [eip-7002](https://eips.ethereum.org/EIPS/eip-7002) geas implementation: https://github.com/lightclient/sys-asm/blob/main/src/withdrawals/main.eas
[wip] test to verify functional correctness of the [eip-2935](https://eips.ethereum.org/EIPS/eip-2935) ring buffer contract, as included in the [Pectra system contracts bytecode audit RFP](https://github.com/ethereum/requests-for-proposals/blob/master/open-rfps/pectra-system-contracts-audit.md).
## Motivation This PR improves symbolic tests using new halmos cheatcode `createCalldata()`. Previously, symbolic tests required custom calldata generators to handle dynamic-sized arrays and bytes. The new `createCalldata()` cheatcode now...