diff options
Diffstat (limited to 'test/Feature')
| -rw-r--r-- | test/Feature/SilentKleeAssume.c | 3 | ||||
| -rw-r--r-- | test/Feature/consecutive_divide_by_zero.c | 3 | ||||
| -rw-r--r-- | test/Feature/srem.c | 3 |
3 files changed, 6 insertions, 3 deletions
diff --git a/test/Feature/SilentKleeAssume.c b/test/Feature/SilentKleeAssume.c index b9229d2e..06872e9b 100644 --- a/test/Feature/SilentKleeAssume.c +++ b/test/Feature/SilentKleeAssume.c @@ -26,5 +26,6 @@ int main() { // CHECK-SILENT-KLEE-ASSUME: KLEE: output directory is "{{.+}}" // CHECK-SILENT-KLEE-ASSUME: KLEE: done: total instructions = {{[0-9]+}} -// CHECK-SILENT-KLEE-ASSUME: KLEE: done: completed paths = 2 +// CHECK-SILENT-KLEE-ASSUME: KLEE: done: completed paths = 1 +// CHECK-SILENT-KLEE-ASSUME: KLEE: done: partially completed paths = 1 // CHECK-SILENT-KLEE-ASSUME: KLEE: done: generated tests = 1 diff --git a/test/Feature/consecutive_divide_by_zero.c b/test/Feature/consecutive_divide_by_zero.c index c2f5e152..0915bbaa 100644 --- a/test/Feature/consecutive_divide_by_zero.c +++ b/test/Feature/consecutive_divide_by_zero.c @@ -25,7 +25,8 @@ int main() { // CHECK: consecutive_divide_by_zero.c:[[@LINE+1]]: divide by zero unsigned int result2 = b / d2; - // CHECK: completed paths = 3 + // CHECK: completed paths = 1 + // CHECK: partially completed paths = 2 // CHECK: generated tests = 3 return 0; } diff --git a/test/Feature/srem.c b/test/Feature/srem.c index 1303ac63..65b324d3 100644 --- a/test/Feature/srem.c +++ b/test/Feature/srem.c @@ -39,5 +39,6 @@ int main(int argc, char** argv) // CHECK: srem.c:[[@LINE+1]]: ASSERTION FAIL assert(-1 % y == -1); - // CHECK: KLEE: done: completed paths = 5 + // CHECK: KLEE: done: completed paths = 2 + // CHECK: KLEE: done: partially completed paths = 3 } |