diff options
| author | Daniel Dunbar <daniel@zuster.org> | 2010-05-02 16:39:02 +0000 |
|---|---|---|
| committer | Daniel Dunbar <daniel@zuster.org> | 2010-05-02 16:39:02 +0000 |
| commit | bae2fa50234b0a575a18a119019e5d96f7ff7ecf (patch) | |
| tree | 732d5cc2ae49831108705505840432dc2f4140a8 /runtime/klee-libc/Makefile | |
| parent | bbfe70007076f28ddbc58abc0eeb7f6dc95e2036 (diff) | |
| download | klee-bae2fa50234b0a575a18a119019e5d96f7ff7ecf.tar.gz | |
Compile klee-libc with -D__NO_INLINE__, to prevent glibc from using inline
definitions of putchar and atoi. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102868 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'runtime/klee-libc/Makefile')
| -rwxr-xr-x | runtime/klee-libc/Makefile | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/runtime/klee-libc/Makefile b/runtime/klee-libc/Makefile index bcd61f73..e6a7ad72 100755 --- a/runtime/klee-libc/Makefile +++ b/runtime/klee-libc/Makefile @@ -16,4 +16,8 @@ BYTECODE_LIBRARY=1 DEBUG_RUNTIME=1 NO_PEDANTIC=1 +# Add __NO_INLINE__ to prevent glibc from using inline definitions of some +# builtins. +C.Flags += -D__NO_INLINE__ + include $(LEVEL)/Makefile.common |