Add a C API test for the leak fixed in r1141 (when pushing/popping assertions), enabl...

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

diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index 98bf6a81993d56d515afbce3d2d884e58013f071..11df111eabb0435253e22c18cff7b68fa6e59271 100644 (file)
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -14,7 +14,7 @@ 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
+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
        rm -rf *.out
 
 0:     
@@ -71,7 +71,7 @@ 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 2
        ./a16.out
 17:
        g++  $(CXXFLAGS)  push-pop.c -o a17.out $(LIBS)
-       ./a17.out
+       $(VALGRIND) ./a17.out
 18:
        g++  $(CXXFLAGS)  cvc-to-c.cpp  -o a18.out $(LIBS)
        #./a18.out ./t.cvc
@@ -119,5 +119,9 @@ 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 2
          ../../lib/libstp.a stp-array-model.c ../../lib/libstp.a
        ./a27.out
 
+28:
+       g++ $(CXXFLAGS) push-no-pop.c -o a28.out $(LIBS)
+       $(VALGRIND) ./a28.out
+
 clean:
        rm -rf *~ *.out *.dSYM

diff --git a/tests/c-api-tests/push-no-pop.c b/tests/c-api-tests/push-no-pop.c
new file mode 100644 (file)
index 0000000..daca81f
--- /dev/null
+++ b/tests/c-api-tests/push-no-pop.c
@@ -0,0 +1,41 @@
+/* g++ -I$(HOME)/stp/c_interface push-no-pop.c -L$(HOME)/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_setFlags(vc,'v');
+  //vc_setFlags(vc,'s');
+
+  Type bv8 = vc_bvType(vc, 8);
+
+  Expr a = vc_varExpr(vc, "a", bv8);
+  Expr ct_0 = vc_bvConstExprFromInt(vc, 8, 0);
+
+  Expr a_eq_0 = vc_eqExpr(vc, a, ct_0);
+
+  int query = vc_query(vc, a_eq_0);
+  printf("query = %d\n", query);
+
+  Expr a_neq_0 = vc_notExpr(vc,a_eq_0);
+  vc_assertFormula(vc,a_eq_0);
+  vc_push(vc);
+
+  Expr queryexp = vc_eqExpr(vc, a, vc_bvConstExprFromInt(vc, 8, 0));
+
+  query = vc_query(vc, queryexp);
+  vc_printCounterExample(vc);
+  printf("query = %d\n", query);
+
+  vc_DeleteExpr(queryexp);
+  vc_DeleteExpr(a_neq_0);
+  vc_DeleteExpr(a_eq_0);
+  vc_DeleteExpr(a);
+
+  vc_Destroy(vc);
+}
+