Comments (3)
At a much larger scale, Linux distributions have solved these problems properly, so it's not that rocket science would be required. I had myself made attempts in the benchmarking toolkit (http://www.cprover.org/software/benchmarks/), and also benchexec has a notion of configuration files to permit reproducible results. I am happy to discuss this here in detail, or else leave it for a future in-person meeting with a wider group.
Best,
Michael
from sv-benchmarks.
How to generate the .i files automatically from the .c files?
How to remember architecture dependencies?
The build system already knows what the target is (x86_64-unknown-linux-gnu or i386-unknown-linux-gnu) so that most logical thing to do is to teach the build system to build the *.i
files from the *.c
files. The changes needed to the build system to do this are pretty trivial and actually vastly simplifies the current implementation.
A reproducible environment is also required if you want consistent *.i
files between Linux distributions using different versions of glibc. One option is just to provide a canonical environment (i.e. a VM or a docker image) that the build should be performed in, my preference would be a docker image as they are much more light weight.
An alternative option to a VM or docker image is to actually provide the headers you want to use in the repository (i.e. in a include/
directory), pass -nostdinc
to the compiler and pass -I include/
to the compiler so that we control what files are included. I'm not a huge fan of this idea as it means we have to maintain our own C library header files.
If we have a consistent way to generate *.i
files then should NOT be stored in the repository as this is a waste of space. We would provide instructions on how to obtain the *.i
files and/or provide nightly builds and also a final (for the competition) snapshot build.
from sv-benchmarks.
So #121 is all about this, and there are discussions on the mailing list. I think we have a vast collection of technical solutions proposed. @PhilippWendler @dbeyer It's now a question of what can be implemented within the constraints of the competition run-time system, or for what there is willingness to implement it.
from sv-benchmarks.
Related Issues (20)
- Tasks in seq-mthreaded wrongly marked as non-terminating HOT 2
- Task ntdrivers/floppy2 is not memory safe
- Task ntdrivers/diskperf.i.cil-1.c is not memory safe HOT 2
- ntdrivers/parport.i.cil-2 is not memory safe
- LDV tasks with undefined behaviour and/or wrong verdicts HOT 3
- cut-2 and od-1 from busy-box are not memory safe HOT 1
- Undefined behavior in two AWS benchmarks
- MemSafety - unset subproperty for false verdict
- Incorrect Verification Task
- geo1-ll.c can overflow HOT 3
- Implementation-defined behaviour HOT 3
- SV-COMP concurrency benchmarks with data races HOT 3
- "Repeated" benchmarks in pthread-wmm
- why can echo-2.i overflow? HOT 2
- __builtin_unreachable() in LDV benchmarks HOT 3
- Benchmarks for weak memory models HOT 3
- Reachable error in pthread-ext/41_FreeBSD_abd_kbd_sliced
- Use of `__VERIFIER_nondet_*` functions that aren't specified in SV-COMP rules HOT 1
- Info on SV-COMP 2022? HOT 2
- Repository moved to GitLab 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 sv-benchmarks.