summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/Makefile.am8
-rw-r--r--src/main/command_executor.cpp4
-rw-r--r--src/main/driver_unified.cpp4
-rw-r--r--src/main/options_handlers.h12
-rw-r--r--src/main/util.cpp20
5 files changed, 34 insertions, 14 deletions
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 952951655..64a43eb02 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -41,9 +41,9 @@ pcvc4_LDADD += $(BOOST_THREAD_LIBS) -lpthread
pcvc4_LDADD += $(BOOST_THREAD_LDFLAGS)
if STATIC_BINARY
-pcvc4_LINK = $(CXXLINK) -all-static
+pcvc4_LINK = $(CXXLINK) -all-static $(pcvc4_LDFLAGS)
else
-pcvc4_LINK = $(CXXLINK)
+pcvc4_LINK = $(CXXLINK) $(pcvc4_LDFLAGS)
endif
endif
@@ -87,8 +87,8 @@ clean-local:
rm -f $(BUILT_SOURCES)
if STATIC_BINARY
-cvc4_LINK = $(CXXLINK) -all-static
+cvc4_LINK = $(CXXLINK) -all-static $(cvc4_LDFLAGS)
else
-cvc4_LINK = $(CXXLINK)
+cvc4_LINK = $(CXXLINK) $(cvc4_LDFLAGS)
endif
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 14625f1d8..6a4e18b5b 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -48,7 +48,7 @@ bool CommandExecutor::doCommand(Command* cmd)
return status;
} else {
- if(d_options[options::verbosity] > 0) {
+ if(d_options[options::verbosity] > 2) {
*d_options[options::out] << "Invoking: " << *cmd << std::endl;
}
@@ -59,7 +59,7 @@ bool CommandExecutor::doCommand(Command* cmd)
bool CommandExecutor::doCommandSingleton(Command *cmd)
{
bool status = true;
- if(d_options[options::verbosity] >= 0) {
+ if(d_options[options::verbosity] >= -1) {
status = smtEngineInvoke(&d_smtEngine, cmd, d_options[options::out]);
} else {
status = smtEngineInvoke(&d_smtEngine, cmd, NULL);
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 741975b11..9fa40d3ab 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -239,7 +239,9 @@ int runCvc4(int argc, char* argv[], Options& opts) {
InteractiveShell shell(*exprMgr, opts);
Message() << Configuration::getPackageName()
<< " " << Configuration::getVersionString();
- if(Configuration::isSubversionBuild()) {
+ if(Configuration::isGitBuild()) {
+ Message() << " [" << Configuration::getGitId() << "]";
+ } else if(Configuration::isSubversionBuild()) {
Message() << " [" << Configuration::getSubversionId() << "]";
}
Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h
index c2eb489ed..f14a67d5f 100644
--- a/src/main/options_handlers.h
+++ b/src/main/options_handlers.h
@@ -26,14 +26,20 @@ inline void showConfiguration(std::string option, SmtEngine* smt) {
fputs(Configuration::about().c_str(), stdout);
printf("\n");
printf("version : %s\n", Configuration::getVersionString().c_str());
- if(Configuration::isSubversionBuild()) {
- printf("subversion : yes [%s r%u%s]\n",
+ if(Configuration::isGitBuild()) {
+ printf("scm : git [%s %s%s]\n",
+ Configuration::getGitBranchName(),
+ std::string(Configuration::getGitCommit()).substr(0, 8).c_str(),
+ Configuration::hasGitModifications() ?
+ " (with modifications)" : "");
+ } else if(Configuration::isSubversionBuild()) {
+ printf("scm : svn [%s r%u%s]\n",
Configuration::getSubversionBranchName(),
Configuration::getSubversionRevision(),
Configuration::hasSubversionModifications() ?
" (with modifications)" : "");
} else {
- printf("subversion : %s\n", Configuration::isSubversionBuild() ? "yes" : "no");
+ printf("scm : no\n");
}
printf("\n");
printf("library : %u.%u.%u\n",
diff --git a/src/main/util.cpp b/src/main/util.cpp
index d4d3e96d8..a6fcddf3b 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -19,10 +19,15 @@
#include <cerrno>
#include <exception>
#include <string.h>
+
+#ifndef __WIN32__
+
#include <signal.h>
#include <sys/resource.h>
#include <unistd.h>
+#endif /* __WIN32__ */
+
#include "util/exception.h"
#include "options/options.h"
#include "util/statistics.h"
@@ -44,9 +49,6 @@ namespace CVC4 {
namespace main {
-size_t cvc4StackSize;
-void* cvc4StackBase;
-
/**
* If true, will not spin on segfault even when CVC4_DEBUG is on.
* Useful for nightly regressions, noninteractive performance runs
@@ -54,6 +56,11 @@ void* cvc4StackBase;
*/
bool segvNoSpin = false;
+#ifndef __WIN32__
+
+size_t cvc4StackSize;
+void* cvc4StackBase;
+
/** Handler for SIGXCPU, i.e., timeout. */
void timeout_handler(int sig, siginfo_t* info, void*) {
fprintf(stderr, "CVC4 interrupted by timeout.\n");
@@ -150,10 +157,12 @@ void ill_handler(int sig, siginfo_t* info, void*) {
#endif /* CVC4_DEBUG */
}
+#endif /* __WIN32__ */
+
static terminate_handler default_terminator;
void cvc4unexpected() {
-#ifdef CVC4_DEBUG
+#if defined(CVC4_DEBUG) && !defined(__WIN32__)
fprintf(stderr, "\n"
"CVC4 threw an \"unexpected\" exception (one that wasn't properly "
"specified\nin the throws() specifier for the throwing function)."
@@ -214,6 +223,7 @@ void cvc4terminate() {
/** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */
void cvc4_init() throw(Exception) {
+#ifndef __WIN32__
stack_t ss;
ss.ss_sp = malloc(SIGSTKSZ);
if(ss.ss_sp == NULL) {
@@ -272,6 +282,8 @@ void cvc4_init() throw(Exception) {
throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno));
}
+#endif /* __WIN32__ */
+
set_unexpected(cvc4unexpected);
default_terminator = set_terminate(cvc4terminate);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback