Skip to content

Commit

Permalink
Liveness testsuite: increase instruction budget
Browse files Browse the repository at this point in the history 
to be able to successfully run these tests with
KLEE_RUNTIME_BUILD_TYPE=Debug
  • Loading branch information
@jbuening
jbuening committed Sep 4, 2018
1 parent b9137a6 commit 4304ee2
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 7 deletions.
6 changes: 3 additions & 3 deletions test/Liveness/control-flow.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,23 +12,23 @@
// RUN: test -f %t-O0.klee-out/test000005.infty.err

// RUN: rm -rf %t-O1.klee-out
// RUN: %klee -libc=uclibc -posix-runtime -output-dir=%t-O1.klee-out -detect-infinite-loops -emit-all-errors -stop-after-n-instructions=10000 -allocate-determ %t-O1.bc 2>&1 | FileCheck %s
// RUN: %klee -libc=uclibc -posix-runtime -output-dir=%t-O1.klee-out -detect-infinite-loops -emit-all-errors -stop-after-n-instructions=100000 -allocate-determ %t-O1.bc 2>&1 | FileCheck %s
// RUN: test -f %t-O1.klee-out/test000001.infty.err
// RUN: test -f %t-O1.klee-out/test000002.infty.err
// RUN: test -f %t-O1.klee-out/test000003.infty.err
// RUN: test -f %t-O1.klee-out/test000004.infty.err
// RUN: test -f %t-O1.klee-out/test000005.infty.err

// RUN: rm -rf %t-O2.klee-out
// RUN: %klee -libc=uclibc -posix-runtime -output-dir=%t-O2.klee-out -detect-infinite-loops -emit-all-errors -stop-after-n-instructions=10000 -allocate-determ %t-O2.bc 2>&1 | FileCheck %s
// RUN: %klee -libc=uclibc -posix-runtime -output-dir=%t-O2.klee-out -detect-infinite-loops -emit-all-errors -stop-after-n-instructions=100000 -allocate-determ %t-O2.bc 2>&1 | FileCheck %s
// RUN: test -f %t-O2.klee-out/test000001.infty.err
// RUN: test -f %t-O2.klee-out/test000002.infty.err
// RUN: test -f %t-O2.klee-out/test000003.infty.err
// RUN: test -f %t-O2.klee-out/test000004.infty.err
// RUN: test -f %t-O2.klee-out/test000005.infty.err

// RUN: rm -rf %t-O3.klee-out
// RUN: %klee -libc=uclibc -posix-runtime -output-dir=%t-O3.klee-out -detect-infinite-loops -emit-all-errors -stop-after-n-instructions=10000 -allocate-determ %t-O3.bc 2>&1 | FileCheck %s
// RUN: %klee -libc=uclibc -posix-runtime -output-dir=%t-O3.klee-out -detect-infinite-loops -emit-all-errors -stop-after-n-instructions=100000 -allocate-determ %t-O3.bc 2>&1 | FileCheck %s
// RUN: test -f %t-O3.klee-out/test000001.infty.err
// RUN: test -f %t-O3.klee-out/test000002.infty.err
// RUN: test -f %t-O3.klee-out/test000003.infty.err
Expand Down
8 changes: 4 additions & 4 deletions test/Liveness/overflow-uint8.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,19 +4,19 @@
// RUN: %llvmgcc %s -emit-llvm -O3 -g -c -o %t-O3.bc

// RUN: rm -rf %t-O0.klee-out
// RUN: %klee -libc=uclibc -posix-runtime -output-dir=%t-O0.klee-out -detect-infinite-loops -stop-after-n-instructions=10000 -allocate-determ %t-O0.bc 2>&1 | FileCheck %s
// RUN: %klee -libc=uclibc -posix-runtime -output-dir=%t-O0.klee-out -detect-infinite-loops -stop-after-n-instructions=100000 -allocate-determ %t-O0.bc 2>&1 | FileCheck %s
// RUN: test -f %t-O0.klee-out/test000001.infty.err

// RUN: rm -rf %t-O1.klee-out
// RUN: %klee -libc=uclibc -posix-runtime -output-dir=%t-O1.klee-out -detect-infinite-loops -stop-after-n-instructions=10000 -allocate-determ %t-O1.bc 2>&1 | FileCheck %s
// RUN: %klee -libc=uclibc -posix-runtime -output-dir=%t-O1.klee-out -detect-infinite-loops -stop-after-n-instructions=100000 -allocate-determ %t-O1.bc 2>&1 | FileCheck %s
// RUN: test -f %t-O1.klee-out/test000001.infty.err

// RUN: rm -rf %t-O2.klee-out
// RUN: %klee -libc=uclibc -posix-runtime -output-dir=%t-O2.klee-out -detect-infinite-loops -stop-after-n-instructions=10000 -allocate-determ %t-O2.bc 2>&1 | FileCheck %s
// RUN: %klee -libc=uclibc -posix-runtime -output-dir=%t-O2.klee-out -detect-infinite-loops -stop-after-n-instructions=100000 -allocate-determ %t-O2.bc 2>&1 | FileCheck %s
// RUN: test -f %t-O2.klee-out/test000001.infty.err

// RUN: rm -rf %t-O3.klee-out
// RUN: %klee -libc=uclibc -posix-runtime -output-dir=%t-O3.klee-out -detect-infinite-loops -stop-after-n-instructions=10000 -allocate-determ %t-O3.bc 2>&1 | FileCheck %s
// RUN: %klee -libc=uclibc -posix-runtime -output-dir=%t-O3.klee-out -detect-infinite-loops -stop-after-n-instructions=100000 -allocate-determ %t-O3.bc 2>&1 | FileCheck %s
// RUN: test -f %t-O3.klee-out/test000001.infty.err

#include <inttypes.h>
Expand Down

0 comments on commit 4304ee2

Please sign in to comment.