Logo Search packages:      
Sourcecode: maria version File versions

int main ( int  argc,
char **  argv 
)

The main function

Parameters:
argc argument count
argv argument vector
Returns:
0 if successful; 1 on parse error

flag: has the computation been aborted?

Definition at line 646 of file maria.C.

References analyze(), NameList::append(), cleanup(), cmdhelp(), compress, connect_addr, define_sym(), deline(), dereset(), execute(), funcSize, hashSize, interrupted, jobs, lastclock, local, maxerrors, maxIndex, md5compact, model(), modular, modulepath, newString(), numTables, optstring, probabilistic, progname, resolve(), scriptcommand, scriptstring, Printer::setRadix(), Printer::setWidth(), sig(), thePrinter, thresold, translator, undef_sym(), unfold(), Dotty::useVisual(), verbose, and VERSION.

{
#ifndef unix
  lastclock = clock ();
#else // !unix
  struct tms current;
  lastclock = times (&current);
#endif // !unix
  setlocale (LC_ALL, "");
  signal (SIGINT, sig);
#ifdef unix
  signal (SIGCHLD, sig);
#endif // unix
  atexit (cleanup);
  progname = *argv;

  /** flag: has the computation been aborted? */
  extern bool exiting;

#if defined YYDEBUG && YYDEBUG
  {
    /** Debugging flag for the Bison-generated parser */
    extern int pndebug;
    char *debug = getenv ("DEBUG");
    if (debug) pndebug = atoi (debug);
  }
#endif // YYDEBUG

#ifndef __WIN32
  const size_t prognamelen = strlen (progname);
  visualizer = new char[prognamelen + 5];
  memcpy (visualizer, progname, prognamelen);
  memcpy (visualizer + prognamelen, "-vis", 5);
  Dotty::useVisual (visualizer);
#endif // __WIN32

  for (;;) {
    int c = getopt (argc, argv, optstring);
    if (c == EOF)
      break;
    switch (c) {
    case ':':
      // fall through
    default:
    case '?':
    case 'h':
      cmdhelp ();
      return 0;
    case 'v':
      verbose = true;
      break;
    case 'V':
      fprintf (stderr, "%s version " VERSION "\n", progname);
      return 0;
    case 'w':
      pnwarnings = false;
      break;
    case 'W':
      pnwarnings = true;
      break;
    case 'd':
      if (model (optarg, 0, true))
      analyze (0, false);
      break;
    case 'b':
      if (model (optarg, 0, true))
      analyze (0, true);
      break;
    case 'g':
      model (0, optarg, false);
      break;
    case 'm':
      model (optarg, 0, true);
      break;
    case 'M':
    case 'P':
    case 'L':
      model (optarg, 0, false);
      md5compact = c == 'M';
      probabilistic = c != 'L';
      break;
    case 'H':
      if (sscanf (optarg, "%u%n,%u%n,%u %n",
              &hashSize, &c, &funcSize, &c, &numTables, &c) < 1 ||
        optarg[c] ||
        !hashSize || !funcSize || !numTables) {
      fprintf (stderr, "error in hash parameters: `%s'\n", optarg);
      return 1;
      }
    case 'r':
      modular = false;
      subnet = net; delete[] modulepath; modulepath = 0;
      break;
    case 'R':
      modular = true;
      break;
    case 'y':
      local = false;
      break;
    case 'Y':
      local = true;
      break;
    case 'z':
      compress = false;
      break;
    case 'Z':
      compress = true;
      break;
#ifndef BUILTIN_LTL
    case 'p':
      delete[] translator;
      translator = newString (optarg);
      break;
#endif // !BUILTIN_LTL
    case 'a':
      {
      char* end = 0;
      maxIndex = strtoul (optarg, &end, 0);
      if (!*optarg || *end) {
        fprintf (stderr, "error in array size limit: `%s'\n", optarg);
        return 1;
      }
      }
      break;
    case 'q':
      {
      char* end = 0;
      maxRange = strtoul (optarg, &end, 0);
      if (!*optarg || *end) {
        fprintf (stderr, "error in quantification limit: `%s'\n", optarg);
        return 1;
      }
      }
      break;
    case 'i':
      {
      char* end = 0;
      unsigned width = strtoul (optarg, &end, 0);
      if (!*optarg || *end) {
        fprintf (stderr, "error in output width limit: `%s'\n", optarg);
        return 1;
      }
      else
        thePrinter.setWidth (width);
      }
      break;
    case 'x':
      {
      if (!strcmp (optarg, "oct") || !strcmp (optarg, "octal") ||
          !strcmp (optarg, "8"))
        thePrinter.setRadix (Printer::Octal);
      else if (!strcmp (optarg, "hex") || !strcmp (optarg, "hexadecimal") ||
             !strcmp (optarg, "16"))
        thePrinter.setRadix (Printer::Hexadecimal);
      else if (!strcmp (optarg, "dec") || !strcmp (optarg, "decimal") ||
             !strcmp (optarg, "10"))
        thePrinter.setRadix (Printer::Decimal);
      else
        fprintf (stderr, "ignoring unknown radix setting: `%s'\n", optarg);
      }
      break;
#if defined __WIN32 || defined WIN32
#else /* __WIN32 || WIN32 */
    case 'j':
      {
      char* end = 0;
      unsigned num = strtoul (optarg, &end, 0);
      if (!*optarg || *end) {
        fprintf (stderr, "error in number of jobs: `%s'\n", optarg);
        return 1;
      }
      else
        jobs = num;
      }
      break;
#endif /* __WIN32 || WIN32 */
    case 'k':
      if (!(connect_addr = resolve (optarg)))
      return 1;
      break;
    case 'I':
      includePath.append (newString (optarg));
      break;
    case 'u':
      unfold (optarg);
      break;
    case 'D':
      define_sym (optarg);
      break;
    case 'U':
      undef_sym (optarg);
      break;
    case 'e':
      if ((scriptstring = optarg) &&
        (interrupted || !execute (scriptcommand)))
      return 4;
      if (exiting)
      return 0;
      break;
    case 'E':
      {
      char* end = 0;
      thresold = strtoul (optarg, &end, 0);
      if (!*optarg || *end) {
        fprintf (stderr, "error in edge thresold: `%s'\n", optarg);
        return 1;
      }
      }
      break;
    case 't':
      {
      char* end = 0;
      maxerrors = strtoul (optarg, &end, 0);
      if (!*optarg || *end) {
        fprintf (stderr, "error in error tolerance: `%s'\n", optarg);
        return 1;
      }
      }
      break;
#ifdef HAS_REGEX
    case 'n':
      regexpExtract (optarg, regexpDisallow);
      break;
    case 'N':
      regexpExtract (optarg, regexpAllow);
      break;
#endif // HAS_REGEX
#ifdef EXPR_COMPILE
    case 'c':
      delete[] compiledir;
      compiledir = 0;
      break;
    case 'C':
      delete[] compiledir;
      compiledir = newString (optarg);
      break;
#endif // EXPR_COMPILE
    }
  }

  for (int i = optind; i < argc; i++)
    if (exiting)
      return 0;
    else if (interrupted || !execute (argv[i]))
      return 4;

  dereset ();
  while (!exiting && (scriptstring = deline ()))
    execute (scriptcommand);

  return 0;
}


Generated by  Doxygen 1.6.0   Back to index