Open ercoppa opened 1 year ago
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 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).