diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-06-13 19:50:35 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-06-13 19:50:35 +0000 |
| commit | 4b3ce37b3d5245d8827d04e4f459c32631083613 (patch) | |
| tree | 61a4ab0e9c0d39656b02f668bfed4217b088ecb0 /Makefile | |
| parent | 0f0f135f98372e32dafb0e70aa918f92b57ae8c7 (diff) | |
Don't use the "inlined" feature of ANTLR 3.2, which causes a buffer overflow condition when reading from stdin. This should completely resolve bug #319.
However, on large inputs especially (like the stp/testcase benchmarks), this inlining feature can speed parsing by 5-10%, at the cost of not supporting interactive sessions on stdin (like in the SMT-COMP application track).
So I updated the submission script and competition build so that
* a competition build with antlr-inlining is built for the main and parallel tracks
* a competition build without antlr-inlining is built for the application track
Again, the effect is only when reading the stdin stream (but that's how SMT-COMP works). For normal (non-competition) builds, we need to support interactive sessions (from e.g. KIND) on stdin, so this inlining is off for all builds except main- and parallel-track competition builds.
Also added a "get-antlr-3.4" script that automatically downloads and locally installs a copy of libantlr3c and the antlr parser generator inside the CVC4 source tree.
Closing bug #319.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 15 |
1 files changed, 14 insertions, 1 deletions
@@ -43,6 +43,12 @@ examples: all YEAR := $(shell date +%Y) submission: + @if [ -n "`ls src/parser/*/generated`" ]; then \ + echo 'ERROR:' >&2; \ + echo 'ERROR: Please make maintainer-clean first.' >&2; \ + echo 'ERROR:' >&2; \ + exit 1; \ + fi if [ ! -e configure ]; then ./autogen.sh; fi ./configure competition --disable-shared --enable-static-binary --with-cln --with-portfolio $(MAKE) @@ -64,7 +70,14 @@ submission: echo 'exec ./pcvc4 -L smt2 --no-interactive' ) > cvc4-parallel-smtcomp-$(YEAR)/run chmod 755 cvc4-parallel-smtcomp-$(YEAR)/run tar cf cvc4-parallel-smtcomp-$(YEAR).tar cvc4-parallel-smtcomp-$(YEAR) - # application track + # application track is a separate build + make maintainer-clean + if [ ! -e configure ]; then ./autogen.sh; fi + ./configure competition --disable-shared --enable-static-binary --with-cln CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK + $(MAKE) + strip builds/bin/cvc4 + $(MAKE) regress1 + # package the application track tarball mkdir -p cvc4-application-smtcomp-$(YEAR) cp -p builds/bin/cvc4 cvc4-application-smtcomp-$(YEAR)/cvc4 ( echo '#!/bin/sh'; \ |