strlen running on a symbolic string.scanf implementation is not complete, but if you just need to support a single, known format string, you can write a hook to do exactly that.project.hook) to make the required modifications to the state in an ad-hoc way.state.posix.queued_syscall_returns list to queue syscall return values. If a return value is queued, the system call will not be executed, and the value will be used instead. Furthermore, a function can be queued instead as the "return value", which will result in that function being applied to the state when the system call is triggered.state.memory.read() and write() might run into a situation where the length of a buffer is symbolic. In general, this is handled very poorly: in many cases, this length will end up being concretized outright or retroactively concretized in later steps of execution. Even in cases when it is not, the source or destination file might end up looking a bit "weird".