diff options
| author | Julian Büning <julian.buening@comsys.rwth-aachen.de> | 2023-05-29 12:48:53 +0200 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-06-05 17:16:13 +0100 |
| commit | a39348ba3b0f3739e1be0ab45942209a2007ae4d (patch) | |
| tree | f456f1278cd40e3681259145a213d56a3d11372f | |
| parent | 0a240e58954753a44989cfdfb2cd6fa6f388cb49 (diff) | |
| download | klee-a39348ba3b0f3739e1be0ab45942209a2007ae4d.tar.gz | |
test/Feature/StackTraceOutput.c: relative checks, clang-format
| -rw-r--r-- | test/Feature/StackTraceOutput.c | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/test/Feature/StackTraceOutput.c b/test/Feature/StackTraceOutput.c index a814adeb..d28cb13c 100644 --- a/test/Feature/StackTraceOutput.c +++ b/test/Feature/StackTraceOutput.c @@ -13,16 +13,19 @@ #include <assert.h> void foo(int i, int k) { - ++i; ++k; + ++i; + ++k; + + // CHECK-DISCARD: {{.*}} in foo(symbolic, 12) at {{.*}}.c:[[@LINE+2]] + // CHECK-NODISCARD: {{.*}} in foo(i=symbolic, k=12) at {{.*}}.c:[[@LINE+1]] assert(0); - // CHECK-DISCARD: {{.*}} in foo(symbolic, 12) at {{.*}}.c:17 - // CHECK-DISCARD: {{.*}} in main() at {{.*}}.c:27 - // CHECK-NODISCARD: {{.*}} in foo(i=symbolic, k=12) at {{.*}}.c:17 - // CHECK-NODISCARD: {{.*}} in main() at {{.*}}.c:27 } int main(void) { - int i, k=12; + int i, k = 12; klee_make_symbolic(&i, sizeof(i), "i"); - foo(i,k); + + // CHECK-DISCARD: {{.*}} in main() at {{.*}}.c:[[@LINE+2]] + // CHECK-NODISCARD: {{.*}} in main() at {{.*}}.c:[[@LINE+1]] + foo(i, k); } |