Comments (10)
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.
Related Issues (20)
- Unwind Issue: How to make a loop inductive? HOT 49
- aarch64: error: incompatible type for argument 1 of '__CPROVER_OBJECT_SIZE HOT 1
- Simple error message if --smt2 set and no Z3 on PATH HOT 1
- Non-termination of CBMC on use of size_t as type of a quantified variable HOT 14
- Simple modular reasoning example with contracts fails HOT 9
- List of C/C++ Compiler Support HOT 1
- centos compile cbmc 6.0.1 failed HOT 6
- Model loop invariant with __CPROVER_loop_entry and __CPROVER_loop_old HOT 4
- Multiplication of complex number is modelled incorrectly HOT 1
- Bitwuzla reports error on simple function verification HOT 1
- Run CBMC regression tests with Bitwuzla HOT 1
- Big performance regression of cbmc --cover in 6.0.1 HOT 7
- goto-instrument for k-induction fails invariant check on SV-COMP style single loop reachability problem
- [QUESTION] The Function of CBMC HOT 1
- Better side-effect checks for loop contracts
- Mal-formed SMT2 generated for Bitwuzla HOT 2
- Conflicting solver selection should make CBMC fail
- Symbol Table Error When Using "--race-check" in goto-instrument with CBMC for Global Array
- [QUESTION] Variables for Control Flow Trace Debugging
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from cbmc.