progPath = argv[0];
// Parse the options
- vector<string> filenames = opts.parseOptions(argc, argv);
+ vector<string> filenames = Options::parseOptions(&opts, argc, argv);
# ifndef PORTFOLIO_BUILD
if( opts.wasSetByUserThreads() ||
*vp++ = NULL;
if(targc > 1) { // this is necessary in case you do e.g. --thread0=" "
try {
- tOpts.parseOptions(targc, targv);
+ Options::parseOptions(&tOpts, targc, targv);
} catch(OptionException& e) {
stringstream ss;
ss << optid << ": " << e.getMessage();
arith_propagation_mode.h \
arith_unate_lemma_mode.cpp \
arith_unate_lemma_mode.h \
- argument_extender.cpp \
+ argument_extender_implementation.cpp \
+ argument_extender_implementation.h \
argument_extender.h \
base_handlers.h \
boolean_term_conversion_mode.cpp \
+++ /dev/null
-/********************* */
-/*! \file preempt_get_option.h
- ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Utility function for parsing commandline options.
- **
- ** Utility function for parsing commandline options.
- **/
-
-#include "options/argument_extender.h"
-
-#include <cstdlib>
-#include <cstring>
-#include <vector>
-
-#include "base/cvc4_assert.h"
-#include "base/output.h"
-
-namespace CVC4 {
-namespace options {
-
-ArgumentExtender::ArgumentExtender(unsigned additional, size_t length)
- : d_additional(additional)
- , d_length(length)
-{
- AlwaysAssert(d_additional >= 1);
- AlwaysAssert(d_length >= 1);
-}
-
-ArgumentExtender::~ArgumentExtender(){}
-
-unsigned ArgumentExtender::getIncrease() const { return d_additional; }
-size_t ArgumentExtender::getLength() const { return d_length; }
-
-void ArgumentExtender::extend(int& argc, char**& argv, const char* opt,
- std::vector<char*>& allocated)
-{
-
- Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl;
-
- AlwaysAssert(opt != NULL && *opt != '\0');
- AlwaysAssert(strlen(opt) <= getLength());
-
- ++argc;
- unsigned i = 1;
- while(argv[i] != NULL && argv[i][0] != '\0') {
- ++i;
- }
-
- if(argv[i] == NULL) {
- unsigned newSize = i + getIncrease();
- argv = (char**) realloc(argv, newSize * sizeof(char*));
- for(unsigned j = i; j < newSize-1; ++j) {
- char* newString = (char*) malloc(sizeof(char) * getLength());
- newString[0] = '\0';
- argv[j] = newString;
- allocated.push_back(newString);
- }
- argv[newSize - 1] = NULL;
- }
-
- strncpy(argv[i], opt, getLength() - 1);
- argv[i][getLength() - 1] = '\0'; // ensure NULL-termination even on overflow
-}
-
-}/* CVC4::options namespace */
-}/* CVC4 namespace */
/********************* */
-/*! \file preempt_get_option.h
+/*! \file argument_extender.h
** \verbatim
** Original author: Tim King
** Major contributors: none
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Utility function for extending commandline options.
+ ** \brief Abstract utility class for extending commandline options.
**
- ** Utility function for extending commandline options.
+ ** Abstract utility class for extending commandline options.
**/
-#include "cvc4_private.h"
+#include "cvc4_public.h"
-#ifndef __CVC4__OPTIONS__PREMPT_GET_OPTION_H
-#define __CVC4__OPTIONS__PREMPT_GET_OPTION_H
+#ifndef __CVC4__OPTIONS__ARGUMENT_EXTENDER_H
+#define __CVC4__OPTIONS__ARGUMENT_EXTENDER_H
#include <cstddef>
-#include <vector>
namespace CVC4 {
namespace options {
-
+/**
+ * Abstract utility class for implementing command line options
+ * parsing for the Options class. This allows for adding preemption
+ * arguments. A preemption is effectivly adding a new argument into
+ * the commandline arguments and must be processed immediately.
+ */
class ArgumentExtender {
- public:
+public:
+ ArgumentExtender(){}
+ virtual ~ArgumentExtender(){}
+
/**
+ * This creates a copy of the current arguments list as a new array.
+ * The new array is stored in argv. The user of this function is
+ * expected to own the memory of the string array, but not the
+ * strings themselves. The length of the new array is
+ * numArguments() and is stored in argc.
+ *
* Preconditions:
- * additional >= 1
- * length >= 1
+ * - argc and argv are non-null.
*/
- ArgumentExtender(unsigned additional, size_t length);
- ~ArgumentExtender();
+ virtual void getArguments(int* argc, char*** argv) const = 0;
+
+ /** Returns the number of arguments that are . */
+ virtual size_t numArguments() const = 0;
/**
- * This purpose of this function is to massage argc and argv upon the event
- * of parsing during Options::parseOptions of an option with the :link or
- * :link-alternative attributes. The purpose of the function is to extend argv
- * with another commandline argument.
- *
- * Preconditions:
- * opt is '\0' terminated, non-null and non-empty c-string.
- * strlen(opt) <= getLength()
- *
- * Let P be the first position in argv that is >= 1 and is either NULL or
- * empty:
- * argv[P] == NULL || argv[P] == '\0'
- *
- * This has a very specific set of side effects:
- * - argc is incremented by one.
- * - If argv[P] == NULL, this reallocates argv to have (P+additional)
- * elements.
- * - The 0 through P-1 elements of argv are the same.
- * - The P element of argv is a copy of the first len-1 characters of opt.
- * This is a newly allocated '\0' terminated c string of length len.
- * - The P+1 through (P+additional-2) elements of argv are newly allocated
- * empty '\0' terminated c strings of size len.
- * - The last element at (P+additional-1) of argv is NULL.
- * - All allocations are pushed back onto allocated.
+ * Inserts a copy of element into the front of the arguments list.
+ * Preconditions: element is non-null and 0 terminated.
+ */
+ virtual void pushFrontArgument(const char* element) = 0;
+
+ /**
+ * Inserts a copy of element into the back of the arguments list.
+ * Preconditions: element is non-null and 0 terminated.
+ */
+ virtual void pushBackArgument(const char* element) = 0;
+
+ /** Removes the front of the arguments list.*/
+ virtual void popFrontArgument() = 0;
+
+ /** Adds a new preemption to the arguments list. */
+ virtual void pushBackPreemption(const char* element) = 0;
+
+ /**
+ * Moves all of the preemptions into the front of the arguments
+ * list.
*/
- void extend(int& argc, char**& argv, const char* opt,
- std::vector<char*>& allocated);
+ virtual void movePreemptionsToArguments() = 0;
- unsigned getIncrease() const;
- size_t getLength() const;
+ /** Returns true iff there is a pending preemption.*/
+ virtual bool hasPreemptions() const = 0;
- private:
- unsigned d_additional;
- size_t d_length;
-};
+};/* class ArgumentExtender */
}/* CVC4::options namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__OPTIONS__PREMPT_GET_OPTION_H */
+#endif /* __CVC4__OPTIONS__ARGUMENT_EXTENDER_H */
--- /dev/null
+/********************* */
+/*! \file argument_extender_implementation.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Utility class for parsing commandline options.
+ **
+ ** Utility class for parsing commandline options.
+ **/
+
+#include "options/argument_extender_implementation.h"
+
+#include <cstdlib>
+#include <cstring>
+#include <list>
+
+#include "base/cvc4_assert.h"
+#include "base/output.h"
+#include "options/argument_extender.h"
+
+namespace CVC4 {
+namespace options {
+
+ArgumentExtenderImplementation::ArgumentExtenderImplementation()
+ : d_allocated()
+ , d_preemptions()
+ , d_arguments()
+{
+}
+
+ArgumentExtenderImplementation::~ArgumentExtenderImplementation(){
+ for(CharPointerList::iterator i = d_allocated.begin(),
+ iend = d_allocated.end(); i != iend; ++i) {
+ char* current = *i;
+ Debug("options") << "~ArgumentExtenderImplementation " << current
+ << std::endl;
+ free(current);
+ }
+ d_allocated.clear();
+}
+
+size_t ArgumentExtenderImplementation::numArguments() const {
+ return d_arguments.size();
+}
+
+char* ArgumentExtenderImplementation::allocateCopy(const char* element) {
+ Assert(element != NULL);
+
+ char* duplicate = strdup(element);
+ Assert(duplicate != NULL);
+ d_allocated.push_back(duplicate);
+ return duplicate;
+}
+
+bool ArgumentExtenderImplementation::hasPreemptions() const {
+ return !d_preemptions.empty();
+}
+
+void ArgumentExtenderImplementation::pushBackPreemption(const char* element) {
+ d_preemptions.push_back(allocateCopy(element));
+}
+
+void ArgumentExtenderImplementation::movePreemptionsToArguments() {
+ d_arguments.splice(d_arguments.begin(), d_preemptions);
+}
+
+void ArgumentExtenderImplementation::popFrontArgument() {
+ Assert(!d_arguments.empty());
+ Debug("options") << "ArgumentExtenderImplementation::popFrontArgument "
+ << d_arguments.front() << std::endl;
+ d_arguments.pop_front();
+}
+
+void ArgumentExtenderImplementation::pushFrontArgument(const char* element) {
+ d_arguments.push_front(allocateCopy(element));
+}
+
+void ArgumentExtenderImplementation::pushBackArgument(const char* element) {
+ d_arguments.push_back(allocateCopy(element));
+}
+
+void ArgumentExtenderImplementation::getArguments(int* argc, char*** argv)
+ const {
+ Assert(argc != NULL);
+ Assert(argv != NULL);
+
+ *argc = numArguments();
+ *argv = copyArguments();
+}
+
+char** ArgumentExtenderImplementation::copyArguments() const {
+ int size = numArguments();
+ Assert(size >= 0);
+
+ char** array = (char**) malloc( sizeof(char*) * size );
+ Assert(array != NULL);
+ int position = 0;
+ for(std::list< char* >::const_iterator i = d_arguments.begin(),
+ iend = d_arguments.end(); i != iend; ++i, ++position) {
+ char* at_position = *i;
+ array[position] = at_position;
+ }
+
+ return array;
+}
+
+}/* CVC4::options namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file argument_extender_implementation.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Utility class for extending commandline options.
+ **
+ ** Utility class for extending commandline options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H
+#define __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H
+
+#include <cstddef>
+#include <list>
+
+#include "options/argument_extender.h"
+
+namespace CVC4 {
+namespace options {
+
+/**
+ * Utility class for implementing command line options parsing for the
+ * Options class. This allows for adding preemption arguments.
+ * Preemptions are processed immediately after the current argument.
+ */
+class ArgumentExtenderImplementation : public ArgumentExtender {
+ public:
+ /** Constructs a new empty ArgumentExtender.*/
+ ArgumentExtenderImplementation();
+
+ /** Destroys an ArgumentExtender and frees its associated memory.*/
+ ~ArgumentExtenderImplementation();
+
+ /**
+ * This creates a copy of the current arguments list as a new array.
+ * The new array is stored in argv. The user of this function is
+ * expected to own the memory of the string array, but not the
+ * strings themselves. The length of the new array is
+ * numArguments() and is stored in argc.
+ *
+ * Preconditions:
+ * - argc and argv are non-null.
+ */
+ void getArguments(int* argc, char*** argv) const;
+
+ /** Returns the number of arguments that are . */
+ size_t numArguments() const;
+
+ /**
+ * Inserts a copy of element into the front of the arguments list.
+ * Preconditions: element is non-null and 0 terminated.
+ */
+ void pushFrontArgument(const char* element);
+
+ /**
+ * Inserts a copy of element into the back of the arguments list.
+ * Preconditions: element is non-null and 0 terminated.
+ */
+ void pushBackArgument(const char* element);
+
+ /** Removes the front of the arguments list.*/
+ void popFrontArgument();
+
+ /** Adds a new preemption to the arguments list. */
+ void pushBackPreemption(const char* element);
+
+ /**
+ * Moves all of the preemptions into the front of the arguments
+ * list.
+ */
+ void movePreemptionsToArguments();
+
+ /** Returns true iff there is a pending preemption.*/
+ bool hasPreemptions() const;
+
+private:
+
+ typedef std::list< char* > CharPointerList;
+
+ /** Creates of copy of the arugments list.*/
+ char** copyArguments() const;
+
+ /** Allocates a copy and stores a copy in d_allocated.*/
+ char* allocateCopy(const char* element);
+
+ /** Contains a copy of the allocated strings.*/
+ CharPointerList d_allocated;
+
+ /**
+ * A list of all of the preempted arguments. All of these pointers
+ * in this list should be contained in d_allocated.
+ */
+ CharPointerList d_preemptions;
+
+ /**
+ * A list of all of the arguments. All of these pointers in this
+ * list should be contained in d_allocated.
+ */
+ CharPointerList d_arguments;
+
+};/* class ArgumentExtenderImplementation */
+
+}/* CVC4::options namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H */
for link in $links; do
run_links="$run_links
#line $lineno \"$kf\"
- argumentExtender.extend(extra_argc, extra_argv, \"$link\", allocated);"
+ extender->pushBackPreemption(\"$link\");"
done
fi
if [ -n "$smt_links" ]; then
for link in $links_alternate; do
run_links_alternate="$run_links_alternate
#line $lineno \"$kf\"
- argumentExtender.extend(extra_argc, extra_argv, \"$link\", allocated);"
+ extender->pushBackPreemption(\"$link\");"
done
fi
if [ -n "$notifications" ]; then
if [ "$type" = bool ]; then
all_modules_option_handlers="${all_modules_option_handlers}${cases}
#line $lineno \"$kf\"
- assignBool(options::$internal, option, true);$run_links
+ options->assignBool(options::$internal, option, true);$run_links
break;
"
elif [ -n "$expect_arg" -a "$internal" != - ]; then
}"
all_modules_option_handlers="${all_modules_option_handlers}${cases}
#line $lineno \"$kf\"
- assign(options::$internal, option, optionarg);$run_links
+ options->assign(options::$internal, option, optionarg);$run_links
break;
"
elif [ -n "$expect_arg" ]; then
if [ "$type" = bool ]; then
all_modules_option_handlers="${all_modules_option_handlers}${cases_alternate}
#line $lineno \"$kf\"
- assignBool(options::$internal, option, false);$run_links_alternate
+ options->assignBool(options::$internal, option, false);$run_links_alternate
break;
"
else
fi
links="$links
#line $lineno \"$kf\"
- argumentExtender.extend(extra_argc, extra_argv, \"$linkopt\", allocated);"
+ extender->pushBackPreemption(\"$linkopt\");"
if [ "$linkarg" ]; then
# include also the arg
links="$links
#line $lineno \"$kf\"
- argumentExtender.extend(extra_argc, extra_argv, optionarg.c_str(), allocated);"
+ extender->pushBackPreemption(optionarg.c_str());"
fi
shift
done
#include "base/listener.h"
#include "base/modal_exception.h"
#include "base/tls.h"
+#include "options/argument_extender.h"
#include "options/language.h"
#include "options/printer_modes.h"
#include "options/option_exception.h"
static std::vector<std::string> suggestSmtOptions(const std::string& optionName) throw();
/**
- * Initialize the options based on the given command-line arguments.
- * The return value is what's left of the command line (that is, the
- * non-option arguments).
+ * Initialize the Options object options based on the given
+ * command-line arguments given in argc and argv. The return value
+ * is what's left of the command line (that is, the non-option
+ * arguments).
+ *
+ * This function uses getopt_long() and is not thread safe.
+ *
+ * Preconditions: options and argv must be non-null.
*/
- std::vector<std::string> parseOptions(int argc, char* argv[])
- throw(OptionException);
+ static std::vector<std::string> parseOptions(Options* options,
+ int argc, char* argv[])
+ throw(OptionException);
/**
* Get the setting for all options.
/** Sends a std::flush to getOut(). */
void flushOut();
+ private:
+
+ /**
+ * Internal procedure for implementing the parseOptions function.
+ * Initializes the options object based on the given command-line
+ * arguments. This uses an ArgumentExtender containing the
+ * command-line arguments. Nonoptions are stored into nonoptions.
+ *
+ * This is not thread safe.
+ *
+ * Preconditions: options, extender and nonoptions are non-null.
+ */
+ static void parseOptionsRecursive(Options* options,
+ options::ArgumentExtender* extender,
+ std::vector<std::string>* nonoptions)
+ throw(OptionException);
};/* class Options */
}/* CVC4 namespace */
#include "base/output.h"
#include "base/tls.h"
#include "options/argument_extender.h"
+#include "options/argument_extender_implementation.h"
#include "options/didyoumean.h"
#include "options/language.h"
#include "options/options_handler.h"
${include_all_option_headers}
-#line 63 "${template}"
+#line 64 "${template}"
#include "options/options_holder.h"
#include "cvc4autoconfig.h"
${option_handler_includes}
-#line 71 "${template}"
+#line 72 "${template}"
using namespace CVC4;
using namespace CVC4::options;
${all_custom_handlers}
-#line 393 "${template}"
+#line 394 "${template}"
#ifdef CVC4_DEBUG
# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
{
}
-#line 411 "${template}"
+#line 412 "${template}"
static const std::string mostCommonOptionsDescription = "\
Most commonly-used CVC4 options:${common_documentation}";
-#line 416 "${template}"
+#line 417 "${template}"
static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
\n\
Additional CVC4 options:${remaining_documentation}";
-#line 422 "${template}"
+#line 423 "${template}"
static const std::string optionsFootnote = "\n\
[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
cvc4 | presentation | pl CVC4 presentation language\n\
smt1 | smtlib1 SMT-LIB format 1.2\n\
smt | smtlib | smt2 |\n\
- smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\
+ smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\
smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\
tptp TPTP format (cnf and fof)\n\
sygus SyGuS format\n\
cvc3 CVC3 presentation language\n\
smt1 | smtlib1 SMT-LIB format 1.2\n\
smt | smtlib | smt2 |\n\
- smt2.0 | smtlib2.0 | smtlib2 SMT-LIB format 2.0\n\
+ smt2.0 | smtlib2.0 | smtlib2 SMT-LIB format 2.0\n\
smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\
tptp TPTP format\n\
z3str SMT-LIB 2.0 with Z3-str string constraints\n\
{ NULL, no_argument, NULL, '\0' }
};/* cmdlineOptions */
-#line 501 "${template}"
+#line 502 "${template}"
// static void preemptGetopt(int& argc, char**& argv, const char* opt) {
* The return value is what's left of the command line (that is, the
* non-option arguments).
*/
-std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) {
- options::OptionsGuard guard(&s_current, this);
+std::vector<std::string> Options::parseOptions(Options* options,
+ int argc, char* argv[])
+ throw(OptionException) {
- // Having this synonym simplifies the generation code in mkoptions.
- options::OptionsHandler* handler = d_handler;
+ Assert(options != NULL);
+ Assert(argv != NULL);
- const char *progName = main_argv[0];
+ options::OptionsGuard guard(&s_current, options);
- ArgumentExtender argumentExtender(s_preemptAdditional, s_maxoptlen);
- std::vector<char*> allocated;
+ const char *progName = argv[0];
- Debug("options") << "main_argv == " << main_argv << std::endl;
+ // To debug options parsing, you may prefer to simply uncomment this
+ // and recompile. Debug flags have not been parsed yet so these have
+ // not been set.
+ //DebugChannel.on("options");
- // Reset getopt(), in the case of multiple calls to parseOptions().
- // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
- optind = 0;
-#if HAVE_DECL_OPTRESET
- optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
-#endif /* HAVE_DECL_OPTRESET */
+ Debug("options") << "Options::parseOptions == " << options << std::endl;
+ Debug("options") << "argv == " << argv << std::endl;
- // find the base name of the program
+ // Find the base name of the program.
const char *x = strrchr(progName, '/');
if(x != NULL) {
progName = x + 1;
}
- d_holder->binary_name = std::string(progName);
+ options->d_holder->binary_name = std::string(progName);
+
+ ArgumentExtender* argumentExtender = new ArgumentExtenderImplementation();
+ for(int position = 1; position < argc; position++) {
+ argumentExtender->pushBackArgument(argv[position]);
+ }
+
+ std::vector<std::string> nonoptions;
+ parseOptionsRecursive(options, argumentExtender, &nonoptions);
+ if(Debug.isOn("options")){
+ for(std::vector<std::string>::const_iterator i = nonoptions.begin(),
+ iend = nonoptions.end(); i != iend; ++i){
+ Debug("options") << "nonoptions " << *i << std::endl;
+ }
+ }
+
+ delete argumentExtender;
+ return nonoptions;
+}
+
+void Options::parseOptionsRecursive(Options* options,
+ ArgumentExtender* extender,
+ std::vector<std::string>* nonoptions)
+ throw(OptionException) {
+
+ int argc;
+ char** argv;
+
+ extender->movePreemptionsToArguments();
+ extender->pushFrontArgument("");
+ extender->getArguments(&argc, &argv);
+
+ if(Debug.isOn("options")) {
+ Debug("options") << "starting a new parseOptionsRecursive with "
+ << argc << " arguments" << std::endl;
+ for( int i = 0; i < argc ; i++ ){
+ Assert(argv[i] != NULL);
+ Debug("options") << " argv[" << i << "] = " << argv[i] << std::endl;
+ }
+ }
- int extra_argc = 1;
- char **extra_argv = (char**) malloc(2 * sizeof(char*));
- extra_argv[0] = NULL;
- extra_argv[1] = NULL;
+ // Having this synonym simplifies the generation code in mkoptions.
+ options::OptionsHandler* handler = options->d_handler;
+ options::OptionsHolder* holder = options->d_holder;
- int extra_optind = 0, main_optind = 0;
+ // Reset getopt(), in the case of multiple calls to parseOptions().
+ // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
+ optind = 0;
+#if HAVE_DECL_OPTRESET
+ optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
+#endif /* HAVE_DECL_OPTRESET */
+
+
+ int main_optind = 0;
int old_optind;
- int *optind_ref = &main_optind;
- char** argv = main_argv;
- std::vector<std::string> nonOptions;
+ while(true) { // Repeat Forever
+
+ if(extender->hasPreemptions()){
+ // Stop this round of parsing. We now parse recursively
+ // to start on a new character array for argv.
+ parseOptionsRecursive(options, extender, nonoptions);
+ break;
+ }
- for(;;) {
- int c = -1;
optopt = 0;
std::string option, optionarg;
- Debug("preemptGetopt") << "top of loop, extra_optind == " << extra_optind
- << ", extra_argc == " << extra_argc << std::endl;
- if((extra_optind == 0 ? 1 : extra_optind) < extra_argc) {
-#if HAVE_DECL_OPTRESET
- if(optind_ref != &extra_optind) {
- optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
- }
-#endif /* HAVE_DECL_OPTRESET */
- old_optind = optind = extra_optind;
- optind_ref = &extra_optind;
- argv = extra_argv;
- Debug("preemptGetopt") << "in preempt code, next arg is "
- << extra_argv[optind == 0 ? 1 : optind]
- << std::endl;
- if(extra_argv[extra_optind == 0 ? 1 : extra_optind][0] != '-') {
- InternalError(
- "preempted args cannot give non-options command-line args (found `%s')",
- extra_argv[extra_optind == 0 ? 1 : extra_optind]);
- }
- c = getopt_long(extra_argc, extra_argv,
- "+:${all_modules_short_options}",
- cmdlineOptions, NULL);
- Debug("preemptGetopt") << "in preempt code"
- << ", c == " << c << " (`" << char(c) << "')"
- << " optind == " << optind << std::endl;
- if(optopt == 0 ||
- ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) {
- // long option
- option = argv[old_optind == 0 ? 1 : old_optind];
- optionarg = (optarg == NULL) ? "" : optarg;
- } else {
- // short option
- option = std::string("-") + char(optopt);
- optionarg = (optarg == NULL) ? "" : optarg;
- }
- if(optind >= extra_argc) {
- Debug("preemptGetopt") << "-- no more preempt args" << std::endl;
- unsigned i = 1;
- while(extra_argv[i] != NULL && extra_argv[i][0] != '\0') {
- extra_argv[i][0] = '\0';
- ++i;
- }
- extra_argc = 1;
- extra_optind = 0;
- } else {
- Debug("preemptGetopt") << "-- more preempt args" << std::endl;
- extra_optind = optind;
- }
+
+ optind = main_optind;
+ old_optind = main_optind;
+ //optind_ref = &main_optind;
+ //argv = main_argv;
+
+ // If we encounter an element that is not at zero and does not start
+ // with a "-", this is a non-option. We consume this element as a
+ // non-option.
+ if (main_optind > 0 && main_optind < argc &&
+ argv[main_optind][0] != '-') {
+ Debug("options") << "enqueueing " << argv[main_optind]
+ << " as a non-option." << std::endl;
+ nonoptions->push_back(argv[main_optind]);
+ ++main_optind;
+ extender->popFrontArgument();
+ continue;
}
- if(c == -1) {
-#if HAVE_DECL_OPTRESET
- if(optind_ref != &main_optind) {
- optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
- }
-#endif /* HAVE_DECL_OPTRESET */
- old_optind = optind = main_optind;
- optind_ref = &main_optind;
- argv = main_argv;
- if(main_optind < argc && main_argv[main_optind][0] != '-') {
- do {
- if(main_optind != 0) {
- nonOptions.push_back(main_argv[main_optind]);
- }
- ++main_optind;
- } while(main_optind < argc && main_argv[main_optind][0] != '-');
- continue;
- }
- Debug("options") << "[ before, optind == " << optind << " ]" << std::endl;
-#if defined(__MINGW32__) || defined(__MINGW64__)
- if(optreset == 1 && optind > 1) {
- // on mingw, optreset will reset the optind, so we have to
- // manually advance argc, argv
- main_argv[optind - 1] = main_argv[0];
- argv = main_argv += optind - 1;
- argc -= optind - 1;
- old_optind = optind = main_optind = 1;
- if(argc > 0) {
- Debug("options") << "looking at : " << argv[0] << std::endl;
- }
- /*c = getopt_long(argc, main_argv,
+
+
+ Debug("options") << "[ before, main_optind == " << main_optind << " ]"
+ << std::endl;
+ Debug("options") << "[ before, optind == " << optind << " ]" << std::endl;
+ Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]"
+ << std::endl;
+ int c = getopt_long(argc, argv,
"+:${all_modules_short_options}",
cmdlineOptions, NULL);
- Debug("options") << "pre-emptory c is " << c << " (" << char(c) << ")" << std::endl;
- Debug("options") << "optind was reset to " << optind << std::endl;
- optind = main_optind;
- Debug("options") << "I restored optind to " << optind << std::endl;*/
- }
-#endif /* __MINGW32__ || __MINGW64__ */
- Debug("options") << "[ argc == " << argc
- << ", main_argv == " << main_argv << " ]" << std::endl;
- c = getopt_long(argc, main_argv,
- "+:${all_modules_short_options}",
- cmdlineOptions, NULL);
- main_optind = optind;
- Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]"
- << std::endl;
- Debug("options") << "[ next option will be at pos: " << optind << " ]"
- << std::endl;
- if(c == -1) {
+
+ while(main_optind < optind) {
+ main_optind++;
+ extender->popFrontArgument();
+ }
+
+ Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]"
+ << "[ next option will be at pos: " << optind << " ]"
+ << std::endl;
+
+ // The initial getopt_long call should always determine that argv[0]
+ // is not an option and returns -1. We always manually advance beyond
+ // this element.
+ //
+ // We have to reinitialize optind to 0 instead of 1 as we need to support
+ // changing the argv array passed to getopt.
+ // This is needed as are using GNU extensions.
+ // From: http://man7.org/linux/man-pages/man3/getopt.3.html
+ // A program that scans multiple argument vectors, or rescans the same
+ // vector more than once, and wants to make use of GNU extensions such
+ // as '+' and '-' at the start of optstring, or changes the value of
+ // POSIXLY_CORRECT between scans, must reinitialize getopt() by
+ // resetting optind to 0, rather than the traditional value of 1.
+ // (Resetting to 0 forces the invocation of an internal initialization
+ // routine that rechecks POSIXLY_CORRECT and checks for GNU extensions
+ // in optstring.)
+ if ( old_optind == 0 && c == -1 ) {
+ Assert(main_optind > 0);
+ continue;
+ }
+
+ if ( c == -1 ) {
+ if(Debug.isOn("options")) {
Debug("options") << "done with option parsing" << std::endl;
- break;
+ for(int index = optind; index < argc; ++index) {
+ Debug("options") << "remaining " << argv[index] << std::endl;
+ }
}
- option = argv[old_optind == 0 ? 1 : old_optind];
- optionarg = (optarg == NULL) ? "" : optarg;
+ break;
}
+ option = argv[old_optind == 0 ? 1 : old_optind];
+ optionarg = (optarg == NULL) ? "" : optarg;
+
Debug("preemptGetopt") << "processing option " << c
<< " (`" << char(c) << "'), " << option << std::endl;
switch(c) {
${all_modules_option_handlers}
-#line 709 "${template}"
+#line 722 "${template}"
case ':':
// This can be a long or short option, and the way to get at the
// name of it is different.
- throw OptionException(std::string("option `") + option + "' missing its required argument");
+ throw OptionException(std::string("option `") + option +
+ "' missing its required argument");
case '?':
default:
- if( ( optopt == 0 || ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} ) ) &&
- !strncmp(argv[optind - 1], "--thread", 8) &&
- strlen(argv[optind - 1]) > 8 ) {
+ if( ( optopt == 0 ||
+ ( optopt >= ${long_option_value_begin} &&
+ optopt <= ${long_option_value_end} )
+ ) && !strncmp(argv[optind - 1], "--thread", 8) &&
+ strlen(argv[optind - 1]) > 8 )
+ {
if(! isdigit(argv[optind - 1][8])) {
throw OptionException(formatThreadOptionException(option));
}
- std::vector<std::string>& threadArgv = d_holder->threadArgv;
+ std::vector<std::string>& threadArgv = holder->threadArgv;
char *end;
long tnum = strtol(argv[optind - 1] + 8, &end, 10);
if(tnum < 0 || (*end != '\0' && *end != '=')) {
}
if(*end == '\0') { // e.g., we have --thread0 "foo"
if(argc <= optind) {
- throw OptionException(std::string("option `") + option
- + "' missing its required argument");
+ throw OptionException(std::string("option `") + option +
+ "' missing its required argument");
}
Debug("options") << "thread " << tnum << " gets option "
<< argv[optind] << std::endl;
- threadArgv[tnum] += argv[(*optind_ref)++];
+ threadArgv[tnum] += argv[main_optind];
+ main_optind++;
} else { // e.g., we have --thread0="foo"
if(end[1] == '\0') {
throw OptionException(std::string("option `") + option +
"' missing its required argument");
}
- Debug("options") << "thread " << tnum << " gets option " << (end + 1)
- << std::endl;
+ Debug("options") << "thread " << tnum << " gets option "
+ << (end + 1) << std::endl;
threadArgv[tnum] += end + 1;
}
- Debug("options") << "thread " << tnum << " now has " << threadArgv[tnum]
- << std::endl;
+ Debug("options") << "thread " << tnum << " now has "
+ << threadArgv[tnum] << std::endl;
break;
}
}
}
- Debug("options") << "returning " << nonOptions.size() << " non-option arguments." << std::endl;
-
- free(extra_argv);
- for(std::vector<char*>::iterator i = allocated.begin(), iend = allocated.end();
- i != iend; ++i)
- {
- char* current = *i;
- #warning "TODO: Unit tests fail if garbage collection is done here."
- //free(current);
- }
- allocated.clear();
+ Debug("options") << "got " << nonoptions->size()
+ << " non-option arguments." << std::endl;
- return nonOptions;
+ free(argv);
}
std::string Options::suggestCommandLineOptions(const std::string& optionName) throw() {
static const char* smtOptions[] = {
${all_modules_smt_options},
-#line 790 "${template}"
+#line 800 "${template}"
NULL
};/* smtOptions[] */
${all_modules_get_options}
-#line 813 "${template}"
+#line 762 "${template}"
return opts;
}
char *argv[2];
argv[0] = strdup("");
argv[1] = strdup("--output-language=ast");
- opts.parseOptions(2, argv);
+ Options::parseOptions(&opts, 2, argv);
free(argv[0]);
free(argv[1]);
char *argv[2];
argv[0] = strdup("");
argv[1] = strdup("--output-language=ast");
- opts.parseOptions(2, argv);
+ Options::parseOptions(&opts, 2, argv);
free(argv[0]);
free(argv[1]);
}
TS_ASSERT(not collection.empty());
- for(int i=0; i < listeners.size(); ++i){
+ for(unsigned i=0; i < listeners.size(); ++i){
ListenerCollection::Registration* at_i = listeners[i];
delete at_i;
}
projects / cvc5.git / commitdiff