Skip to content

Commit

Permalink
[fix]
Browse files Browse the repository at this point in the history
  • Loading branch information
misonijnik committed Jan 6, 2024
1 parent 399a10a commit a2b2aee
Show file tree
Hide file tree
Showing 6 changed files with 9 additions and 8 deletions.
2 changes: 1 addition & 1 deletion test/Industry/CoverageBranches/CostasArray-17.c
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ int __VERIFIER_nondet_int();

#ifdef GCOV
extern void __gcov_dump(void);
extern void exit( int exit_code ) __attribute__((noreturn));
extern void exit(int exit_code) __attribute__((noreturn));
#endif

void abort_prog() {
Expand Down
2 changes: 1 addition & 1 deletion test/Industry/CoverageBranches/matrix-2-2.c
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,10 @@

#include "klee-test-comp.c"

extern void exit(int);
extern void abort(void);
#ifdef GCOV
extern void __gcov_dump(void);
extern void exit(int);
#endif

void dump() {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@

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

// CHECK: Lines executed:{{(9[0-9]\.[0-9][0-9])}}% of 411{{4|5}}
// CHECK: Lines executed:{{(9[0-9]\.[0-9][0-9])}}% of 411{{3|4}}
// CHECK-NEXT: Branches executed:{{(9[0-9]\.[0-9][0-9])}}% of 13404
// CHECK-NEXT: Taken at least once:{{([8|9][0-9]\.[0-9][0-9])}}% of 13404

Expand All @@ -34,6 +34,7 @@ extern void exit(int);
extern void abort(void);
#ifdef GCOV
extern void __gcov_dump(void);
extern void exit(int exit_code) __attribute__((noreturn));
#endif

void dump() {
Expand Down
4 changes: 2 additions & 2 deletions test/Industry/egcd3-ll_valuebound10.c
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,10 @@
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state %t1.bc

// RUN: rm -f %t*.gcda %t*.gcno %t*.gcov
// RUN: rm -f ./%gcov-files-path*.gcda ./%gcov-files-path*.gcno ./%gcov-files-path*.gcov
// RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage
// RUN: %replay %t.klee-out %t_runner
// RUN: gcov -b %t_runner-%basename_t > %t.cov.log
// RUN: gcov -b %gcov-files-path > %t.cov.log

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

Expand Down
2 changes: 1 addition & 1 deletion test/Solver/CallComputeValue.c
Original file line number Diff line number Diff line change
Expand Up @@ -17,5 +17,5 @@ int main() {
return 2;
}

// CHECK: KLEE: done: completed paths = 3
// CHECK: KLEE: done: completed paths = {{3|5}}
// CHECK: KLEE: done: partially completed paths = 0
4 changes: 2 additions & 2 deletions test/regression/2023-03-27-lib-function.c
Original file line number Diff line number Diff line change
Expand Up @@ -26,8 +26,8 @@ const char *inet_ntop(int af, const void *restrict src,

int main(int argc, char **argv) {
inet_ntop(0, 0, 0, 0);
// CHECK_INTERNAL-NOT: calling external: inet_ntop
// CHECK_EXTERNAL: calling external: inet_ntop
// CHECK_INTERNAL-NOT: calling external: {{inet_ntop|__inet_ntop}}
// CHECK_EXTERNAL: calling external: {{inet_ntop|__inet_ntop}}
#ifdef INET_PTON
struct in_addr inaddr;
inet_pton(AF_INET, "10.1.0.29", &inaddr);
Expand Down

0 comments on commit a2b2aee

Please sign in to comment.