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

Conversion error with _Generic + array #8243

Open
P-p-H-d opened this issue Mar 15, 2024 · 1 comment
Open

Conversion error with _Generic + array #8243

P-p-H-d opened this issue Mar 15, 2024 · 1 comment
Assignees

Comments

@P-p-H-d
Copy link

P-p-H-d commented Mar 15, 2024

CBMC version: CBMC version 5.95.1
Operating system: 64-bit x86_64 linux
Exact command line resulting in the issue: cbmc t.c
What behaviour did you expect: Parsing source file with _Generic + array
What happened instead: CONVERSION ERROR

CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Parsing t.c
Converting
Type-checking t
file t.c line 4 function main: unmatched generic selection: m_string_t
CONVERSION ERROR

The program:

typedef struct m_string_s { int s, a; char *ptr; } m_string_t[1];
int main(void) {
  m_string_t s;
  return _Generic( s, struct m_string_s *: 0);
}
@P-p-H-d
Copy link
Author

P-p-H-d commented Mar 15, 2024

Conversion from "array of type" to "pointer to type" seems not done as per §6.3.2.1.3 of C11.

@tautschnig tautschnig self-assigned this Mar 15, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants