From: vijay_ganesh Date: Fri, 28 Aug 2009 20:28:03 +0000 (+0000) Subject: Introduced a C API regression option 'make regress_c_api'. Only one test fails: due... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=e32a218bddccf8cd394fa8fb290cfb1eb4aa8f8b;p=francis%2Fstp.git Introduced a C API regression option 'make regress_c_api'. Only one test fails: due to printing error in cvc-2-C git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@153 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/Makefile b/Makefile index 24ddc7c..7294e80 100644 --- a/Makefile +++ b/Makefile @@ -77,8 +77,8 @@ REGRESS_LOG = `date +%Y-%m-%d`"-regress.log" PROGNAME=bin/stp ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS) -.PHONY: regress -regress: +.PHONY: regressall +regressall: @echo "*********************************************************" \ | tee -a $(REGRESS_LOG) @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG) @@ -126,18 +126,25 @@ regress_smt: @echo "*********************************************************" \ | tee -a $(REGRESS_LOG) - -.PHONY: regressall -regressall: - $(MAKE) regress +.PHONY: regress_c_api +regress_c_api: + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG) + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + $(MAKE) -C tests/c-api-tests 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ] + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG) + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) GRIND_LOG = `date +%Y-%m-%d`"-grind.log" GRINDPROG = valgrind --leak-check=full --undef-value-errors=no GRIND_TAR = $(BIN_DIR)/stp -d GRIND_CALL = -vc "$(GRINDPROG) $(GRIND_TAR)" GRIND_OPTIONS = -l $(REGRESS_LEVEL) -rt $(GRIND_CALL) $(REGRESS_TESTS) - - .PHONY: grind grind: diff --git a/scripts/Makefile.in b/scripts/Makefile.in index 24ddc7c..7294e80 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -77,8 +77,8 @@ REGRESS_LOG = `date +%Y-%m-%d`"-regress.log" PROGNAME=bin/stp ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS) -.PHONY: regress -regress: +.PHONY: regressall +regressall: @echo "*********************************************************" \ | tee -a $(REGRESS_LOG) @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG) @@ -126,18 +126,25 @@ regress_smt: @echo "*********************************************************" \ | tee -a $(REGRESS_LOG) - -.PHONY: regressall -regressall: - $(MAKE) regress +.PHONY: regress_c_api +regress_c_api: + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG) + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + $(MAKE) -C tests/c-api-tests 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ] + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) + @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG) + @echo "*********************************************************" \ + | tee -a $(REGRESS_LOG) GRIND_LOG = `date +%Y-%m-%d`"-grind.log" GRINDPROG = valgrind --leak-check=full --undef-value-errors=no GRIND_TAR = $(BIN_DIR)/stp -d GRIND_CALL = -vc "$(GRINDPROG) $(GRIND_TAR)" GRIND_OPTIONS = -l $(REGRESS_LEVEL) -rt $(GRIND_CALL) $(REGRESS_TESTS) - - .PHONY: grind grind: diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h index 04f2837..78ebf4a 100644 --- a/src/c_interface/c_interface.h +++ b/src/c_interface/c_interface.h @@ -144,7 +144,7 @@ extern "C" { //! Prints asserts to stdout. The flag simplify_print must be set to //"1" if you wish simplification to occur dring printing. It must be //set to "0" otherwise - void vc_printAsserts(VC vc, int simplify_print); + void vc_printAsserts(VC vc, int simplify_print=0); //! Prints the state of the query to malloc'd buffer '*buf' and //stores ! the length of the buffer to '*len'. It is the diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile new file mode 100644 index 0000000..a5d7040 --- /dev/null +++ b/tests/c-api-tests/Makefile @@ -0,0 +1,44 @@ + +all: + g++ -DEXT_HASH_MAP array-cvcl-02.c -I../../src/c_interface -L../../lib -lstp -o a0.out + ./a0.out + g++ -DEXT_HASH_MAP b4-c.c -I../../src/c_interface -L../../lib -lstp -o a1.out + ./a1.out + g++ -DEXT_HASH_MAP b4-c2.c -I../../src/c_interface -L../../lib -lstp -o a2.out + ./a2.out + g++ -DEXT_HASH_MAP getbvunsignedlonglong-check.c -I../../src/c_interface -L../../lib -lstp -o a3.out + ./a3.out + g++ -DEXT_HASH_MAP multiple-queries.c -I../../src/c_interface -L../../lib -lstp -o a4.out + ./a4.out + g++ -DEXT_HASH_MAP parsefile-using-cinterface.c -I../../src/c_interface -L../../lib -lstp -o a5.out + ./a5.out + g++ -DEXT_HASH_MAP print.c -I../../src/c_interface -L../../lib -lstp -o a6.out + ./a6.out + g++ -DEXT_HASH_MAP push-pop-1.c -I../../src/c_interface -L../../lib -lstp -o a7.out + ./a7.out + g++ -DEXT_HASH_MAP sbvmod.c -I../../src/c_interface -L../../lib -lstp -o a8.out + ./a8.out + g++ -DEXT_HASH_MAP simplify.c -I../../src/c_interface -L../../lib -lstp -o a9.out + ./a9.out + g++ -DEXT_HASH_MAP simplify1.c -I../../src/c_interface -L../../lib -lstp -o a10.out + ./a10.out + g++ -DEXT_HASH_MAP squares-leak.c -I../../src/c_interface -L../../lib -lstp -o a11.out + ./a11.out + g++ -DEXT_HASH_MAP stp-counterex.c -I../../src/c_interface -L../../lib -lstp -o a12.out + ./a12.out + g++ -DEXT_HASH_MAP stp-div-001.c -I../../src/c_interface -L../../lib -lstp -o a13.out + ./a13.out + g++ -DEXT_HASH_MAP stpcheck.c -I../../src/c_interface -L../../lib -lstp -o a14.out + ./a14.out + g++ -DEXT_HASH_MAP x.c -I../../src/c_interface -L../../lib -lstp -o a15.out + ./a15.out + g++ -DEXT_HASH_MAP y.c -I../../src/c_interface -L../../lib -lstp -o a16.out + ./a16.out + g++ -DEXT_HASH_MAP push-pop.c -I../../src/c_interface -L../../lib -lstp -o a17.out + ./a17.out + g++ -DEXT_HASH_MAP cvc-to-c.cpp -I../../src/c_interface -L../../lib -lstp -o a18.out + ./a18.out ./t.cvc + + +clean: + rm -rf *~ *.out \ No newline at end of file diff --git a/tests/c-api-tests/t.cvc b/tests/c-api-tests/t.cvc index 0a6f9f4..0736f42 100644 --- a/tests/c-api-tests/t.cvc +++ b/tests/c-api-tests/t.cvc @@ -130,3 +130,4 @@ ASSERT( NOT(0hex00 = arr666[0hex00000003] ); ASSERT( 0hex00 = arr666[0hex00000004] ); +QUERY FALSE; \ No newline at end of file