Comments (5)
I am sorry, I don't understand how to reproduce this. Where can I find that let _ = std::boxed::Box::new(0_usize);
that needs to be removed in order to observe the problem?
from cbmc.
Contracts instrumentation attempts to load free
from the CPROVER library no matter what the GOTO model contains
CF here:
The contracts instrumentation assumes that if an entry for a library function like free
is found in the symbol table then the body of the function is present too, and it doesn't attempt to force-load the function. So the only way contracts would not load the free
function into the model is if the symbol table produced by Kani contains an entry for the free
function but does not contain the body of the function.
from cbmc.
The output mentioning builtin-library-free suggests it is loaded, so Iām quite confused what is actually going on here. Needs details to reproduce and debug.
from cbmc.
This is an extract of kani_lib.c
// Declare functions instead of importing more headers in order to avoid conflicting definitions.
// See https://github.com/model-checking/kani/issues/1774 for more details.
void free(void *ptr);
void *memcpy(void *dst, const void *src, size_t n);
void *calloc(size_t nmemb, size_t size);
Could these declarations result in an entry being present for free
in the symbol table but the value of the symbol being absent ? or the entry being present but the GOTO function being pruned if its not actually used before contracts instrumentation is applied ?
from cbmc.
file <builtin-library-free>
really suggests that we are reading (using?) the definition from CBMC's library, though admittedly this is part of a warning, so it could be that we don't actually link in the implementation. So, still, we need a way to actually reproduce this.
from cbmc.
Related Issues (20)
- Generating GOTO-programs as front-end to other tool HOT 2
- String abstraction crash on very simple C program
- Zero-termination assertion fails on zero-terminated strings
- Non-termination of proof on simple array copy example HOT 3
- CBMC 6.0.0-preview fails with mal-formed SMT HOT 13
- Opened in error - apologies. Please delete or close.
- CBMC-6.0.0 fails if local variable name overloads name of quantified variable in contract HOT 2
- no bounds check assertion HOT 1
- Unwind Issue: How to make a loop inductive? HOT 49
- aarch64: error: incompatible type for argument 1 of '__CPROVER_OBJECT_SIZE HOT 1
- goto-cc 6.0.0 fails compilation of s2n-tls unit on Linux, but works on macOS HOT 10
- 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
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.