Error when compiling develop on MacOS

[victoria-tuck]

CBMC version:
commit 63703d off of develop

Operating system:
macOS Mojave 10.14.6

Exact command line resulting in the issue:
make -C src

What behaviour did you expect:
This to occur without error

What happened instead:

[victoria-tuck]

I tried this without the -C option and it did work. I'm not sure what the difference is, but if without -C is ok then maybe this should be updated in the compile docs

[martin-cs]

The -C is "change directory before starting". The docs could say:

cd src
make

which is IMHO clearer, but slightly more verbose.

[tautschnig]

@esteffin or @thomasspriggs Could you please take a look? I suspect that this just needs a type name for the inner element being constructed rather than leaving it to the compiler to infer it (where the compiler on 10.14 might simply be too old).

[NlightNFotis]

@tautschnig Hi Michael, this came up to my attention just now.

I will have a look at this a bit later, and update you here.

[thomasspriggs]

Yes, this might just need smt_get_value_responset::valuation_pairt adding in order to fix this. The construction should already be unambiguous as you can't construct an std::string using a pair of smt_termt as constructor parameters. I don't have a Mac on hand to test this. So I'm going to leave this with @NlightNFotis for the moment.

It is worth noting that the oldest version of MacOS we test in CI is MacOS-11. So even if we fix this particular compilation issue more are likely to crop up over time. The github actions runner for MacOS 10 is deprecated - https://github.blog/changelog/2022-07-20-github-actions-the-macos-10-15-actions-runner-image-is-being-deprecated-and-will-be-removed-by-8-30-22/

[NlightNFotis]

Hello - I did have some time to look into this this morning and I have the following notes:

• First of all, I cannot reproduce it, but that's probably because I'm on a later version of the SDK and the operating system than the OP - @victoria-tuck can you please let us know what your SDK version is (xcrun -show-sdk-version) and what your Clang version is (clang --version)?
• A speculative fix (because I can't reproduce locally) would be to change the reported line from return resultt{{valid_descriptor, valid_value}}; to return resultt{smt_get_value_responset::valuation_pairt{valid_descriptor, valid_value}};. This doesn't seem like a very productive change to make to me, because we depend on compiler template argument deduction on a number of places, and fixing just this one probably won't make much of a difference in the grand scheme of things - unless we have a way to find all of those places (with a compiler error perhaps?).
• I am slightly concerned with the reported issue vanishing when changing the make invocation. In theory the -C flag shouldn't change anything in the build (outside from $PWD while invoking clang et al) but could this be an issue of configuration skipped/not initialised properly outside of a specific folder?

Any thoughts here @tautschnig ?

[tautschnig]

1. If @victoria-tuck can try out change proposed by @NlightNFotis and confirm this is the only change needed to get it to build then let's do it. Else what @NlightNFotis said: we can not reasonably support such compilers for we can't test.
2. The make "fix" might be that @victoria-tuck tried make src, which will just say make: Nothing to be done for 'src'. and happily terminate, as "src" exists (as a directory). But then make just didn't even try to build anything.

@victoria-tuck I think we need more information from your side at this point.