Closed HNYuuu closed 3 years ago
The memory model is too complicated, especially the reverse the concat resulted from the little endian and big endian.
可以考虑在运行过程中不保证 memory 的正确性，但是在输入输出时保持信息的正确性。因为 Z3 造成的 Extract 和 Concat 造成了可读性严重下降。
在 0452189 中解决了内存的两个问题：
HNYuuu
commented
3 years ago HNYuuu
commented
3 years ago
The memory model is too complicated, especially the reverse the concat resulted from the little endian and big endian.
可以考虑在运行过程中不保证 memory 的正确性，但是在输入输出时保持信息的正确性。因为 Z3 造成的 Extract 和 Concat 造成了可读性严重下降。