Fix concurrent traces generated via --trace #697
Conversation
src/goto-symex/build_goto_trace.cpp
Outdated
| @@ -286,6 +294,19 @@ void build_goto_trace( | |||
| for(auto &t_it : time_map) | |||
| goto_trace.steps.splice(goto_trace.steps.end(), t_it.second); | |||
|
|
|||
| // cut off the trace at the desired end or after the first failed | |||
There was a problem hiding this comment.
In test generation, wouldn't we cut off traces that cover several test goals at the first goal that is reached? We would like to see the full trace to the end of the SSA.
There was a problem hiding this comment.
It's going to cut them off at the specified end, which will be set individually for each goal.
There was a problem hiding this comment.
The problem is that we need observe the output behaviour beyond the goal.
There was a problem hiding this comment.
The current code (before this PR) doesn't actually do this, does it?!
There was a problem hiding this comment.
In the current code I can call the first variant of build_goto_trace() that does not truncate.
tautschnig
force-pushed
the
concurrency-trace
branch
2 times, most recently
from
b54d79b to
fd1987f
Compare
|
I have now restored the previous behaviour, my apologies for missing that aspect. |
Traces had been cut off at the failing assertion without considering steps performed in threads with a higher thread id. The behaviour of --stop-on-fail was correct in this regard. The trace trimming must only be performed after re-ordering of steps according to their time stamps.
tautschnig
force-pushed
the
concurrency-trace
branch
from
fd1987f to
7fd6180
Compare
Traces had been cut off at the failing assertion without considering steps
performed in threads with a higher thread id. The behaviour of --stop-on-fail
was correct in this regard. The trace trimming must only be performed after
re-ordering of steps according to their time stamps.