From adbdf846cfe5fdfd6ab9c318b038371e53cd3050 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 17 Mar 2012 12:07:57 +0000 Subject: [PATCH] Fix. Some of the test cases are now build with the c-compiler rather than just the C++ compiler. Thanks to Spencer Whitman for informing us. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1599 e59a4935-1847-0410-ae03-e826735625c1 --- tests/c-api-tests/Makefile | 74 ++++++++++++++--------------- tests/c-api-tests/array-cvcl-02.c | 15 +++--- tests/c-api-tests/b4-c.c | 10 ++-- tests/c-api-tests/push-no-pop.c | 8 ++-- tests/c-api-tests/stp-array-model.c | 3 +- tests/c-api-tests/timeout.c | 5 +- 6 files changed, 54 insertions(+), 61 deletions(-) diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile index 0c4e097..693a29b 100644 --- a/tests/c-api-tests/Makefile +++ b/tests/c-api-tests/Makefile @@ -4,7 +4,7 @@ TOP = ../.. include $(TOP)/scripts/Makefile.common CXXFLAGS= -DEXT_HASH_MAP $(CFLAGS) -I../../src/c_interface LDFLAGS=-L../../lib -LIBS=$(LDFLAGS) -lstp +LIBS=$(LDFLAGS) -lstp -lstdc++ VALGRINDPATH=`which valgrind` ifeq "$(VALGRINDPATH)" "" @@ -14,117 +14,117 @@ else endif -all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 +all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 rm -rf *.out 0: - g++ $(CXXFLAGS) array-cvcl-02.c -o a0.out $(LIBS) + $(CC) $(CXXFLAGS) array-cvcl-02.c -o a0.out $(LIBS) ./a0.out 1: - g++ $(CXXFLAGS) b4-c.c -lstp -o a1.out $(LIBS) + $(CC) $(CXXFLAGS) b4-c.c -lstp -o a1.out $(LIBS) ./a1.out 2: - g++ $(CXXFLAGS) b4-c2.c -lstp -o a2.out $(LIBS) + $(CXX) $(CXXFLAGS) b4-c2.c -lstp -o a2.out $(LIBS) ./a2.out 3: - g++ $(CXXFLAGS) getbvunsignedlonglong-check.c -o a3.out $(LIBS) + $(CXX) $(CXXFLAGS) getbvunsignedlonglong-check.c -o a3.out $(LIBS) $(VALGRIND) ./a3.out 4: - g++ $(CXXFLAGS) multiple-queries.c -o a4.out $(LIBS) + $(CXX) $(CXXFLAGS) multiple-queries.c -o a4.out $(LIBS) ./a4.out 5: - g++ $(CXXFLAGS) parsefile-using-cinterface.c -o a5.out $(LIBS) + $(CXX) $(CXXFLAGS) parsefile-using-cinterface.c -o a5.out $(LIBS) ./a5.out 6: - g++ $(CXXFLAGS) print.c -o a6.out $(LIBS) + $(CXX) $(CXXFLAGS) print.c -o a6.out $(LIBS) ./a6.out 7: - g++ $(CXXFLAGS) push-pop-1.c -o a7.out $(LIBS) + $(CXX) $(CXXFLAGS) push-pop-1.c -o a7.out $(LIBS) ./a7.out 8: - g++ $(CXXFLAGS) sbvdiv.c -o a8.out $(LIBS) + $(CXX) $(CXXFLAGS) sbvdiv.c -o a8.out $(LIBS) ./a8.out 9: - g++ $(CXXFLAGS) simplify.c -o a9.out $(LIBS) + $(CXX) $(CXXFLAGS) simplify.c -o a9.out $(LIBS) ./a9.out 10: - g++ $(CXXFLAGS) simplify1.c -o a10.out $(LIBS) + $(CXX) $(CXXFLAGS) simplify1.c -o a10.out $(LIBS) ./a10.out 11: - g++ $(CXXFLAGS) squares-leak.c -o a11.out $(LIBS) + $(CXX) $(CXXFLAGS) squares-leak.c -o a11.out $(LIBS) $(VALGRIND) ./a11.out 12: - g++ $(CXXFLAGS) stp-counterex.c -o a12.out $(LIBS) + $(CXX) $(CXXFLAGS) stp-counterex.c -o a12.out $(LIBS) ./a12.out 13: - g++ $(CXXFLAGS) stp-div-001.c -o a13.out $(LIBS) + $(CXX) $(CXXFLAGS) stp-div-001.c -o a13.out $(LIBS) ./a13.out 14: - g++ $(CXXFLAGS) stpcheck.c -o a14.out $(LIBS) + $(CXX) $(CXXFLAGS) stpcheck.c -o a14.out $(LIBS) ./a14.out 15: - g++ $(CXXFLAGS) x.c -o a15.out $(LIBS) + $(CXX) $(CXXFLAGS) x.c -o a15.out $(LIBS) $(VALGRIND) ./a15.out 16: - g++ $(CXXFLAGS) y.c -lstp -o a16.out $(LIBS) + $(CXX) $(CXXFLAGS) y.c -lstp -o a16.out $(LIBS) ./a16.out 17: - g++ $(CXXFLAGS) push-pop.c -o a17.out $(LIBS) + $(CXX) $(CXXFLAGS) push-pop.c -o a17.out $(LIBS) $(VALGRIND) ./a17.out 18: - g++ $(CXXFLAGS) cvc-to-c.cpp -o a18.out $(LIBS) + $(CXX) $(CXXFLAGS) cvc-to-c.cpp -o a18.out $(LIBS) #./a18.out ./t.cvc 19: - g++ -g $(CXXFLAGS) biosat-rna.cpp -o a19.out $(LIBS) + $(CXX) -g $(CXXFLAGS) biosat-rna.cpp -o a19.out $(LIBS) ./a19.out AUUGGUAUGUAAGCUACUUCUUCCAAGACCA 800 20: - g++ -g $(CXXFLAGS) leak.c -o a20.out $(LIBS) + $(CXX) -g $(CXXFLAGS) leak.c -o a20.out $(LIBS) $(VALGRIND) ./a20.out 21: - g++ $(CXXFLAGS) interface-check.c -o a21.out $(LIBS) + $(CXX) $(CXXFLAGS) interface-check.c -o a21.out $(LIBS) ./a21.out 22: - g++ $(CXXFLAGS) parsestring-using-cinterface.c -o a22.out $(LIBS) + $(CXX) $(CXXFLAGS) parsestring-using-cinterface.c -o a22.out $(LIBS) ./a22.out # Test 23 is the same as test 0, except linked in a different order. # This is meant to catch problems in which libstp.a contains a # main() function or has extra dependencies. 23: - g++ $(CXXFLAGS) -o a23.out \ - ../../lib/libstp.a array-cvcl-02.c ../../lib/libstp.a + $(CXX) $(CXXFLAGS) -o a23.out \ + ../../lib/libstp.a array-cvcl-02.c $(LIBS) ./a23.out 24: - g++ $(CXXFLAGS) -o a24.out \ - ../../lib/libstp.a if-check.c ../../lib/libstp.a + $(CXX) $(CXXFLAGS) -o a24.out \ + ../../lib/libstp.a if-check.c $(LIBS) ./a24.out 25: - g++ $(CXXFLAGS) -o a25.out \ - ../../lib/libstp.a stp-bool.c ../../lib/libstp.a + $(CXX) $(CXXFLAGS) -o a25.out \ + ../../lib/libstp.a stp-bool.c $(LIBS) ./a25.out 26: - g++ $(CXXFLAGS) -o a26.out \ - ../../lib/libstp.a stp-test3.c ../../lib/libstp.a + $(CC) $(CXXFLAGS) -o a26.out \ + ../../lib/libstp.a stp-test3.c $(LIBS) ./a26.out 27: - g++ $(CXXFLAGS) -o a27.out \ - ../../lib/libstp.a stp-array-model.c ../../lib/libstp.a + $(CC) $(CXXFLAGS) -o a27.out \ + ../../lib/libstp.a stp-array-model.c $(LIBS) ./a27.out 28: - g++ $(CXXFLAGS) push-no-pop.c -o a28.out $(LIBS) + $(CC) $(CXXFLAGS) push-no-pop.c -o a28.out $(LIBS) $(VALGRIND) ./a28.out 29: - g++ $(CXXFLAGS) timeout.c -o a29.out $(LIBS) + $(CXX) $(CXXFLAGS) timeout.c -o a29.out $(LIBS) ./a29.out clean: diff --git a/tests/c-api-tests/array-cvcl-02.c b/tests/c-api-tests/array-cvcl-02.c index ce98565..96e948b 100644 --- a/tests/c-api-tests/array-cvcl-02.c +++ b/tests/c-api-tests/array-cvcl-02.c @@ -1,15 +1,10 @@ -/* -g++ -DEXT_HASH_MAP array-cvcl-02.c -I/home/vganesh/stp/c_interface -L/home/vganesh/stp/lib -lstp -o cc -*/ - - #include #include "c_interface.h" int main() { VC vc = vc_createValidityChecker(); - vc_setFlags(vc,'n'); - vc_setFlags(vc,'d'); - vc_setFlags(vc,'p'); + vc_setFlag(vc,'n'); + vc_setFlag(vc,'d'); + vc_setFlag(vc,'p'); Expr cvcl_array = vc_varExpr1(vc, "a",32,32); Expr i = vc_varExpr1(vc, "i", 0, 8); @@ -37,7 +32,8 @@ int main() { long long v; Expr pre = vc_bvConstExprFromInt(vc,24,0); - for(int j=0;j<10;j++) { + int j; + for(j=0;j<10;j++) { Expr exprj = vc_bvConstExprFromInt(vc,8,j); Expr index = vc_bvConcatExpr(vc, pre, exprj); index = vc_simplify(vc,index); @@ -46,4 +42,5 @@ int main() { } vc_Destroy(vc); //vc_printCounterExample(vc); + return 0; } diff --git a/tests/c-api-tests/b4-c.c b/tests/c-api-tests/b4-c.c index dfaa735..4453020 100644 --- a/tests/c-api-tests/b4-c.c +++ b/tests/c-api-tests/b4-c.c @@ -3,12 +3,9 @@ int main() { VC vc = vc_createValidityChecker(); - vc_setFlags(vc,'v'); - vc_setFlags(vc,'s'); - vc_setFlags(vc,'n'); - //vc_setFlags(vc,'a'); - //vc_setFlags(vc,'w'); - //vc_setFlags(vc,'r'); + vc_setFlag(vc,'v'); + vc_setFlag(vc,'s'); + vc_setFlag(vc,'n'); //vc_push(vc); Expr e12866 = vc_varExpr(vc, "at", vc_bvType(vc, 5)); @@ -284,4 +281,5 @@ int main() //vc_pop(vc); //vc_pop(vc); vc_Destroy(vc); + return 0; } diff --git a/tests/c-api-tests/push-no-pop.c b/tests/c-api-tests/push-no-pop.c index daca81f..3f02ede 100644 --- a/tests/c-api-tests/push-no-pop.c +++ b/tests/c-api-tests/push-no-pop.c @@ -5,11 +5,9 @@ int main() { VC vc = vc_createValidityChecker(); - vc_setFlags(vc,'n'); - vc_setFlags(vc,'d'); - vc_setFlags(vc,'p'); - //vc_setFlags(vc,'v'); - //vc_setFlags(vc,'s'); + vc_setFlag(vc,'n'); + vc_setFlag(vc,'d'); + vc_setFlag(vc,'p'); Type bv8 = vc_bvType(vc, 8); diff --git a/tests/c-api-tests/stp-array-model.c b/tests/c-api-tests/stp-array-model.c index e0e2f2c..4953f3a 100644 --- a/tests/c-api-tests/stp-array-model.c +++ b/tests/c-api-tests/stp-array-model.c @@ -43,7 +43,8 @@ int main() { exit(3); } - for (int j = 0; j < size; ++j) { + int j; + for (j = 0; j < size; ++j) { Expr index = vc_getCounterExample(vc, indices[j]); Expr value = vc_getCounterExample(vc, values[j]); unsigned long long i = getBVUnsigned(index); diff --git a/tests/c-api-tests/timeout.c b/tests/c-api-tests/timeout.c index 54a73c1..8ebbdd8 100644 --- a/tests/c-api-tests/timeout.c +++ b/tests/c-api-tests/timeout.c @@ -1,5 +1,3 @@ -//g++ -I$(HOME)/stp/c_interface print.c -L$(HOME)/stp/lib -lstp -o hex - #include #include "c_interface.h" #include @@ -16,9 +14,10 @@ int main() { { int time = rand() % 7000; std::cout << "Timeout : " << time << " : result " ; - std::cout << vc_query(vc,vc_falseExpr(vc),time) << std::endl; + std::cout << vc_query_with_timeout(vc,vc_falseExpr(vc),time) << std::endl; } vc_DeleteExpr(c); vc_Destroy(vc); + return 0; } -- 2.47.3