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