Defined type interpreted as symbol when used with gcc specifiers

[mstachyraa]

CBMC version: 5.85.0
Operating system: ubuntu-20.04 x86_64 GNU/Linux
Exact command line resulting in the issue: cbmc test1.c --bounds-check --pointer-check
What behaviour did you expect: VERIFICATION SUCCESSFUL
What happened instead: CONVERSION ERROR

Defined type is not interpreted correctly when used as an argument in gcc specifiers. Instead it is considered a symbol and given a tag.

typedef unsigned long u64;

struct __attribute__((aligned(sizeof(unsigned long)))) structure1 { // <- Works correctly
    unsigned int number;
};

struct __attribute__((aligned(sizeof(u64)))) structure2 { // <- CONVERSION ERROR
    unsigned int number;
};

char main() {
return 0;
}

Program output:

CBMC version 5.85.0 (cbmc-5.85.0) 64-bit x86_64 linux
Parsing test1.c
Converting
Type-checking test1
file test1.c line 11: failed to find symbol 'tag-u64'
CONVERSION ERROR

Parse tree for the selected type:

Declarator: declarator

• type: nil
• #source_location:
  • file: test1.c
  • line: 2
  • function:
  • working_directory: /media/storage/cbmc/tests
• value: nil
• name: u64
• base_name: u64
  ...
  1: aligned
  • #source_location:
    • file: test1.c
    • line: 11
    • function:
    • working_directory: /media/storage/cbmc/tests
  • size: sizeof
    • #source_location:
      • file: test1.c
      • line: 11
      • function:
      • working_directory: /media/storage/cbmc/tests
        0: symbol
        • #source_location:
          • file: test1.c
          • line: 11
          • function:
          • working_directory: /media/storage/cbmc/tests
        • identifier: tag-u64
        • #id_class: 3
        • #base_name: u64

[TGWDB]

Thanks for reporting this. Can confirm I've reproduced locally.