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