about summary refs log tree commit diff homepage
path: root/runtime/klee-libc
diff options
context:
space:
mode:
Diffstat (limited to 'runtime/klee-libc')
-rwxr-xr-xruntime/klee-libc/Makefile6
-rw-r--r--runtime/klee-libc/putchar.c5
2 files changed, 7 insertions, 4 deletions
diff --git a/runtime/klee-libc/Makefile b/runtime/klee-libc/Makefile
index e6a7ad72..eca63169 100755
--- a/runtime/klee-libc/Makefile
+++ b/runtime/klee-libc/Makefile
@@ -10,11 +10,13 @@
 LEVEL=../..
 
 LIBRARYNAME=klee-libc
-DONT_BUILD_RELINKED=1
+MODULE_NAME=klee-libc
+#DONT_BUILD_RELINKED=1
 BYTECODE_LIBRARY=1
+MODULE_NAME=klee-libc
 # Don't strip debug info from the module.
 DEBUG_RUNTIME=1
-NO_PEDANTIC=1
+#NO_PEDANTIC=1
 
 # Add __NO_INLINE__ to prevent glibc from using inline definitions of some
 # builtins.
diff --git a/runtime/klee-libc/putchar.c b/runtime/klee-libc/putchar.c
index 4c3a57e4..497402a6 100644
--- a/runtime/klee-libc/putchar.c
+++ b/runtime/klee-libc/putchar.c
@@ -15,6 +15,7 @@
 
 int putchar(int c) {
   char x = c;
-  write(1, &x, 1);
-  return 1;
+  if (1 == write(1, &x, 1))
+    return c;
+  return EOF;
 }