Build fails when using Clang 15

[esteffin]

CBMC build fails when using Clang 15 (latest version of Clang released in September 2022) on Mac.

Multiple new warning are produced when building with Clang 15. This makes the build to fail as we use -Werror.

CBMC version: 5.76.1
Operating system: MacOS
Exact command line resulting in the issue: make
What behaviour did you expect: build succeed
What happened instead: build failure

[tautschnig]

Would you mind sharing the warnings so that they can be addressed, or are you already working on a PR to do so?

[esteffin]

Unfortunately there are many warnings.

The first 2 to be encountered are:

/Users/esteffin/git/cbmc/src/goto-programs/osx_fat_reader.cpp:134:30: error: argument 'hdr' of type 'char[4]' with mismatched bound [-Werror,-Warray-parameter]
bool is_osx_mach_object(char hdr[4])
                             ^
/Users/esteffin/git/cbmc/src/goto-programs/osx_fat_reader.h:77:30: note: previously declared as 'char[8]' here
bool is_osx_mach_object(char hdr[8]);
                             ^

/Users/esteffin/git/cbmc/src/goto-programs/goto_trace.cpp:400:15: error: variable 'function_depth' set but not used [-Werror,-Wunused-but-set-variable]
  std::size_t function_depth = 0;
              ^

Addressing them unleashes many others such as:

• 4 error: this style of line directive is a GNU extension [-Werror,-Wgnu-line-marker]
• 14 error: a function declaration without a prototype is deprecated in all versions of C [-Werror,-Wstrict-prototypes] in various files.

I don't know if fixing all those errors is enough though.

[tautschnig]

Unfortunately there are many warnings.

So we should just go and fix them.

The first 2 to be encountered are:

/Users/esteffin/git/cbmc/src/goto-programs/osx_fat_reader.cpp:134:30: error: argument 'hdr' of type 'char[4]' with mismatched bound [-Werror,-Warray-parameter]
bool is_osx_mach_object(char hdr[4])
                             ^
/Users/esteffin/git/cbmc/src/goto-programs/osx_fat_reader.h:77:30: note: previously declared as 'char[8]' here
bool is_osx_mach_object(char hdr[8]);
                             ^

Good catch, this should be 4 in both cases. Fixed in #7526 .

/Users/esteffin/git/cbmc/src/goto-programs/goto_trace.cpp:400:15: error: variable 'function_depth' set but not used [-Werror,-Wunused-but-set-variable]
  std::size_t function_depth = 0;
              ^

This seems spurious?! We use that variable 3 lines later.

Addressing them unleashes many others such as:

* 4 `error: this style of line directive is a GNU extension [-Werror,-Wgnu-line-marker]`

Any example of this one?

* 14 `error: a function declaration without a prototype is deprecated in all versions of C [-Werror,-Wstrict-prototypes]` in various files.

Where is this showing up?

I don't know if fixing all those errors is enough though.

[esteffin]

/Users/esteffin/git/cbmc/src/goto-programs/goto_trace.cpp:400:15: error: variable 'function_depth' set but not used [-Werror,-Wunused-but-set-variable]
  std::size_t function_depth = 0;

Yes, it is used 2 lines ago, but actually that variable is never read.
It is set to 0. at the beginning, then incremented/decremented with ++ and --, but never actually used or checked.

• 4 error: this style of line directive is a GNU extension [-Werror,-Wgnu-line-marker]
• 14 error: a function declaration without a prototype is deprecated in all versions of C [-Werror,-Wstrict-prototypes]

Both this 2 sets of errors are generated by src/ansi-c/library_check.sh and are related to __libcheck.c __libcheck.i and cprover_builtin_headers.h.

As for extra errors I cannot say as clearly the compilation stops at this point.

[tautschnig]

/Users/esteffin/git/cbmc/src/goto-programs/goto_trace.cpp:400:15: error: variable 'function_depth' set but not used [-Werror,-Wunused-but-set-variable]
  std::size_t function_depth = 0;

Yes, it is used 2 lines ago, but actually that variable is never read. It is set to 0. at the beginning, then incremented/decremented with ++ and --, but never actually used or checked.

Ah, thank you. Fixed in #7529.