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