Skip to content

Commit a1eac5c

Browse files
committed
[chore] Update tests
1 parent cf3e335 commit a1eac5c

File tree

7 files changed

+74
-4
lines changed

7 files changed

+74
-4
lines changed

test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99

1010
// RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK-COV %s
1111

12-
// Branch coverage 100%, the number of branches is 1:
12+
// Branch coverage 100%, the number of branches is 2:
1313
// CHECK-COV: Lines executed:100.00% of 11
1414
// CHECK-COV-NEXT: Branches executed:100.00% of 2
1515
// CHECK-COV-NEXT: Taken at least once:100.00% of 2

test/Industry/CoverageBranches/CostasArray-17.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@
1919

2020
// RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK %s
2121

22-
// Branch coverage 100%, the number of branches is 1:
22+
// Branch coverage 100%, the number of branches is 2:
2323
// CHECK: Lines executed:{{(0\.7[0-9])}}% of 1545
2424
// CHECK-NEXT: Branches executed:100.00% of 2
2525
// CHECK-NEXT: Taken at least once:100.00% of 2

test/Industry/CoverageBranches/egcd3-ll_valuebound10.c

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@
99

1010
// RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK %s
1111

12-
// Branch coverage 100%, the number of branches is 1:
1312
// CHECK: Lines executed:87.93% of 58
1413
// CHECK-NEXT: Branches executed:100.00% of 18
1514
// CHECK-NEXT: Taken at least once:83.33% of 18
Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
// RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc
2+
// RUN: rm -rf %t.klee-out
3+
// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --optimize=true --delete-dead-loops=false --use-forked-solver=false -max-memory=6008 --cex-cache-validity-cores --only-output-states-covering-new=true --dump-states-on-halt=true --use-sym-size-alloc=true --symbolic-allocation-threshold=8192 %t1.bc 2>&1
4+
5+
// RUN: rm -f %t*.gcda %t*.gcno %t*.gcov
6+
// RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage
7+
// RUN: %replay %t.klee-out %t_runner
8+
// RUN: gcov -b %t_runner-%basename_t > %t.cov.log
9+
10+
// RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK-COV %s
11+
12+
// CHECK-COV: Lines executed:85.19% of 27
13+
// CHECK-COV-NEXT: Branches executed:100.00% of 16
14+
// CHECK-COV-NEXT: Taken at least once:93.75% of 16
15+
16+
#include "klee-test-comp.c"
17+
extern void abort(void);
18+
#ifdef GCOV
19+
extern void __gcov_dump(void);
20+
#endif
21+
22+
void dump() {
23+
#ifdef GCOV
24+
__gcov_dump();
25+
#endif
26+
}
27+
28+
void abort_prog() {
29+
#ifdef GCOV
30+
__gcov_dump();
31+
exit(0);
32+
#else
33+
abort();
34+
#endif
35+
}
36+
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
37+
void reach_error() { dump(); __assert_fail("0", "matrix-2-2.c", 3, "reach_error"); }
38+
39+
void __VERIFIER_assert(int cond) {
40+
if (!(cond)) {
41+
ERROR: {reach_error();abort();}
42+
}
43+
return;
44+
}
45+
extern unsigned int __VERIFIER_nondet_uint();
46+
extern int __VERIFIER_nondet_int();
47+
48+
int main()
49+
{
50+
unsigned int N_LIN=__VERIFIER_nondet_uint();
51+
unsigned int N_COL=__VERIFIER_nondet_uint();
52+
if (N_LIN >= 4000000000 / sizeof(int) || N_COL >= 4000000000 / sizeof(int)) {
53+
return 0;
54+
}
55+
unsigned int j,k;
56+
int matriz[N_COL][N_LIN], maior;
57+
58+
maior = __VERIFIER_nondet_int();
59+
for(j=0;j<N_COL;j++)
60+
for(k=0;k<N_LIN;k++)
61+
{
62+
matriz[j][k] = __VERIFIER_nondet_int();
63+
64+
if(matriz[j][k]>maior)
65+
maior = matriz[j][k];
66+
}
67+
68+
for(j=0;j<N_COL;j++)
69+
for(k=0;k<N_LIN;k++)
70+
__VERIFIER_assert(matriz[j][k]<maior);
71+
}
72+

test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@
1010

1111
// RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK %s
1212

13-
// Branch coverage 89.29%
1413
// CHECK: Lines executed:{{(9[0-9]\.[0-9][0-9])}}% of 4114
1514
// CHECK-NEXT: Branches executed:{{(9[0-9]\.[0-9][0-9])}}% of 13404
1615
// CHECK-NEXT: Taken at least once:{{(8[0-9]\.[0-9][0-9])}}% of 13404

0 commit comments

Comments
 (0)