summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/main/about.h4
-rw-r--r--src/main/getopt.cpp6
-rw-r--r--src/main/main.h2
-rw-r--r--src/main/usage.h2
-rw-r--r--src/main/util.cpp2
5 files changed, 11 insertions, 5 deletions
diff --git a/src/main/about.h b/src/main/about.h
index e81e04288..592c09551 100644
--- a/src/main/about.h
+++ b/src/main/about.h
@@ -7,7 +7,7 @@
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** [[ Add file-specific comments here ]]
+ ** The "about" string for the CVC4 driver binary.
**/
#ifndef __CVC4__MAIN__ABOUT_H
@@ -26,4 +26,4 @@ Copyright (C) 2009 The ACSys Group\n\
}/* CVC4::main namespace */
}/* CVC4 namespace */
-#endif /* __CVC4_MAIN_H */
+#endif /* __CVC4__MAIN__ABOUT_H */
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index ec4ee11a5..24c96f69a 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -41,11 +41,13 @@ Languages currently supported as arguments to the -L / --lang option:\n\
smt | smtlib SMT-LIB format\n\
";
+// FIXME add a comment here describing the purpose of this
enum OptionValue {
SMTCOMP = 256, /* no clash with char options */
STATS
};/* enum OptionValue */
+// FIXME add a comment here describing the option array
static struct option cmdlineOptions[] = {
// name, has_arg, *flag, val
{ "help" , no_argument , NULL, 'h' },
@@ -56,7 +58,7 @@ static struct option cmdlineOptions[] = {
{ "debug" , required_argument, NULL, 'd' },
{ "smtcomp", no_argument , NULL, SMTCOMP },
{ "stats" , no_argument , NULL, STATS }
-};
+};/* if you add things to the above, please remember to update usage.h! */
int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionException) {
const char *progName = argv[0];
@@ -69,6 +71,7 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
}
opts->binary_name = string(progName);
+ // FIXME add a comment here describing the option string
while((c = getopt_long(argc, argv, "+:hVvqL:d:", cmdlineOptions, NULL)) != -1) {
switch(c) {
@@ -110,6 +113,7 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
case 'd':
Debug.on(optarg);
+ /* fall-through */
case STATS:
opts->statistics = true;
diff --git a/src/main/main.h b/src/main/main.h
index ff19110c4..0141e2848 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -7,7 +7,7 @@
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** [[ Add file-specific comments here ]]
+ ** Header for main CVC4 driver.
**/
#include <exception>
diff --git a/src/main/usage.h b/src/main/usage.h
index 0b503cdb2..d48c1c96d 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -7,7 +7,7 @@
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** [[ Add file-specific comments here ]]
+ ** The "usage" string for the CVC4 driver binary.
**/
#ifndef __CVC4__MAIN__USAGE_H
diff --git a/src/main/util.cpp b/src/main/util.cpp
index e2333b417..94a295d54 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -25,6 +25,8 @@ using namespace std;
namespace CVC4 {
namespace main {
+// FIXME add comments to functions
+
void sigint_handler(int sig, siginfo_t* info, void*) {
fprintf(stderr, "CVC4 interrupted by user.\n");
abort();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback