diff options
| author | Martin Nowack <m.nowack@imperial.ac.uk> | 2020-01-16 18:37:28 +0000 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-01-18 16:34:03 +0000 |
| commit | 4300ed7cd1ec48292a1983bb80161099f15b2023 (patch) | |
| tree | 5f95eb4109c216fab9ff91595d8b656e85bea499 /test | |
| parent | c7cdc0f15f0f08fb4a808096e741263ff4fb26e3 (diff) | |
| download | klee-4300ed7cd1ec48292a1983bb80161099f15b2023.tar.gz | |
Fix handling of debug information for functions
Tracking function locations separately correctly without prefixing it with a directory.
Diffstat (limited to 'test')
| -rw-r--r-- | test/Feature/SourceMapping.c | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test/Feature/SourceMapping.c b/test/Feature/SourceMapping.c index 6a071933..de0c0605 100644 --- a/test/Feature/SourceMapping.c +++ b/test/Feature/SourceMapping.c @@ -11,7 +11,7 @@ // Assuming the compiler doesn't reorder things, f0 should be first, and it // should immediately follow the first file name marker. -// CHECK: fl={{.*}}/SourceMapping.c +// CHECK: fl={{.*}}test/Feature/SourceMapping.c // CHECK-NEXT: fn=f0 // Ensure we have a known position for the first instruction (instr and line @@ -35,6 +35,8 @@ int f1(int a, int b) { // This check just brackets the checks above, to make sure they fall in the // appropriate region of the run.istats file. // +// Explicitly check that there is no duplication of the path +// CHECK-NOT: fl={{.*}}/test/Feature/{{.*}}/test/Feature/SourceMapping.c // CHECK: fn=main int main() { int x = f1(1, 2); |