The idea is to allow extra logging while tracing. This is then also considered while retracing.
Approach: Manually instrument the original source code with the following macros:
LOG_INTEGER( i );
LOG_STRING( s );
LOG_DATA( buf, size );
Basically, the trace format allows that already by using _TRACE_SET_LEN_x, _TRACE_SET_LEN_STRING and _TRACE_SET_LEN_PREFIX for integers, null-terminated strings and data with size up to 255 bits (logging data with a bigger size would not be helpful anyways). So the remaining steps are:
[ ] Define those macros in a new C header. When size is bigger than 255 bits, the compiler should fail with an exception.
[ ] Match and constrain the symbolic execution with logged data wile retracing.
The idea is to allow extra logging while tracing. This is then also considered while retracing.
Approach: Manually instrument the original source code with the following macros:
Basically, the trace format allows that already by using
_TRACE_SET_LEN_x,_TRACE_SET_LEN_STRINGand_TRACE_SET_LEN_PREFIXfor integers, null-terminated strings and data with size up to 255 bits (logging data with a bigger size would not be helpful anyways). So the remaining steps are: