We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
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
The current implementation of _sym_get_input_byte in the simple backend is:
_sym_get_input_byte
Z3_ast _sym_get_input_byte(size_t offset, uint8_t) { static std::vector<SymExpr> stdinBytes; if (offset < stdinBytes.size()) return stdinBytes[offset]; auto varName = "stdin" + std::to_string(stdinBytes.size()); auto *var = build_variable(varName.c_str(), 8); stdinBytes.resize(offset); stdinBytes.push_back(var); return var; }
This does not work well in the case of lseek/fseek operations:
lseek/fseek
*seek
offset < stdinBytes.size()
Moreover, the varName should likely be "stdin" + std::to_string(offset) to be more intuitive.
varName
"stdin" + std::to_string(offset)
Am I right?
Let me know if this could be a reasonable fix (or how to improve it).
The text was updated successfully, but these errors were encountered:
No branches or pull requests
The current implementation of
_sym_get_input_byte
in the simple backend is:This does not work well in the case of
lseek/fseek
operations:*seek
operation moves the offset to X > 0offset < stdinBytes.size()
will then make return NULL for entries before XMoreover, the
varName
should likely be"stdin" + std::to_string(offset)
to be more intuitive.Am I right?
Let me know if this could be a reasonable fix (or how to improve it).
The text was updated successfully, but these errors were encountered: