diff options
author | Daniel Dunbar <daniel@zuster.org> | 2014-09-12 18:06:13 -0700 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2014-09-12 18:06:13 -0700 |
commit | f3c83eaa5506da9776c24416faba4c45a622a1ef (patch) | |
tree | 6bc8a5e73b2629e93b2be506387f77dda07f8b72 /test | |
parent | f31f54e5cfeebd956f49920d680a167507400994 (diff) | |
download | klee-f3c83eaa5506da9776c24416faba4c45a622a1ef.tar.gz |
[tests] Add a workaround to try and prevent llvm-gcc from calling putchar(), which the LLVM JIT can't handle.
Diffstat (limited to 'test')
-rw-r--r-- | test/Concrete/_testingUtils.c | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/test/Concrete/_testingUtils.c b/test/Concrete/_testingUtils.c index 52e4f13e..693a5a09 100644 --- a/test/Concrete/_testingUtils.c +++ b/test/Concrete/_testingUtils.c @@ -15,6 +15,11 @@ TYPED_PRINT(i16, unsigned short) TYPED_PRINT(i32, unsigned int) TYPED_PRINT(i64, unsigned long long) +// This is a workaround to hide the "%c" only format string from the compiler -- +// llvm-gcc can optimize this into putchar even at -O0, and the LLVM JIT doesn't +// recognize putchar() as a valid external function. +char *char_format_string = "%c"; + void print_int(unsigned long long val) { int cur = 1; @@ -26,11 +31,11 @@ void print_int(unsigned long long val) { while (cur) { int digit = val / cur; - printf("%c", digit + '0'); + printf(char_format_string, digit + '0'); val = val % cur; cur /= 10; } - printf("%c", '\n'); + printf(char_format_string, '\n'); } |