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

Header file "dirent.h" poses problems for goto-cc #8504

Open
metamaterialsuit opened this issue Nov 14, 2024 · 0 comments
Open

Header file "dirent.h" poses problems for goto-cc #8504

metamaterialsuit opened this issue Nov 14, 2024 · 0 comments

Comments

@metamaterialsuit
Copy link

CBMC version: 6.1.1-2
Operating system: Linux
Exact command line `resulting in the issue: goto-cc -o file.o file.c
What behaviour did you expect: A goto program to be built
What happened instead: The file contains a <dirent.h> include. goto-cc reports:
"error: function symbol 'readdir' redefined with different type:"
"Original: struct dirent * (DIR *)"
"New: struct dirent64 * (DIR *)"
"extern struct dirent64 *readdir64(DIR *__dirp) __nonnull ((1));"

I believe this is happening because internally dirent.h includes <bits/dirent.h> which defines a struct dirent and can conditionally swap it to a dirent64 if the appropriate define is available. Or at least thats what I think is happening, hence the redefinition error. Unfortunately I have no idea how to fix this because it is a system header.

In any case, would appreciate some help.

-M

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