diffblue/cbmc

Conversion error with _Generic + array

Opened this issue · 1 comments

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);
}

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