addressed some concerns raised by Clark in bug #6 (code review of driver code)

diff --git a/src/main/about.h b/src/main/about.h
index e81e04288befcc6cb501bdad8b2eed37c479f26d..592c09551e9a6d0f41c58c0ae707794559363dad 100644 (file)
--- 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 ec4ee11a57afc3ee050d897cb4aabeac8ce975da..24c96f69ad5f60c5e7dbece5037e4308538b9a67 100644 (file)
--- 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 ff19110c4ad63142934605f7fd67f23896220c98..0141e28487ad2ebad9b928e5e6c3ba8571d9eb52 100644 (file)
--- 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 0b503cdb2895c73608d9f052dd6da8679be1d599..d48c1c96d1063c84bcef1a241a9a6047b25302f4 100644 (file)
--- 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 e2333b41759d8ba12a6f978f428ffdc49ccf3ee7..94a295d5418fa3e465144ba4cc93f64b0afb883b 100644 (file)
--- 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();