Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Problem with enviroment model and line directives #4

Open
PavelAndrianov opened this issue Oct 7, 2020 · 1 comment
Open

Problem with enviroment model and line directives #4

PavelAndrianov opened this issue Oct 7, 2020 · 1 comment

Comments

@PavelAndrianov
Copy link
Contributor

Now, the environment model looks like

main(..) {
pthread_t thread1;
ldv_thread create(&thread1, ...);

pthread_t thread2;
ldv_thread create(&thread2, ...);
...

This is the origin code. CIL optimizes is to the C99 standart, which claims that all definitions should be at function start:

# line 1
main(..) {
pthread_t thread1;
pthread_t thread2;
...
# line 3
ldv_thread create(&thread1, ...);
# line 6
ldv_thread create(&thread2, ...);
...

But thre problem is that line directives refer to the origin code. Thus we have one block of definitions, which corresponds to one line. This brokes CPAchecker calculation of mapping to the origin files and all references here and (important!) further will differenciate from real ones.
Try to do something in CPAchecker, but if it is possible, maybe, try to generate a correct main function right in generator.

@PavelAndrianov
Copy link
Contributor Author

Actually, I am not correct, the problem does not affect to the following code. So, this is just an inconsistensy for main function.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant