    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava;
    004
    005    import java.util.Enumeration;
    006    import java.util.Hashtable;
    007    import java.util.Vector;
    008    import java.io.*;
    009
    010    import javafe.ast.*;
    011    import javafe.util.Set;
    012    import javafe.util.UsageError;
    013    import escjava.ast.*;
    014    import escjava.ast.TagConstants;
    015    import escjava.translate.NoWarn;
    016
    017    /**
    018     * This class parses the options on the command-line and is a structure for holding
    019     * the values of options.
    020     */
    021
    022    public class Options extends javafe.SrcToolOptions
    023    {
    024      final String[][] escPublicOptionData = {
    025        { "-CounterExample",
    026          "If a warning is discovered, generate a counter-example if possible." },
    027        { "-JavaAssertions, -eaJava",
    028          "Treat Java assert statements as normal Java asserts." },
    029        { "-JMLAssertions, -eaJML",
    030          "Treat Java assert statements like JML assert statements.  -eaJML and -eaJava are mutually exclusive switches.  -eaJML is the default setting." },
    031        { "-Loop <iteration_count>[.0|.5]",
    032          "Consider <iteration_count> iterations of all loops (i.e., unroll all loops <iteration_count> times; if <iteration_count>.5, evaluate loop guard one extra time." },
    033        { "-NoCheck",
    034          "Do all steps, including verification condition generation, but perform no checking with the prover." },
    035        { "-NoSemicolonWarnings",
    036          "Suppress warnings about semicolons missing at the end of annotations (to support old ESC/Java)." },
    037        { "-Simplify <path_to_executable>",
    038          "The path to the SIMPLIFY executable." },
    039        { "-Specs <path_to_specs_directory_or_jarfile>",
    040          "The jar file or directory path of the set of system specs to use; these are appended to the sourcepath, if specified, or else the classpath.  Multiple uses of -Specs are ignored; only final use of -Specs is recognized, as in javac." },
    041        { "-Typecheck",
    042          "Perform only parsing and typechecking; no generation of verification conditions or execution of prover takes place." },
    043        { "-LoopSafe",
    044          "Use an alternate form of loop unrolling for VC generation that is more rigorous but more expensive." },
    045        { "-NoRedundancy",
    046          "Do not check specs in redundant specification (e.g., requires_redundantly, etc.)." },
    047        { "-NoTrace",
    048          "Do not print the execution trace that leads to the potential error being warned about." },
    049        { "-NoWarn <category>",
    050          "Do not warn about the specified warning category.  The special category 'All' can be used to ignore all warnings.  The full list of warnings is found in the User's Manual." },
    051        { "-PlainWarning",
    052          "Suppress the output of the partial counterexample in the case of invariant warnings." },
    053        //$$
    054        { "-Prover",
    055          "Use provers listed after this option, for example : -Prover simplify harvey"},
    056        //$$
    057        { "-Routine [<routine_identifier> | <fully_quality_routine_signature>]",
    058          "Check\n\tonly the specified routine in all specified classes." },
    059        { "-RoutineIndirect <routine_file>",
    060          "The file <routine_file> should contain a list of all routines that are to be checked, similar to the -list\n\toption." },
    061        { "-Start <line_number>",
    062          "Start checking the first class specified at line number\n" +
    063          "\t<line_number>; all lines before <line_number> have warnings disabled." },
    064        { "-Stats",
    065          "Display a more detailed breakdown of some information. You can supply some keyword indicating what you want :  time space complexity termComplexity variableComplexity quantifierComplexity. Usage example : -Stats time,space,variableComplexity. Default behavior is -Stats time,space. The complexity parameter displays all *Complexity flags." },
    066        { "-Suggest",
    067          "After each warning, suggest an annotation that will suppress the\n\twarning." },
    068        { "-VCLimit <number>",
    069          "Set the maximum size of the VC to <number> bytes;\n\tdefaults to 500,000." },
    070        { "-Warn <category>",
    071          "Turns on all warnings of category <category> if they are currently turned off." }
    072      };
    073
    074      final String[][] escPrivateOptionData = {
    075        { "-ShowDesugardedSpecs, -sds",
    076          "Show the parsed specs after being desugared from heavyweight to lightweight specs" },
    077        { "-PrintGuardedCommands, -pgc",
    078          "Print the guarded commands" },
    079        { "-PrettyPrintVC, -ppvc",
    080          "Pretty-print verification conditions" },
    081        { "-pxLog <filename>",
    082          "Pretty-print the commands (S-expressions)sent to Simplify in the file named <filename>" },
    083        { "-sxLog <filename>",
    084          "Print the commands (S-expressions) sent to Simplify in the file named <filename>" },
    085        { "-Stages <number>",
    086          "Run at most <number> stages.  The current stages are (1) loading, parsing, and type checking; (2) generating the type-specific background predicate; (3) translating from Java to guarded commands; (4) optionally converting to dynamic-single-assignment form; (5) generating the verification condition (VC); (6) and calling the theorem prover to verify the VC." },
    087        { "-InlineFromConstructors",
    088          "When checking a constructor of a class 'T', inline every call 'this.m(...)' transitively from within the constructor, whenever 'm' statically resolves to a non-overridable instance method defined in 'T'." },
    089        { "-InlineCheckDepth <depth>",
    090          "When a method body is translated, at least <depth> levels of inlining of calls are performed.  The <depth> level of inlining is checked, while all previous levels are turned off.  By default, <depth> is zero.   This flag cannot be used with -inlineConstructors.  See also -inlineDepthPastCheck." },
    091        { "-InlineDepthPastCheck <depth>",
    092          "When a method body is translated, 'n' levels of inlining of calls are performed beyond the inlining level that is checked (see the -inlineCheckDepth option).  Checks at all 'n' levels are turned off.  By default 'n' is 0.  This flag cannot be used in combination with the -inlineConstructors flag." },
    093        { "-InlineConstructors",
    094          "For each non-static method 'm' and constructor 'c', generate and check a new method consisting of an inline call to 'c' followed immediately by 'm'.  This flag cannot be used in combination with -inlineCheckDepth or -inlineDepthPastCheck." },
    095        { "-PrintCounterExampleContext, -pcc",
    096          "Causes the full counterexample context to be displayed after each unsuccessful verification attempt." },
    097        { "-NoStrongestPostconditionVC, -nospvc",
    098          "Generate verification conditions using weakest preconditions, not strongest postconditions." },
    099        { "-Passify",
    100          "TBD" },
    101        { "-UseDefPred",
    102          "TBD" },
    103        { "-NoDynamicSingleAssignment, -nodsa",
    104          "Do not convert guarded command into dynamic single-assignment form before generating a VC.  This flag implies the -nospvc flag." },
    105        { "-PrintDynamicSingleAssignment, -pdsa",
    106          "For each method and constructor to be verified, the guarded-command translation of its body in dynamic single-assignment form is printed if available." },
    107        { "-PrintVC, -pvc",
    108          "Print the generated VC.  See also -ppvc." },
    109        { "-wpnxw <number>",
    110          "TBD" },
    111        { "-NamePCSize <number>",
    112          "TBD" },
    113        { "-CheckSpecs",
    114          "TBD" },
    115        { "-PrintJavaWithTypes, -pjt",
    116          "Prints out the Java source plus annotations, with a comment before each expression containing its Java static type." },
    117        { "-NoVariableUniquification, -nvu",
    118          "Print all name resolutions performed when using -pgc without location information." },
    119        { "-AssertContinue, -ac",
    120          "Experimental feature to try to make Houdini invocations refute more than one annotation in one pass." },
    121        { "-NoTrackReadChars",
    122          "Turns off recording of characters that come back from the prover, which makes unexpected Simplify output messages be less informative." },
    123        { "-FilterMethodSpecs",
    124          "Ignore routine preconditions, frame axioms, and postconditions that mention fields that are not spec-accessible." },
    125        { "-NoPeepOptGCAssertFalse",
    126          "Experimental patch for the benefit of Houdini.  Disengages the guarded command peephole optimization that removes what is sequentially composed after an 'assert false'." },
    127        { "-NoEPeepOpt",
    128          "Turns off peephold optimization for expressions." },
    129        { "-NoGCPeepOpt",
    130          "Turns off peephole optimizations for guarded commands." },
    131        { "-LazySubst",
    132          "Enable lazy substitutions.  Possibly uses less memory and more time." },
    133        { "-MergeInv",
    134          "Merge all invariants into a single predicate.  This improves checking speed at the cost of incorrect error report locations for invariant warnings." },
    135        { "-NoAllocUseOpt",
    136          "Causes the variable 'alloc' in the guarded-command encoding to be treated as possibly being modified by every routine call." },
    137        { "-UseAllInvPostCall",
    138          "Check all postconditions resulting from invariants even if there is no overlap between the free variables of the invariant and the modifies clause of the call." },
    139        { "-UseAllInvPostBody",
    140          "Check all postconditions resulting from invariants even if there is no overlap between the free variables of the invariant and the syntactic targets of the body being checked.  See also -UseAllInvPreBody." },
    141        { "-UseAllInvPreBody",
    142          "Check all preconditions resulting from invariants even if there is no overlap between the free variables of the invariant and the syntactic targets of the body being checked.  See also -UseAllInvPostBody." },
    143        { "-FilterInvariants",
    144          "Ignore invariants and axioms that mention variables that are not spec-accessible." },
    145        { "-PrintAssumers",
    146          "Prints the list of annotations that are in some way related to each routine.  This switch is provided for the benefit of Houdini." },
    147        { "-PrintCompilationUnitsOnLoad",
    148          "Prints the name of each file as it is loaded." },
    149        { "-GuardedVC <directory>",
    150          "Write all guarded verification conditions to the specified directory, one file per VC." },
    151        { "-IgnoreAnnFile <filename>",
    152          "TBD" },
    153        { "-Skip",
    154          "TBD" },
    155        { "-PreciseTargets",
    156          "; using this switch implies -loopSafe is enabled also" },
    157        { "-LoopFallThru",
    158          "Insert a break at the end of all loop unrolling, rather than the guarded command 'fail'.  (Probably undesirable.)" },
    159        { "-MapsUnrollCount <count>",
    160          "TBD" },
    161        { "-PredAbstract",
    162          "TBD" },
    163        { "-InferPredicates",
    164          "; using this switch implies -loopSafe is enabled also" },
    165        { "-NoDirectTargetsOpt",
    166          "Uses normal targets, instead of direct targets, when intersecting the free variables on invariants to see if the invariant needs to be considered." },
    167        { "-NestQuantifiers",
    168          "Causes all user-supplied quantifiers to be nested in the translation, with one bound variable per quantification." },
    169        { "-UseIntQuantAntecedents",
    170          "Generates type antecedent for user-supplied quantified variables of type 'int' and 'long' (rather than just 'true')." },
    171        { "-ExcuseNullInitializers, -eni",
    172          "Suppress the non-null check for explicit null initialization in constructors." },
    173        { "-StrongAssertPostNever",
    174          "Causes the strongest-postcondition based verification condition generation to never assume a condition after it has been asserted.  (Note, depending on Simplify's subsumption settings, a proved condition may still be assumed by Simplify.)  See also -StrongAssertPostAtomic and -StrongAssertPostAlways." },
    175        { "-StrongAssertPostAtomic",
    176          "Causes the strongest-postcondition based verification condition generation to, in essence, assume a condition after it has been asserted, provided the condition is 'simple', meaning a conjunction of atomic formulas.  This is the default behavior.  See also -StrongAssertPostNever and -StrongAssertPostAlways." },
    177        { "-StrongAssertPostAlways",
    178          "Causes the strongest-postcondition based verification condition generation to, in essence, always assume a condition after it has been asserted.  See also -StrongAssertPostAtomic and -StrongAssertPostNever." },
    179        { "-NoLastVarUseOpt",
    180          "Disables the dead variable analysis and optimization that are otherwise applied in the generation of the DSA form of guarded commands." },
    181        { "-NoVarCheckDeclsAndUses",
    182          "Dispense with the check that there are no multiply declared local variables, no free uses of variables outside their local-declaration blocks, and no duplicate dynamic-instance inflections, assumptions that DSA uses when making all local-declaration blocks implicit." },
    183        { "-Hidecall",
    184          "Omit the details of calls when printing guarded commands." },
    185        { "-ShowLoop",
    186          "Show all details of desugaring of loops when printing guarded commands." },
    187        { "-VerboseTrace",
    188          "Print additional trace information.  See also -notrace." },
    189        { "-BubbleNotDown, -bnd",
    190          "Bubble down all logical NOTs in specification formulas to literals whenever possible." },
    191        { "-BackPredFile <filename>, -bpf <filename>",
    192          "Specifies an alternate file that should be used as the universal background predicate." },
    193        { "-NoOutCalls",
    194          "By default, we allow calls out from routines even when one or more objects have their invariants broken so long as those objects are not passed as (implicit) parameters or via static fields (in scope) to the callee.  This switch outlaws even those calls unless the only object broken is the object being constructed by the caller (a constructor)." },
    195        { "-ParsePlus",
    196          "Parse pragmas that begin with /*+@ which are normally only parsed by the core JML tools." },
    197        { "-NoNotCheckedWarnings",
    198          "Do not print any warnings about constructs that are not checked." },
    199        { "-TestRef",
    200          "Pretty-print each compilation unit on the command-line; used primarily to test refinement synthesis." },
    201        { "-CheckPurity",
    202          "Enable checking of pure methods; currently disabled by default until issues with pure inheritance semantics are resolved." },
    203        { "-RewriteDepth <depth>",
    204          "Set the limit to the rewriting depth of non-functional method calls to <depth> calls." },
    205        { "-UseFcns",
    206          "TBD" },
    207        { "-UseVars",
    208          "TBD" },
    209        { "-UseFcnsForModelVars",
    210          "TBD" },
    211        { "-UseVarsForModelVars",
    212          "TBD" },
    213        { "-UseFcnsForMethods",
    214          "TBD" },
    215        { "-UseVarsForMethods",
    216          "TBD" },
    217        { "-ShowFields",
    218          "TBD" },
    219        { "-EscProjectFileV0",
    220          "TBD" },
    221        { "-NonNullElements, -nne",
    222          "Enable support for generating type-predicates for the \nonnullelements keyword.  Disabled by default." },
    223        //$$
    224        { "-PvsProof"
    225          ,
    226          "Writes the transcription of the proof into pvs format to '$ESCTOOLS/Escjava/' ."},
    227        { "-nvcg",
    228          "Use the new verification conditions generator"},
    229        { "-nvcgpi",
    230          "Print information about the vcg"},
    231        { "-pSimplify",
    232          "Write the proof for simplify generated by the new verification condition generator to a file."},
    233        { "-pPvs",
    234          "Write the proof for pvs generated by the new verification condition generator to a file."},
    235        { "-vc2dot",
    236          "Output the gc tree in dot format"},
    237        { "-ifpvc2dot",
    238          "Output the translation of the gc tree in dot format"}
    239        //$$
    240      };
    241
    242      // Global escjava flags
    243
    244      /*
    245       * These are set by the command-line switches of the same name.
    246       * They default to false (unset).
    247       */
    248
    249      public String simplify = System.getProperty("simplify");
    250
    251      //$$
    252      /*
    253       * Flags indicating which prover you want to use
    254       */
    255      public boolean useSimplify = true;
    256      // -> by default simplify is used when the option -Prover is not given.
    257      public boolean useSammy = false;
    258      public boolean useHarvey = false;
    259
    260      /* flag for writing pvs proof to a file located in $ESCTOOLS/Escjava/
    261       The name of the file is the identifier of the method being tested */
    262      public boolean pvsProof = false;
    263
    264      // use the new verification conditions generator
    265      public boolean nvcg = false;
    266      // print information about the vcg
    267      public boolean nvcgpi = false;
    268      // output vc generated by the new verification condition generator
    269      // to a file.
    270      public boolean pSimplify = false;
    271      public boolean pPvs = false;
    272      // output gc tree in dot format
    273      public boolean vc2dot = false;
    274      public boolean ifpvc2dot = false;
    275      //$$
    276
    277      public boolean suggest = false;
    278
    279      public boolean pjt     = false; // print java w/ types
    280      public boolean nvu     = false; // unknown functionality
    281      public boolean pgc     = false; // print the guarded commands
    282      public boolean pdsa    = false; // prints the single-assignment GCs
    283      public boolean pvc     = false; // pretty-print the verification conditions
    284      public boolean pcc     = false; // a pruned, pretty-printed version of pcc:
    285      public boolean counterexample = false;
    286      public boolean statsTime = false;
    287      public boolean statsSpace = false;
    288      public boolean statsTermComplexity = false;
    289      public boolean statsVariableComplexity = false;
    290      public boolean statsQuantifierComplexity = false;
    291
    292      public boolean plainWarning   = false;
    293
    294      public boolean useOldStringHandling = false; // Just for backwards compatibility for Esc/Java tests
    295
    296      /** JML allows only subtypes of Exception in signals clauses.  Thus signals
    297       clauses cannot be written about Errors.  Set this option to true to have
    298       annotations allow any Throwable.
    299       */
    300      public boolean useThrowable = false;
    301
    302      /** The dirpath or jar file of system specs to use. */
    303      public String specspath = null;
    304
    305      /** Statically check against redundant specs?  Default is true. */
    306      public boolean checkRedundantSpecs = true;
    307
    308      // trace info: (0) no, (1) default, (2) verbose
    309      public int traceInfo = 1;
    310      //@ invariant 0 <= traceInfo && traceInfo < 3;
    311
    312      /** When set, pretty-prints the VCs that are obtained with verbose output
    313       or in the log (-sxLog) */
    314      public boolean prettyPrintVC = false;
    315
    316      /** When set, prints out the desugared specs for debugging purposes. */
    317      public boolean desugaredSpecs = false;
    318
    319      /** When true, pretty prints each compilation unit on the command-line;
    320       this is only used for testing, to test the combining of refinements.
    321       */
    322      public boolean testRef = false;
    323
    324      /** Temporary option to turn on purity checking, since it is off by
    325       default until purity issues with inheritance are resolved.
    326       */
    327      public boolean checkPurity = false;
    328
    329      public boolean strictExceptions = false;
    330
    331      /** When true, parses pragmas that begin with /*+@, which are normally
    332       parsed only by JML; this allows test runs in which everything JML
    333       parses is parsed by escjava, to see if we have full coverage of all
    334       of JML.
    335       */
    336      public boolean parsePlus = false;
    337
    338      /** When true, does not print any warnings about things not checked. */
    339      public boolean noNotCheckedWarnings = false;
    340
    341      /** JML requires semicolons to terminate annotations.  ESC/Java2 will
    342       warn about such missing semicolons; these were not required in
    343       ESC/Java.  When the following option is true, such warnings are
    344       suppressed to support old ESC/Java annotations.
    345       **/
    346      public boolean noSemicolonWarnings = false;
    347
    348      //** The limit to the rewriting depth when handling non-functional method calls. */
    349      public int rewriteDepth = 2;
    350
    351      public boolean spvc = true;
    352      public boolean dsa = true;
    353      //@ invariant spvc ==> dsa;  // spvc requires dsa for soundness
    354      public boolean passify = false;
    355      public boolean wpp = false;
    356      public boolean useDefpred = false;
    357      public int wpnxw = 0;
    358      public int namePCsize = 0;
    359
    360      public boolean peepOptE=true;
    361      public boolean peepOptGC=true;
    362      public boolean lazySubst = false;
    363      public boolean mergeInv=false;
    364
    365      public static final int JAVA_ASSERTIONS = 0;
    366      public static final int JML_ASSERTIONS = 1;
    367      public int assertionMode = JAVA_ASSERTIONS;
    368
    369      public boolean useAllInvPostCall = false;
    370      public boolean useAllInvPostBody = false;
    371      public boolean useAllInvPreBody = false;
    372      public boolean allocUseOpt = true;
    373
    374      public static final int LOOP_FAST = 0;
    375      public static final int LOOP_SAFE = 1;
    376      public static final int LOOP_FALL_THRU = 2;
    377      public int loopTranslation = LOOP_FAST;
    378      //@ invariant LOOP_FAST <= loopTranslation && loopTranslation <= LOOP_FALL_THRU;
    379
    380      // The default loop unrolling is: -loop 1.5
    381      public int loopUnrollCount = 1;
    382      public boolean loopUnrollHalf = true;
    383
    384      public int mapsUnrollCount = 2;
    385
    386      public boolean preciseTargets = false;
    387
    388      public boolean predAbstract = false;
    389      public boolean inferPredicates = false;
    390
    391      public boolean noDirectTargetsOpt = false;
    392      public boolean nestQuantifiers = false;
    393
    394      public boolean lastVarUseOpt = true;
    395      public boolean noVarCheckDeclsAndUses = false;
    396
    397      public boolean useIntQuantAntecedents = false;
    398
    399      public boolean excuseNullInitializers = false;
    400
    401      /** The following values are used: <br>
    402       *   0-never, 1-atomic (default), 2-always
    403       */
    404      public int strongAssertPost = 1;
    405
    406      public boolean showCallDetails = true;
    407      public boolean showLoopDetails = false;
    408      public boolean bubbleNotDown=false;
    409      public int startLine = -1;    // starting line # for processing
    410      public int vclimit = 500000;
    411
    412      public boolean checkSpecs = false;
    413      public boolean noOutCalls = false;
    414
    415      // flags primarily used by Houdini
    416      public boolean printAssumers = false;
    417      public boolean noPeepOptGCAssertFalse = false;
    418      public boolean assertContinue = false;
    419      public boolean trackReadChars = true;
    420      public boolean guardedVC = false;
    421      public String guardedVCDir;
    422      public String guardedVCFileNumbers = "files.txt";
    423      public String guardedVCGuardFile = "guards.txt";
    424      public String guardedVCPrefix = "G_";
    425      public String guardedVCFileExt = "sx";
    426      public Set guardVars = new Set();
    427      public String ClassVCPrefix = "*Class*";
    428      public String MethodVCPrefix = "*Method*";
    429
    430      public Set ignoreAnnSet = null;
    431
    432      public boolean printCompilationUnitsOnLoad = false;
    433
    434      // Flags to control the treatment of model variables and routines calls
    435      public boolean useFcnsForModelVars = true;
    436      public boolean useFcnsForMethods = true;
    437      public boolean useFcnsForAllocations = true;
    438
    439      // filter invariants and axioms
    440      public boolean filterInvariants = false;
    441
    442      // filter method specifications
    443      public boolean filterMethodSpecs = false;
    444
    445      public Set routinesToCheck = null;  // null means "check everything"
    446      public Set routinesToSkip = null;  // null means "skip nothing"
    447
    448      // do the inlined constructor experiment?
    449      public boolean inlineConstructors = false;
    450
    451      // do some other inlining experiment, using at least one of the two
    452      // inline depth flags?
    453      public boolean inlineDepthFlags = false;
    454
    455      // when checking a constructor of a class T, inline every call
    456      // this.m(...) transitively from within the constructor, whenever m
    457      // statically resolves to a non-overridable instance method defined in T.
    458      public boolean inlineFromConstructors = false;
    459
    460      public String sxLog = null;
    461
    462      // The following switch hardcodes whether or not also_requires is to
    463      // be part of the annotation language
    464      public boolean allowAlsoRequires = true;
    465
    466      // Debug flag that dumps the fields of each class
    467      public boolean showFields = false;
    468
    469      /**
    470       * Number of stages to run.  The stages currently in order are:
    471       * <pre>
    472       *     1. loading, parsing, and type checking
    473       *     2. generating the type-specific background predicate
    474       *        3. translating from Java to GC
    475       *        4. translating from GC to DSA
    476       *     5. generating the VC from the GC
    477       *     6. calling the theorem prover to verify the VC
    478       * </pre>
    479       *
    480       * <p> Defaults to running all stages (6); must be positive.
    481       *
    482       * <p> -nocheck sets <code>stages</code> to run all but the last
    483       * stage (5).  The -stages option can be used to set
    484       * <code>stages</code> to a particular value.
    485       */
    486      public int stages = 6;
    487
    488      //* Which file to obtain the universal background predicate from.
    489      public String univBackPredFile = null;
    490
    491      /**
    492       * Enable support for generating type-predicates for the
    493       * \nonnullelements keyword.  Disabled by default.
    494       */
    495      public boolean nne = false;
    496
    497
    498      // Generating an options message
    499
    500      /**
    501       * Generate all command-line option information.
    502       *
    503       * @param all if true show all non-public (experimental) switches as well.
    504       * @return a String containing all command-line option information.
    505       */
    506      public String showOptions(boolean all) {
    507        String s = super.showOptions(all);
    508        // All public options.
    509        s += showOptionArray(escPublicOptionData);
    510        // All private options only if requested.
    511        if (all)
    512          s += showOptionArray(escPrivateOptionData);
    513        return s;
    514      }
    515
    516      /**
    517       * @return non-option usage information in a string.
    518       */
    519      public String showNonOptions() {
    520        return super.showNonOptions();
    521      }
    522
    523
    524      // Option processing
    525
    526      /**
    527       * Process next tool option.
    528       *
    529       * <p> See {@link javafe.Options#processOptions(String [])} for the complete
    530       * specification of this routine.
    531       */
    532      public int processOption(String option, String[] args, int offset)
    533          throws UsageError {
    534        // First, change option to lowercase for case-less comparison.
    535        option = option.toLowerCase();
    536
    537        if (option.equals("-nocheck")) {
    538          stages = 5; // run all but last stage
    539          return offset;
    540        } else if (option.equals("-typecheck")) {
    541          stages = 1;
    542          return offset;
    543        } else if (option.equals("-stages")) {
    544          if (offset == args.length) {
    545            throw new UsageError("Option " + option +
    546                                 " requires one integer argument");
    547          }
    548          try {
    549            stages = new Integer(args[offset]).intValue();
    550            if (stages<1)
    551              throw new NumberFormatException();
    552          } catch (NumberFormatException e) {
    553            throw new UsageError("Option " + option +
    554                                 " requires one positive integer argument: " +
    555                                 e.toString());
    556          }
    557          return offset+1;
    558        } else if (option.equals("-start")) {
    559          if (offset>=args.length) {
    560            throw new UsageError("Option " + option +
    561                                 " requires one integer argument");
    562          }
    563          try {
    564            startLine = new Integer(args[offset]).intValue();
    565          } catch (NumberFormatException e) {
    566            throw new UsageError("Option " + option +
    567                                 " requires one positive integer argument: " +
    568                                 e.toString());
    569          }
    570          return offset+1;
    571        } else if (option.equals("-specs")) {
    572          if (offset >= args.length) {
    573            throw new UsageError("Option " + option +
    574                                 " requires one String argument");
    575          }
    576          specspath = args[offset];
    577          return offset+1;
    578        } else if (option.equals("-vclimit")) {
    579          if (offset>=args.length) {
    580            throw new UsageError("Option " + option +
    581                                 " requires one integer argument");
    582          }
    583          try {
    584            vclimit = new Integer(args[offset]).intValue();
    585          } catch (NumberFormatException e) {
    586            throw new UsageError("Option " + option +
    587                                 " requires one positive integer argument: " +
    588                                 e.toString());
    589          }
    590          return offset+1;
    591        } else if (option.equals("-inlinefromconstructors")) {
    592          inlineFromConstructors = true;
    593          return offset;
    594        } else if (option.equals("-inlinecheckdepth")) {
    595          inlineDepthFlags = true;
    596          // can't use this along with the -inlineConstructors flag
    597          if (inlineConstructors)
    598            throw new UsageError("Can't use -inlineConstructors in combination with either -inlineCheckDepth or -inlineDepthPastCheck");
    599          if (offset == args.length) {
    600            throw new UsageError("Option " + option +
    601                                 " requires one integer argument");
    602          }
    603          try {
    604            Main.gctranslator.inlineCheckDepth =
    605              new Integer(args[offset]).intValue();
    606            if (Main.gctranslator.inlineCheckDepth < 0)
    607              throw new NumberFormatException();
    608          } catch (NumberFormatException e) {
    609            throw new UsageError("Option " + option +
    610                                 " requires one positive integer argument: " +
    611                                 e.toString());
    612          }
    613          return offset+1;
    614        } else if (option.equals("-inlinedepthpastcheck")) {
    615          inlineDepthFlags = true;
    616          // can't use this along with the -inlineConstructors flag
    617          if (inlineConstructors)
    618            throw new UsageError("can't use -inlineConstructors in combination with either -inlineCheckDepth or -inlineDepthPastCheck");
    619          if (offset == args.length) {
    620            throw new UsageError("Option " + option +
    621                                 " requires one integer argument");
    622          }
    623          try {
    624            Main.gctranslator.inlineDepthPastCheck =
    625              new Integer(args[offset]).intValue();
    626            if (Main.gctranslator.inlineDepthPastCheck < 0)
    627              throw new NumberFormatException();
    628          } catch (NumberFormatException e) {
    629            throw new UsageError("Option " + option +
    630                                 " requires one positive integer argument: " +
    631                                 e.toString());
    632          }
    633          return offset+1;
    634        } else if (option.equals("-inlineconstructors")) {
    635          // can't use this along with either of the inline depth flags
    636          if (inlineDepthFlags)
    637            throw new UsageError("can't use -inlineConstructors in combination with either -inlineCheckDepth or -inlineDepthPastCheck");
    638          inlineConstructors = true;
    639          return offset;
    640        } else if (option.equals("-suggest")) {
    641          suggest = true;
    642          return offset;
    643        } else if (option.equals("-pgc") ||
    644                   option.equals("-printguardedcommands")) {
    645          pgc = true;
    646          return offset;
    647        } else if (option.equals("-printcounterexamplecontext") ||
    648                   option.equals("-pcc")) {
    649          pcc = true;
    650          return offset;
    651        } else if (option.equals("-noStrongestPostconditionVC") ||
    652                   option.equals("-nospvc")) {
    653          spvc = false;
    654          return offset;
    655        } else if (option.equals("-passify")) {
    656          passify = true;
    657          return offset;
    658        } else if (option.equals("-wpp")) {
    659          wpp = true;
    660          return offset;
    661        } else if (option.equals("-usedefpred")) {
    662          useDefpred = true;
    663          return offset;
    664        } else if (option.equals("-noDynamicSingleAssignment") ||
    665                   option.equals("-nodsa")) {
    666          dsa = false;
    667          spvc = false;  // spvc requires dsa for soundness
    668          return offset;
    669        } else if (option.equals("-printDynamicSingleAssignment") ||
    670                   option.equals("-pdsa")) {
    671          pdsa = true;
    672          return offset;
    673        } else if (option.equals("-printVC") ||
    674                   option.equals("-pvc")) {
    675          pvc = true;
    676          prettyPrintVC = true;
    677          return offset;
    678        }
    679        //$$
    680        /*
    681         * Surely it's possible to reuse some pre existing feature of Javafe
    682         * to do that, but it's simple, works and did not interfer with the
    683         * rest of the code, so that's nice for me atm . There will be time
    684         * to FIXME...
    685         * Clement
    686         * Update : we can do it in the same way that Stats, it changes the syntax from
    687         * '-Prover sammy simplify' to '-Prover sammy,simplify' but the code would be shorter
    688         */
    689        else if (option.equals("-prover")) {
    690          useSimplify = false; // override default settings
    691
    692          int newOffset = offset;
    693
    694          if ((offset >= args.length) || (args[offset].charAt(0) == '-')) {
    695            throw new UsageError(
    696                                 "Option "
    697                                 + option
    698                                 + " requires one argument or more indicating which prover you want to use.\n"
    699                                 + "(e.g., \"-Prover simplify sammy\")");
    700          }
    701
    702          // all strings are converted to lower case
    703          // thus no need for huge test
    704          String optionChecked;
    705
    706          if( offset + 1 <= args.length ) { // at least one more command after
    707
    708            optionChecked = new String(args[offset]).toLowerCase();
    709
    710            if( optionChecked.equals("simplify") )
    711              useSimplify = true;
    712            if( optionChecked.equals("sammy") )
    713              useSammy = true;
    714            if( optionChecked.equals("harvey") )
    715              useHarvey = true;
    716
    717            newOffset++;
    718          }
    719
    720          if( offset + 2 <= args.length ) { // at least two more commands after
    721
    722            optionChecked = new String(args[newOffset]).toLowerCase();
    723
    724            if( optionChecked.equals("simplify") )
    725              useSimplify = true;
    726            if( optionChecked.equals("sammy") )
    727              useSammy = true;
    728            if( optionChecked.equals("harvey") )
    729              useHarvey = true;
    730
    731            newOffset++;
    732          }
    733
    734          if( offset + 3 <= args.length ) { // at least three more commands after
    735
    736            optionChecked = new String(args[newOffset]).toLowerCase();
    737
    738            if( optionChecked.equals("simplify") )
    739              useSimplify = true;
    740            if( optionChecked.equals("sammy") )
    741              useSammy = true;
    742            if( optionChecked.equals("harvey") )
    743              useHarvey = true;
    744
    745            newOffset++;
    746          }
    747
    748          newOffset--;
    749
    750          return newOffset;
    751
    752        }
    753        else if (option.equals("-pvsproof")) {
    754          pvsProof = true;
    755
    756          return offset;
    757        }
    758        else if (option.equals("-nvcg")){
    759          nvcg = true;
    760
    761          return offset;
    762        }
    763        else if (option.equals("-nvcgpi")){
    764          nvcgpi = true;
    765
    766          return offset;
    767        }
    768        else if (option.equals("-psimplify")){
    769          pSimplify = true;
    770
    771          return offset;
    772        }
    773        else if (option.equals("-ppvs")){
    774          pPvs = true;
    775
    776          return offset;
    777        }
    778        else if (option.equals("-vc2dot")){
    779          vc2dot = true;
    780
    781          return offset;
    782        }
    783        else if (option.equals("-ifpvc2dot")){
    784          ifpvc2dot = true;
    785
    786          return offset;
    787        }
    788        //$$
    789        else if (option.equals("-wpnxw")) {
    790          if (offset >= args.length) {
    791            throw new UsageError("Option " + option +
    792                                 " requires one integer argument");
    793          }
    794          wpnxw = new Integer(args[offset]).intValue();
    795          return offset+1;
    796
    797        } else if (option.equals("-namepcsize")) {
    798          if (offset >= args.length) {
    799            throw new UsageError("Option " + option +
    800                                 " requires one integer argument");
    801          }
    802          namePCsize = new Integer(args[offset]).intValue();
    803          return offset+1;
    804        } else if (option.equals("-stats")) {
    805
    806          /* no more parameter or last parameter
    807           * , default behavior is to consider
    808           * keyword 'time' & 'space' as activated.
    809           */
    810          if ((offset >= args.length) || (args[offset].charAt(0) == '-')){
    811            statsTime = true;
    812            statsSpace = true;
    813
    814            return offset;
    815          }
    816          else { /* parse the string after the stats keyword
    817                    which shouldn't contain any space
    818                    the usual way to handle it is to store the string in a field
    819                    (look at guardedVCDir for example)
    820                    and use it in the main, but this way is nicer I think. [Clément]
    821            */
    822              if(args[offset].charAt(args[offset].length()-1) ==',')
    823                  throw new UsageError("Argument to option '"+ option +"' is finished by ',' which is not correct.");
    824
    825              String[] s = args[offset].split(",");
    826              String sTemp = null;
    827              int i = 0;
    828
    829              for ( ; i < s.length; i++){
    830
    831                  sTemp = s[i];
    832
    833                  //@ assert sTemp.length() != 0;
    834
    835                  if(sTemp.equals("time"))
    836                      statsTime = true;
    837                  else if(sTemp.equals("space"))
    838                      statsSpace = true;
    839                  else if(sTemp.equals("complexity")) {
    840                      // default behavior for complexity implemented here
    841                      statsTermComplexity = true;
    842                      statsVariableComplexity = true;
    843                      statsQuantifierComplexity = true;
    844                  }
    845                  else if(sTemp.equals("termComplexity"))
    846                      statsTermComplexity = true;
    847                  else if(sTemp.equals("variableComplexity"))
    848                      statsVariableComplexity = true;
    849                  else if(sTemp.equals("quantifierComplexity"))
    850                      statsQuantifierComplexity = true;
    851                  else
    852                      throw new UsageError("Argument to the option '" + option +"' not recognized : '"+s+"', skipping it");
    853
    854              }
    855
    856              return offset + 1;
    857
    858          } // </else>
    859
    860        } else if (option.equals("-checkspecs")) {
    861          checkSpecs = true;
    862          return offset;
    863        } else if (option.equals("-printjavawithtypes") ||
    864                   option.equals("-pjt")) {
    865          pjt = true;
    866          return offset;
    867        } else if (option.equals("-novariableuniquification") ||
    868                   option.equals("-nvu")) {
    869          nvu = true;
    870          return offset;
    871        } else if (option.equals("-ac") ||
    872                   option.equals("-assertcontinue")) {
    873          assertContinue = true;
    874          return offset;
    875        } else if (option.equals("-notrackreadchars")) {
    876          trackReadChars = false;
    877          return offset;
    878        } else if (option.equals("-filtermethodspecs")) {
    879          filterMethodSpecs = true;
    880          return offset;
    881        } else if (option.equals("-nopeepoptgcassertfalse")) {
    882          noPeepOptGCAssertFalse = true;
    883          return offset;
    884        } else if (option.equals("-noepeepopt")) {
    885          peepOptE = false;
    886          return offset;
    887        } else if (option.equals("-nogcpeepopt")) {
    888          peepOptGC = false;
    889          return offset;
    890        } else if (option.equals("-lazysubst")) {
    891          lazySubst = true;
    892          return offset;
    893        } else if (option.equals("-mergeinv")) {
    894          mergeInv = true;
    895          return offset;
    896        } else if (option.equals("-noallocuseopt")) {
    897          allocUseOpt = false;
    898          return offset;
    899        } else if (option.equals("-useallinvpostcall")) {
    900          useAllInvPostCall = true;
    901          return offset;
    902        } else if (option.equals("-useallinvpostbody")) {
    903          useAllInvPostBody = true;
    904          return offset;
    905        } else if (option.equals("-useallinvprebody")) {
    906          useAllInvPreBody = true;
    907          return offset;
    908        } else if (option.equals("-filterinvariants")) {
    909          filterInvariants = true;
    910          return offset;
    911        } else if (option.equals("-printassumers")) {
    912          printAssumers = true;
    913          return offset;
    914        } else if (option.equals("-printcompilationunitsonload")) {
    915          printCompilationUnitsOnLoad = true;
    916          return offset;
    917        } else if (option.equals("-guardedvc")) {
    918          if (offset >= args.length) {
    919            throw new UsageError("Option " + option +
    920                                 " requires one directory argument");
    921          }
    922          guardedVC = true;
    923          guardedVCDir = args[offset];
    924          return offset+1;
    925        } else if (option.equals("-ignoreannfile")) {
    926          if (offset >= args.length) {
    927            throw new UsageError("Option " + option +
    928                                 " requires one filename argument");
    929          }
    930          ignoreAnnSet = new Set(readFile(args[offset]).elements());
    931          // System.out.println("Ignore set: "+ignoreAnnSet+"\n");
    932          return offset+1;
    933        } else if (option.equals("-routine")) {
    934          // the argument to "-routine" is either a simple routine name or a fully
    935          // qualified routine name with signature, but we won't ever parse these
    936          if (offset == args.length) {
    937            throw new UsageError("Option " + option +
    938                                 " requires one argument");
    939          }
    940          String routine = args[offset].intern();
    941          if (routinesToCheck == null) {
    942            routinesToCheck = new Set();
    943          }
    944          routinesToCheck.add(routine);
    945          return offset+1;
    946        } else if (option.equals("-skip")) {
    947          // the argument to "-skip" is either a simple routine name or a fully
    948          // qualified routine name with signature, but we won't ever parse these
    949          if (offset == args.length) {
    950            throw new UsageError("Option " + option +
    951                                 " requires one argument");
    952          }
    953          String routine = args[offset].intern();
    954          if (routinesToSkip == null) {
    955            routinesToSkip = new Set();
    956          }
    957          routinesToSkip.add(routine);
    958          return offset+1;
    959        } else if (option.equals("-routineindirect")) {
    960          if (offset == args.length) {
    961            throw new UsageError("Option " + option +
    962                                 " requires one argument");
    963          }
    964          if (routinesToCheck == null) {
    965            routinesToCheck = new Set();
    966          }
    967          String routineIndirectionFilename = args[offset];
    968          BufferedReader in = null;
    969          try {
    970            in = new BufferedReader(
    971                                    new FileReader(routineIndirectionFilename));
    972            while (true) {
    973              String routine = in.readLine();
    974              if (routine == null) {
    975                break;
    976              }
    977              routine = routine.intern();
    978              routinesToCheck.add(routine);
    979            }
    980          } catch (IOException e) {
    981            throw new UsageError("error reading routine indirection file '" +
    982                                 routineIndirectionFilename + "': " +
    983                                 e.toString());
    984          } finally {
    985            try {
    986              if (in != null) in.close();
    987            } catch (IOException e) {
    988              throw new UsageError(
    989                                   "error closing routine indirection file '" +
    990                                   routineIndirectionFilename + "': " +
    991                                   e.toString());
    992            }
    993          }
    994          return offset+1;
    995        } else if (option.equals("-loopsafe")) {
    996          loopTranslation = LOOP_SAFE;
    997          return offset;
    998        } else if (option.equals("-precisetargets")) {
    999          preciseTargets = true;
    1000          loopTranslation = LOOP_SAFE;
    1001          return offset;
    1002        } else if (option.equals("-loop")) {
    1003          // syntax:  -loop <N>[.0|.5]
    1004          if (offset == args.length) {
    1005            throw new UsageError("Option " + option +
    1006                                 " requires one argument");
    1007          }
    1008          String number = args[offset];
    1009          if (number.length() == 0 || option.charAt(0) == '.') {
    1010            throw new UsageError("illegal argument to -loop: " + number);
    1011          }
    1012          // any other parsing error will be caught in the following loop
    1013          int cnt = 0;
    1014          boolean andAHalf = false;
    1015          for (int i = 0; i < number.length(); i++) {
    1016            char ch = number.charAt(i);
    1017            if ('0' <= ch && ch <= '9') {
    1018              if (10000 <= cnt) {
    1019                throw new UsageError("-loop specifies too many iterations: " +
    1020                                     number);
    1021              }
    1022              cnt = 10*cnt + ch - '0';
    1023              continue;
    1024            } else if (ch == '.') {
    1025              if (number.length() == i+2) {
    1026                if (number.charAt(i+1) == '5') {
    1027                  andAHalf = true;
    1028                  break;
    1029                } else if (number.charAt(i+1) == '0') {
    1030                  andAHalf = false;
    1031                  break;
    1032                }
    1033              }
    1034            }
    1035            throw new UsageError("illegal argument to -loop: " + number);
    1036          }
    1037          loopUnrollCount = cnt;
    1038          loopUnrollHalf = andAHalf;
    1039          return offset+1;
    1040        } else if (option.equals("-loopfallthru")) {
    1041          loopTranslation = LOOP_FALL_THRU;
    1042          return offset;
    1043        } else if (option.equals("-mapsunrollcount")) {
    1044          if (offset == args.length) {
    1045            throw new UsageError("Option " + option +
    1046                                 " requires one argument");
    1047          }
    1048          mapsUnrollCount = Integer.parseInt(args[offset]);
    1049          return offset+1;
    1050        } else if (option.equals("-predabstract")) {
    1051          predAbstract = true;
    1052          loopTranslation = LOOP_SAFE;
    1053          lastVarUseOpt = false;
    1054          return offset;
    1055        } else if (option.equals("-inferpredicates")) {
    1056          inferPredicates = true;
    1057          predAbstract = true;
    1058          loopTranslation = LOOP_SAFE;
    1059          lastVarUseOpt = false;
    1060          return offset;
    1061        } else if (option.equals("-nodirecttargetsopt")) {
    1062          noDirectTargetsOpt = true;
    1063          return offset;
    1064        } else if (option.equals("-nestquantifiers")) {
    1065          nestQuantifiers = true;
    1066          return offset;
    1067        } else if (option.equals("-useintquantantecedents")) {
    1068          useIntQuantAntecedents = true;
    1069          return offset;
    1070        } else if (option.equals("-excusenullinitializers") ||
    1071                   option.equals("-eni")) {
    1072          excuseNullInitializers = true;
    1073          return offset;
    1074        } else if (option.equals("-strongassertpostnever")) {
    1075          strongAssertPost = 0;
    1076          return offset;
    1077        } else if (option.equals("-strongassertpostatomic")) {
    1078          strongAssertPost = 1;
    1079          return offset;
    1080        } else if (option.equals("-strongassertpostalways")) {
    1081          strongAssertPost = 2;
    1082          return offset;
    1083        } else if (option.equals("-nolastvaruseopt")) {
    1084          lastVarUseOpt = false;
    1085          return offset;
    1086        } else if (option.equals("-novarcheckdeclsanduses")) {
    1087          noVarCheckDeclsAndUses = true;
    1088          return offset;
    1089        } else if (option.equals("-hidecall")) {
    1090          showCallDetails = false;
    1091          return offset;
    1092        } else if (option.equals("-showloop")) {
    1093          showLoopDetails = true;
    1094          return offset;
    1095        } else if (option.equals("-plainwarning")) {
    1096          plainWarning = true;
    1097          return offset;
    1098        } else if (option.equals("-noredundancy")) {
    1099          checkRedundantSpecs = false;
    1100          return offset;
    1101        } else if (option.equals("-notrace")) {
    1102          traceInfo = 0;
    1103          return offset;
    1104        } else if (option.equals("-verbosetrace")) {
    1105          traceInfo = 2;
    1106          return offset;
    1107        } else if (option.equals("-counterexample")) {
    1108          counterexample = true;
    1109          return offset;
    1110        } else if (option.equals("-bubblenotdown") ||
    1111                   option.equals("-bnd")) {
    1112          bubbleNotDown = true;
    1113          return offset;
    1114        } else if (option.equals("-nooutcalls")) {
    1115          noOutCalls = true;
    1116          return offset;
    1117        } else if (option.equals("-backpredfile") ||
    1118                   option.equals("-bpf")) {
    1119          if (offset >= args.length) {
    1120            throw new UsageError("Option " + option +
    1121                                 " requires one argument");
    1122          }
    1123          univBackPredFile = args[offset];
    1124          return offset+1;
    1125        } else if (option.equals("-sxlog")) {
    1126          if (offset>=args.length) {
    1127            throw new UsageError("Option " + option +
    1128                                 " requires one argument");
    1129          }
    1130          sxLog = args[offset];
    1131          return offset+1;
    1132        } else if (option.equals("-pxlog")) {
    1133          if (offset>=args.length) {
    1134            throw new UsageError("Option " + option +
    1135                                 " requires one argument");
    1136          }
    1137          sxLog = args[offset];
    1138          prettyPrintVC = true;
    1139          return offset+1;
    1140        } else if (option.equals("-nowarn")) {
    1141          if (offset >= args.length) {
    1142            throw new UsageError("Option " + option +
    1143                                 " requires one argument");
    1144          }
    1145          if (args[offset].equals("All")) {
    1146            NoWarn.setAllChkStatus(TagConstants.CHK_AS_ASSUME);
    1147          } else {
    1148            int tag = NoWarn.toNoWarnTag(args[offset]);
    1149            if (tag == 0) {
    1150              throw new UsageError("'" + args[offset]
    1151                                   + "' is not a legal warning category");
    1152            }
    1153            NoWarn.setChkStatus(tag, TagConstants.CHK_AS_ASSUME);
    1154          }
    1155          return offset+1;
    1156        } else if (option.equals("-warn")) {
    1157          if (offset>=args.length) {
    1158            throw new UsageError("Option " + option +
    1159                                 " requires one argument");
    1160          }
    1161          // Note:  There's an intentional lack of symmetry with -nowarn
    1162          // here, in that "-warn All" is not supported.  This design
    1163          // allows ESC/Java to include special checks, perhaps like the
    1164          // Stale checks of the Higher-Level Races checker, that won't
    1165          // be publicly advertised.
    1166          int tag = NoWarn.toNoWarnTag(args[offset]);
    1167          if (tag == 0) {
    1168            throw new UsageError("'" + args[offset]
    1169                                 + "' is not a legal warning category");
    1170          }
    1171          NoWarn.setChkStatus(tag, TagConstants.CHK_AS_ASSERT);
    1172          return offset+1;
    1173        } else if (option.equals("-parseplus")) {
    1174          parsePlus = true;
    1175          return offset;
    1176        } else if (option.equals("-nonotcheckedwarnings")) {
    1177          noNotCheckedWarnings = true;
    1178          return offset;
    1179        } else if (option.equals("-testref")) {
    1180          testRef = true;
    1181          return offset;
    1182        } else if (option.equals("-strictexceptions")) {
    1183          strictExceptions = true;
    1184          return offset;
    1185        } else if (option.equals("-checkpurity")) {
    1186          checkPurity = true;
    1187          return offset;
    1188        } else if (option.equals("-nocheckpurity")) {
    1189          checkPurity = false;
    1190          return offset;
    1191        } else if (option.equals("-ppvc") ||
    1192                   option.equals("-prettyprintvc")) {
    1193          prettyPrintVC = true;
    1194          return offset;
    1195        } else if (option.equals("-sds") ||
    1196                   option.equals("-showdesugaredspecs")) {
    1197          desugaredSpecs = true;
    1198          return offset;
    1199        } else if (option.equals("-javaassertions") ||
    1200                   option.equals("-eajava")) {
    1201          assertionMode = JAVA_ASSERTIONS;
    1202          assertionsEnabled = true;
    1203          assertIsKeyword = true;
    1204          return offset;
    1205        } else if (option.equals("-jmlassertions") ||
    1206                   option.equals("-eajml")) {
    1207          assertionMode = JML_ASSERTIONS;
    1208          assertIsKeyword = true;
    1209          assertionsEnabled = true;
    1210          return offset;
    1211        } else if (option.equals("-rewritedepth")) {
    1212          if (offset >= args.length) {
    1213            throw new UsageError("Option " + option +
    1214                                 " requires one integer argument");
    1215          }
    1216          rewriteDepth = Integer.parseInt(args[offset]);
    1217          return offset+1;
    1218        } else if (option.equals("-nosemicolonwarnings")) {
    1219          noSemicolonWarnings = true;
    1220          return offset;
    1221        } else if (option.equals("-usefcns")) {
    1222          useFcnsForModelVars = true;
    1223          useFcnsForMethods = true;
    1224          useFcnsForAllocations = true;
    1225          return offset;
    1226        } else if (option.equals("-usevars")) {
    1227          useFcnsForModelVars = false;
    1228          useFcnsForMethods = false;
    1229          useFcnsForAllocations = false;
    1230          return offset;
    1231        } else if (option.equals("-usefcnsformodelvars")) {
    1232          useFcnsForModelVars = true;
    1233          return offset;
    1234        } else if (option.equals("-usevarsformodelvars")) {
    1235          useFcnsForModelVars = false;
    1236          return offset;
    1237        } else if (option.equals("-usefcnsformethods")) {
    1238          useFcnsForMethods = true;
    1239          return offset;
    1240        } else if (option.equals("-usevarsformethods")) {
    1241          useFcnsForMethods = false;
    1242          return offset;
    1243        } else if (option.equals("-showfields")) {
    1244          showFields = true;
    1245          return offset;
    1246        } else if (option.equals("-simplify")) {
    1247          // FIXME - shcek for additional argument
    1248          simplify = args[offset];
    1249          //System.setProperty("simplify",args[offset]);
    1250          return offset+1;
    1251        } else if (option.equals("-escprojectfilev0")) {
    1252          // Ignored, but also used to mark a project file.
    1253          return offset;
    1254        } else if (option.equals("-nonnullelements") ||
    1255                   option.equals("-nne")) {
    1256          nne = true;
    1257          return offset+1;
    1258        } else if (option.equals("-useoldstringhandling")) {
    1259          useOldStringHandling = true;
    1260          return offset;
    1261        } else if (option.equals("-usethrowable")) {
    1262          useThrowable = true;
    1263          return offset;
    1264        }
    1265
    1266        // Pass on unrecognized options:
    1267        return super.processOption(option, args, offset);
    1268      }
    1269
    1270
    1271      private Vector readFile(String filename) {
    1272        Vector r = new Vector();
    1273        StringBuffer s = new StringBuffer();
    1274        Reader R = null;
    1275        try {
    1276          R = new BufferedReader(new InputStreamReader(new FileInputStream(filename)));
    1277          int c;
    1278          do {
    1279            while( (c=R.read())!= -1 && c != '\n' ) {
    1280              s.append( (char)c );
    1281            }
    1282            // Delete from 3rd space on
    1283            String st = s.toString();
    1284            int i=st.indexOf(' ');
    1285            if( i != -1 ) i=st.indexOf(' ',i+1);
    1286            if( i != -1 ) i=st.indexOf(' ',i+1);
    1287            if( i != -1 ) st=st.substring(0,i);
    1288            r.addElement( st );
    1289            s.setLength(0);
    1290          } while( c != -1 );
    1291          return r;
    1292        } catch(IOException e) {
    1293          throw new RuntimeException("IOException: " + e);
    1294        } finally {
    1295          try {
    1296            if (R != null) R.close();
    1297          } catch (IOException e) {
    1298            throw new RuntimeException(
    1299                                       "IOException: " + e);
    1300          }
    1301        }
    1302      }
    1303
    1304      public String nowarnOptionString() {
    1305        StringBuffer sb = new StringBuffer(200);
    1306        for (int i = escjava.ast.TagConstants.FIRSTESCCHECKTAG;
    1307             i < escjava.ast.TagConstants.CHKQUIET; ++i) {
    1308          if (NoWarn.getChkStatus(i) == escjava.ast.TagConstants.CHK_AS_ASSUME) {
    1309            sb.append(" -nowarn ");
    1310            sb.append(escjava.ast.TagConstants.toString(i));
    1311          }
    1312        }
    1313        return sb.toString();
    1314      }
    1315    } // end of class Options
    1316
    1317    /*
    1318     * Local Variables:
    1319     * Mode: Java
    1320     * fill-column: 85
    1321     * End:
    1322     */
    1323