| Age | Commit message (Collapse) | Author |
|---|
|
the --svcomp-runtime flag. This is accompanied with a set of tests
to check all the functions are callable.
Due to the fact that the SV-COMP benchmark suite contains a mixture
of i386 and x86_64 benchmarks it is necessary to compile the runtime
functions twice, once for i386 and once for x86_64 and then link the
right version in at runtime. An example function that is problematic
is ``__VERIFIER_nondet_long()`` which is a different size on i386
and x86_64.
|
|
it can find klee-uclibc inside the same folder as the other
runtime libraries with the name "klee-uclibc.bca"
This is implemented as follows:
* When building, a sym-link is created to klee-uclibc's libc.a file
in the same directory that the rest of KLEE's runtime libraries
are built. This done so that if a developer changes klee-uclibc
on their system then the correct version of klee-uclibc is used
by KLEE.
* When installing, klee-uclibc's libc.a file is installed in the same
directory that the rest of KLEE's runtime libraries are installed.
In addition the configure script argument --with-uclibc can now
operate in two ways. It can either be passed the path to the root
of klee-uclibc or it can be passed a path to the libc.a file built
by klee-uclibc. This new behaviour has been added to allow users
to potential use pre-built versions of klee-uclibc.
|
|
|
|
- Lots more tweaks, documentation, and web page content is needed,
but this should compile & work on OS X & Linux.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8
|
