Skip to content

Commit 81d177e

Browse files
committed
[ci]
1 parent 2d753ad commit 81d177e

File tree

4 files changed

+4
-1
lines changed

4 files changed

+4
-1
lines changed

test/Industry/egcd3-ll_valuebound10.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
// REQUIRES: not-darwin
12
// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
23
// RUN: rm -rf %t.klee-out
34
// 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=true --search=dfs --search=random-state %t1.bc

test/Industry/ll_create_rec-alloca-2.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
// RUN: %klee-stats --print-columns 'ICov(%),BCov(%)' --table-format=csv %t.klee-out > %t.stats
55
// RUN: FileCheck -check-prefix=CHECK-BRANCH -input-file=%t.stats %s
66

7-
// Branch coverage 100%, and instruction coverage can variate:
7+
// Branch coverage 100%, and instruction coverage may vary:
88
// CHECK-BRANCH: ICov(%),BCov(%)
99
// CHECK-BRANCH-NEXT: {{([1-9][0-9]\.[0-9][0-9])}},100.00
1010

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
// REQUIRES: geq-llvm-12.0, not-darwin
12
// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
23
// RUN: rm -rf %t.klee-out
34
// RUN: %klee --output-dir=%t.klee-out --max-instructions=100 --optimize-aggressive=false --track-coverage=branches --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=3s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state --use-iterative-deepening-search=max-cycles --max-cycles=4 %t1.bc

test/regression/2023-10-16-CostasArray-17.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
// REQUIRES: not-darwin
12
// RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc
23
// RUN: rm -rf %t.klee-out
34
// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=true --search=dfs %t1.bc

0 commit comments

Comments
 (0)