Fix. Some of the test cases are now build with the c-compiler rather than just the...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1599 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index 0c4e0973414ab78b8c0e0da399dca2be0a6217d8..693a29bb5bf986a8e7009b6da7066813534165bf 100644 (file)
--- 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 ce98565427210df08a0fa209a5ea527188c1e859..96e948b232a74d1060c994a8ff10157de7f72ea5 100644 (file)
--- 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 <stdio.h>
 #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 dfaa735c4cf3c48dcc869358e13d6bbe1146873f..4453020d5206ab36d068de5cad5bf4fe91536ce6 100644 (file)
--- 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 daca81f053884f00ea48a6a69f9588870ddaf2d6..3f02edee99c7be25c1d1d4bc10f099db48ff68a0 100644 (file)
--- 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 e0e2f2c4fe6113666b7ac8727d76d435655959b5..4953f3a7e1e1f62adfcbd7d30ba1e726dfaf6c00 100644 (file)
--- 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 54a73c15ec7434ec43e2900dd4c352659776f267..8ebbdd81355d0c8c45977020772a2bfe5c0a39cb 100644 (file)
--- 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 <stdio.h>
 #include "c_interface.h"
 #include <iostream>
@@ -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;
 }