Add -lprofiler when --with-google-perftools is offered; also fix some newswire-raised...

diff --git a/configure.ac b/configure.ac
index 25108adcc2f3c7d7fd6ac383a3cb096d09cf40d8..975d032b8107d0a85a336cc0c8c07d479e1847ae 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -721,7 +721,8 @@ AC_ARG_WITH(
 AC_MSG_CHECKING([whether to link in google perftools libraries])
 if test $cvc4_use_google_perftools = 1; then
   AC_MSG_RESULT([yes])
-  AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program])], [-lpthread])
+  AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
+  AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
 else
   AC_MSG_RESULT([no (user didn't request it)])
 fi

diff --git a/src/parser/bounded_token_buffer.h b/src/parser/bounded_token_buffer.h
index a29462687447d4f3dbe4371bd3e136e764f2cd59..5121f1cc6a267c7900d65b55280171d944719289 100644 (file)
--- a/src/parser/bounded_token_buffer.h
+++ b/src/parser/bounded_token_buffer.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -25,6 +25,8 @@
  ** are SKIP()'d and not "hidden".
  **/
 
+#include "cvc4parser_private.h"
+
 #ifndef        __CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H
 #define        __CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H
 

diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index e26c879e47d7ea66e5ee31f6401643f70df17f2f..cbbff95c166ac973979694b4219dfec212a5ff9e 100644 (file)
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file rewriter_tables_template.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Rewriter tables for various theories
+ **
+ ** This file contains template code for the rewriter tables that are generated
+ ** from the Theory kinds files.
+ **/
+
 #pragma once
 
 #include "theory/rewriter.h"
@@ -56,7 +75,6 @@ ${post_rewrite_set_cache}
   }
 }
 
-
 void Rewriter::init() {
 ${rewrite_init}
 }
@@ -65,5 +83,5 @@ void Rewriter::shutdown() {
 ${rewrite_shutdown}
 }
 
-}
-}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */