diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2017-01-14 19:44:08 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2017-01-14 23:03:06 +0000 |
commit | dcc709dd23fc8a50d5dc087d4d5961dea041bf01 (patch) | |
tree | 84c553f78bc9e8bdcdd5b7aa2e2c9c78d84494dc /runtime | |
parent | 6137888c07ab45bee354ff7b66f6f313ea158da8 (diff) | |
download | klee-dcc709dd23fc8a50d5dc087d4d5961dea041bf01.tar.gz |
Change how error handling is done in libkleeRuntest.
Previously error messages would be emitted but execution would continue which might not be desirable. Now a wrapper function (for fprintf) `report_internal_error()` is used which will cause the program to exit. The older behaviour of continuing to execute after an error can be achieved by setting a new environment variable `KLEE_RUN_TEST_ERRORS_NON_FATAL`. This commit also adds a test for each error case.
Diffstat (limited to 'runtime')
-rw-r--r-- | runtime/Runtest/intrinsics.c | 42 |
1 files changed, 29 insertions, 13 deletions
diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c index d67f093e..4d785ee2 100644 --- a/runtime/Runtest/intrinsics.c +++ b/runtime/Runtest/intrinsics.c @@ -10,8 +10,9 @@ /* Straight C for linking simplicity */ #include <assert.h> -#include <stdlib.h> +#include <stdarg.h> #include <stdio.h> +#include <stdlib.h> #include <string.h> #include <sys/mman.h> #include <sys/time.h> @@ -31,6 +32,23 @@ static unsigned char rand_byte(void) { return x & 0xFF; } +static void report_internal_error(const char *msg, ...) + __attribute__((format(printf, 1, 2))); +static void report_internal_error(const char *msg, ...) { + fprintf(stderr, "KLEE_RUN_TEST_ERROR: "); + va_list ap; + va_start(ap, msg); + vfprintf(stderr, msg, ap); + va_end(ap); + fprintf(stderr, "\n"); + char *testErrorsNonFatal = getenv("KLEE_RUN_TEST_ERRORS_NON_FATAL"); + if (testErrorsNonFatal) { + fprintf(stderr, "KLEE_RUN_TEST_ERROR: Forcing execution to continue\n"); + } else { + exit(1); + } +} + void klee_make_symbolic(void *array, size_t nbytes, const char *name) { static int rand_init = -1; @@ -82,7 +100,7 @@ void klee_make_symbolic(void *array, size_t nbytes, const char *name) { for (;; ++testPosition) { if (testPosition >= testData->numObjects) { - fprintf(stderr, "ERROR: out of inputs, using zero\n"); + report_internal_error("out of inputs. Will use zero if continuing."); memset(array, 0, nbytes); break; } else { @@ -95,13 +113,14 @@ void klee_make_symbolic(void *array, size_t nbytes, const char *name) { continue; } if (strcmp(name, o->name) != 0) { - fprintf(stderr, "ERROR: object name mismatch. Requesting \"%s\" but " - "returning \"%s\"", - name, o->name); + report_internal_error( + "object name mismatch. Requesting \"%s\" but returning \"%s\"", + name, o->name); } memcpy(array, o->bytes, nbytes < o->numBytes ? nbytes : o->numBytes); if (nbytes != o->numBytes) { - fprintf(stderr, "ERROR: object sizes differ\n"); + report_internal_error("object sizes differ. Expected %zu but got %u", + nbytes, o->numBytes); if (o->numBytes < nbytes) memset((char *)array + o->numBytes, 0, nbytes - o->numBytes); } @@ -119,14 +138,13 @@ uintptr_t klee_choose(uintptr_t n) { uintptr_t x; klee_make_symbolic(&x, sizeof x, "klee_choose"); if(x >= n) - fprintf(stderr, "ERROR: max = %ld, got = %ld\n", n, x); - assert(x < n); + report_internal_error("klee_choose failure. max = %ld, got = %ld\n", n, x); return x; } void klee_assume(uintptr_t x) { if (!x) { - fprintf(stderr, "ERROR: invalid klee_assume\n"); + report_internal_error("invalid klee_assume"); } } @@ -148,10 +166,8 @@ int klee_range(int begin, int end, const char* name) { int x; klee_make_symbolic(&x, sizeof x, name); if (x<begin || x>=end) { - fprintf(stderr, - "KLEE: ERROR: invalid klee_range(%u,%u,%s) value, got: %u\n", - begin, end, name, x); - abort(); + report_internal_error("invalid klee_range(%u,%u,%s) value, got: %u\n", + begin, end, name, x); } return x; } |