diff options
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 |