diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/Coverage/ReplayOutDir.c | 2 | ||||
-rw-r--r-- | test/Feature/AliasFunction.c | 2 | ||||
-rw-r--r-- | test/Feature/AliasFunctionExit.c | 2 | ||||
-rw-r--r-- | test/Feature/MakeSymbolicName.c | 2 | ||||
-rw-r--r-- | test/Feature/NamedSeedMatching.c | 16 | ||||
-rw-r--r-- | test/Feature/const_array_opt1.c | 2 | ||||
-rw-r--r-- | test/Makefile | 4 | ||||
-rw-r--r-- | test/regression/2007-10-12-failed-make-symbolic-after-copy.c | 4 | ||||
-rw-r--r-- | test/regression/2008-04-10-bad-alloca-free.c | 2 |
9 files changed, 18 insertions, 18 deletions
diff --git a/test/Coverage/ReplayOutDir.c b/test/Coverage/ReplayOutDir.c index 3ca6fb80..ca7e590a 100644 --- a/test/Coverage/ReplayOutDir.c +++ b/test/Coverage/ReplayOutDir.c @@ -5,7 +5,7 @@ int main() { int i; - klee_make_symbolic(&i, sizeof i); + klee_make_symbolic(&i, sizeof i, "i"); klee_print_range("i", i); return 0; } diff --git a/test/Feature/AliasFunction.c b/test/Feature/AliasFunction.c index e7acfc19..16d89ef6 100644 --- a/test/Feature/AliasFunction.c +++ b/test/Feature/AliasFunction.c @@ -11,7 +11,7 @@ void bar() { printf(" bar()\n"); } int main() { int x; - klee_make_symbolic_name(&x, sizeof(x), "x"); + klee_make_symbolic(&x, sizeof(x), "x"); // no aliases foo(); diff --git a/test/Feature/AliasFunctionExit.c b/test/Feature/AliasFunctionExit.c index fcaf7e6c..4bda950a 100644 --- a/test/Feature/AliasFunctionExit.c +++ b/test/Feature/AliasFunctionExit.c @@ -22,7 +22,7 @@ void end(int status) { int main() { int x; - klee_make_symbolic_name(&x, sizeof(x), "x"); + klee_make_symbolic(&x, sizeof(x), "x"); klee_alias_function("exit", "end"); start(x); diff --git a/test/Feature/MakeSymbolicName.c b/test/Feature/MakeSymbolicName.c index c1f11424..a4d4e2a6 100644 --- a/test/Feature/MakeSymbolicName.c +++ b/test/Feature/MakeSymbolicName.c @@ -7,7 +7,7 @@ int main() { int a[4] = {1, 2, 3, 4}; unsigned i; - klee_make_symbolic_name(&i, sizeof(i), "index"); + klee_make_symbolic(&i, sizeof(i), "index"); if (i > 3) klee_silent_exit(0); diff --git a/test/Feature/NamedSeedMatching.c b/test/Feature/NamedSeedMatching.c index 6d52e7a4..cff34282 100644 --- a/test/Feature/NamedSeedMatching.c +++ b/test/Feature/NamedSeedMatching.c @@ -16,20 +16,20 @@ int main(int argc, char **argv) { int a, b, c, x; if (argc==2 && strcmp(argv[1], "initial") == 0) { - klee_make_symbolic_name(&a, sizeof a, "a"); - klee_make_symbolic_name(&b, sizeof b, "b"); - klee_make_symbolic_name(&c, sizeof c, "c"); - klee_make_symbolic_name(&x, sizeof x, "a"); + klee_make_symbolic(&a, sizeof a, "a"); + klee_make_symbolic(&b, sizeof b, "b"); + klee_make_symbolic(&c, sizeof c, "c"); + klee_make_symbolic(&x, sizeof x, "a"); klee_assume(a == 3); klee_assume(b == 4); klee_assume(c == 5); klee_assume(x == 6); } else { - klee_make_symbolic_name(&a, sizeof a, "a"); - klee_make_symbolic_name(&c, sizeof c, "c"); - klee_make_symbolic_name(&b, sizeof b, "b"); - klee_make_symbolic_name(&x, sizeof x, "a"); + klee_make_symbolic(&a, sizeof a, "a"); + klee_make_symbolic(&c, sizeof c, "c"); + klee_make_symbolic(&b, sizeof b, "b"); + klee_make_symbolic(&x, sizeof x, "a"); } if (a==3) printf("a==3\n"); diff --git a/test/Feature/const_array_opt1.c b/test/Feature/const_array_opt1.c index 96c46fb9..09ed07fd 100644 --- a/test/Feature/const_array_opt1.c +++ b/test/Feature/const_array_opt1.c @@ -20,7 +20,7 @@ int main() { for (i=0; i<N; i++) a[i] = i % 256; - klee_make_symbolic_name(k, sizeof(k), "k"); + klee_make_symbolic(k, sizeof(k), "k"); for (i=0; i<N_IDX; i++) { if (k[i] >= N) diff --git a/test/Makefile b/test/Makefile index 0c42a6f6..8cd8688a 100644 --- a/test/Makefile +++ b/test/Makefile @@ -89,8 +89,8 @@ site.exp: Makefile $(LEVEL)/Makefile.config @echo 'set compile_c "$(CC) $(CPP.Flags) $(C.Flags) $(CompileCommonOpts) -c "' >>site.tmp @echo 'set compile_cxx "$(CXX) $(CPP.Flags) $(CXX.Flags) $(CompileCommonOpts) - c"' >> site.tmp @echo 'set link "$(CXX) $(CPP.Flags) $(CXX.Flags) $(CompileCommonOpts) $(LD.Flags)"' >>site.tmp - @echo 'set llvmgcc "$(LLVMGCC)"' >> site.tmp - @echo 'set llvmgxx "$(LLVMGCC)"' >> site.tmp + @echo 'set llvmgcc "$(LLVMGCC) -m32"' >> site.tmp + @echo 'set llvmgxx "$(LLVMGCC) -m32"' >> site.tmp @echo 'set llvmgccmajvers "$(LLVMGCC_MAJVERS)"' >> site.tmp @echo 'set shlibext "$(SHLIBEXT)"' >> site.tmp @echo '## All variables above are generated by configure. Do Not Edit ## ' >>site.tmp diff --git a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c index 144281fa..9d81fad0 100644 --- a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c +++ b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c @@ -5,13 +5,13 @@ int main() { unsigned x, y[4]; - klee_make_symbolic(&x,sizeof x); + klee_make_symbolic(&x, sizeof x, "x"); if (x>=4) klee_silent_exit(0); y[x] = 0; if (x) { // force branch so y is copied - klee_make_symbolic(&y, sizeof y); + klee_make_symbolic(&y, sizeof y, "y"); if (y[x]==0) klee_silent_exit(0); return 0; // should be reachable } else { diff --git a/test/regression/2008-04-10-bad-alloca-free.c b/test/regression/2008-04-10-bad-alloca-free.c index 46e2b0cf..a6215f64 100644 --- a/test/regression/2008-04-10-bad-alloca-free.c +++ b/test/regression/2008-04-10-bad-alloca-free.c @@ -2,7 +2,7 @@ // RUN: %klee --exit-on-error %t1.bc void f(int *addr) { - klee_make_symbolic_name(addr, sizeof *addr, "moo"); + klee_make_symbolic(addr, sizeof *addr, "moo"); } int main() { |