Don't use the "inlined" feature of ANTLR 3.2, which causes a buffer overflow conditio...
authorMorgan Deters <mdeters@gmail.com>
Wed, 13 Jun 2012 19:50:35 +0000 (19:50 +0000)
committerMorgan Deters <mdeters@gmail.com>
Wed, 13 Jun 2012 19:50:35 +0000 (19:50 +0000)
commit4b3ce37b3d5245d8827d04e4f459c32631083613
tree61a4ab0e9c0d39656b02f668bfed4217b088ecb0
parent0f0f135f98372e32dafb0e70aa918f92b57ae8c7
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.
Makefile
config/antlr.m4
contrib/Makefile.am
contrib/get-antlr-3.4 [new file with mode: 0755]
src/main/driver.cpp
src/main/driver_portfolio.cpp
src/parser/cvc/Cvc.g
src/parser/smt/Smt.g
src/parser/smt2/Smt2.g