Feature #7264
closed
EMG should generate ldv_thread_join with two arguments
Added by Pavel Andrianov almost 8 years ago.
Updated almost 8 years ago.
Category:
Environment models
Published in build:
54d9b77
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.
What are you going to do with programs that haven't specially prepared environments that in particular include everything related with threads management?
The general approach certainly has to track thread pointers, but it is not efficient enough, thus now we are focusing on the simplified task.
- Status changed from New to Resolved
Implemented in branch 'thread-join-fix'.
- 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.
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!
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.
Also available in: Atom
PDF