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 generation and use the same message for both types of calls.
This issue isn't critical because the message for unknown calls is used only for tracing purposes, and most unknown calls use the CALL scheme. However, the trace information could be incorrect or confusing if there are unknown calls via DELEGATECALL.
Note: the message generation code is updated by PR #336, but this issue is orthogonal, and can be fixed after merging the PR.
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 generation and use the same message for both types of calls.
Message for known calls: https://github.com/a16z/halmos/blob/f7ff1f8323207334c35da1542005ae4b77d23ae3/src/halmos/sevm.py#L1579-L1586
Message for unknown calls: https://github.com/a16z/halmos/blob/f7ff1f8323207334c35da1542005ae4b77d23ae3/src/halmos/sevm.py#L1776-L1782
This issue isn't critical because the message for unknown calls is used only for tracing purposes, and most unknown calls use the CALL scheme. However, the trace information could be incorrect or confusing if there are unknown calls via DELEGATECALL.
Note: the message generation code is updated by PR #336, but this issue is orthogonal, and can be fixed after merging the PR.