diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
832 stars 262 forks source link

Conversion error with _Generic + array #8243

Open P-p-H-d opened 7 months ago

P-p-H-d commented 7 months ago

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 commented 7 months ago

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