goto-cc 6.0.0 fails compilation of s2n-tls unit on Linux, but works on macOS about cbmc HOT 10 CLOSED

Could you please attach preprocessed source to this issue? You can obtain these by adding -E to the goto-cc commands.

Edit: Also, please add the s2n-tls commit id you are working off of.

Thank you!

from cbmc.

If I run gcc directly on that source file, I get a slightly more detailed error message:

In file included from cbmc_utils.c:16:
cbmc_utils.c: In function ‘assert_rc_decrement_on_evp_pkey_ctx’:
cbmc_utils.c:203:29: error: invalid use of incomplete typedef ‘EVP_PKEY’ {aka ‘struct evp_pkey_st’}
  203 |         assert(storage->pkey->references == storage->pkey_refs - 1);
      |                             ^~

from cbmc.

If I run gcc directly on that source file, I get a slightly more detailed error message:

So this isn’t a goto-cc issue?!

from cbmc.

Well... it seems that the compiler upon which goto-cc is built and/or based on seems to matter in some way. Here is the expanded source attached.
cbmc_utils_expanded.c.gz

from cbmc.

cbmc_utils_expanded.c.gz

Is this Linux or macOS? Could you please provide the other one as well?

from cbmc.

That one was pre-processed on Linux.

from cbmc.

Here it is again, this time expanded with clang 15.0.0 on macOS...
cbmc_utils_expanded_macos.c.gz

from cbmc.

goto-gcc simply calls gcc, passing through any arguments, goto-clang calls clang, and so on. We should find a way of clarifying whether an error message is generated by the underlying compiler, or by our own parser/typechecker.

from cbmc.

The difference here is on your Linux system you appear to have OpenSSL's header files installed in the default include search path of the preprocessor (and you don't use -nostdinc). With those header files installed, crypto/s2n_evp.h will bring in /usr/include/openssl/evp.h instead of tests/cbmc/aws-verification-model-for-libcrypto/include/openssl/evp.h (as is the case in your macOS run).

Closing as this doesn't seem an issue on goto-cc's side. Please feel free to reopen with more info if you still think that goto-cc needs to be changed in any way.

from cbmc.

Ah... that makes sense. The instructions in the s2n-tls README file tell me to install "libssl-dev" to build s2n-tls on Linux, so that makes sense. Now... I will ask the s2n-tls developers how they handle this case.

from cbmc.