Feature #7264
closedEMG should generate ldv_thread_join with two arguments
0%
Description
For our analysis it is important to know what function is joined. The pointer to the function executed in the joined thread should be transferred as a second argument of the function ldv_thread_join.
Updated by Evgeny Novikov almost 8 years ago
What are you going to do with programs that haven't specially prepared environments that in particular include everything related with threads management?
Updated by Pavel Andrianov almost 8 years ago
The general approach certainly has to track thread pointers, but it is not efficient enough, thus now we are focusing on the simplified task.
Updated by Ilja Zakharov almost 8 years ago
- Status changed from New to Resolved
Implemented in branch 'thread-join-fix'.
Updated by Evgeny Novikov almost 8 years ago
- Status changed from Resolved to Closed
- Published in build set to 54d9b77
I merged the branch to master in 54d9b77 and just wondering why we need to provide such the stub implementation of ldv_thread*() functions, i.e. who wins something from it and why not just provide corresponding function declarations.
Updated by Pavel Andrianov almost 8 years ago
The stub implementation was used in the first versions of the analysis. Then the problem of recursion occurred and we had to support special thread-create constructions in CPAchecker. Thus, now the implementations are not necessary, just calls. However, if the function is used, it is more correct to provide an implementation, even it is a stub. Less undefined functions!
Updated by Evgeny Novikov almost 8 years ago
Well, let's leave them as is now. I just cared how to use some other implementations but this is likely a concern of an new upcoming rules and settings based approach for preparing verification tasks.