|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectjavafe.Options
javafe.SrcToolOptions
escjava.Options
This class parses the options on the command-line and is a structure for holding the values of options.
Field Summary | |
boolean |
allocUseOpt
|
boolean |
allowAlsoRequires
|
boolean |
assertContinue
|
int |
assertionMode
|
boolean |
bubbleNotDown
|
boolean |
checkPurity
Temporary option to turn on purity checking, since it is off by default until purity issues with inheritance are resolved. |
boolean |
checkRedundantSpecs
Statically check against redundant specs? |
boolean |
checkSpecs
|
java.lang.String |
ClassVCPrefix
|
boolean |
counterexample
|
boolean |
desugaredSpecs
When set, prints out the desugared specs for debugging purposes. |
boolean |
dsa
|
(package private) java.lang.String[][] |
escPrivateOptionData
|
(package private) java.lang.String[][] |
escPublicOptionData
|
boolean |
excuseNullInitializers
|
boolean |
filterInvariants
|
boolean |
filterMethodSpecs
|
boolean |
guardedVC
|
java.lang.String |
guardedVCDir
|
java.lang.String |
guardedVCFileExt
|
java.lang.String |
guardedVCFileNumbers
|
java.lang.String |
guardedVCGuardFile
|
java.lang.String |
guardedVCPrefix
|
Set |
guardVars
|
boolean |
ifpvc2dot
|
Set |
ignoreAnnSet
|
boolean |
inferPredicates
|
boolean |
inlineConstructors
|
boolean |
inlineDepthFlags
|
boolean |
inlineFromConstructors
|
static int |
JAVA_ASSERTIONS
|
static int |
JML_ASSERTIONS
|
boolean |
lastVarUseOpt
|
boolean |
lazySubst
|
static int |
LOOP_FALL_THRU
|
static int |
LOOP_FAST
|
static int |
LOOP_SAFE
|
int |
loopTranslation
|
int |
loopUnrollCount
|
boolean |
loopUnrollHalf
|
int |
mapsUnrollCount
|
boolean |
mergeInv
|
java.lang.String |
MethodVCPrefix
|
int |
namePCsize
|
boolean |
nestQuantifiers
|
boolean |
nne
Enable support for generating type-predicates for the \nonnullelements keyword. |
boolean |
noDirectTargetsOpt
|
boolean |
noNotCheckedWarnings
When true, does not print any warnings about things not checked. |
boolean |
noOutCalls
|
boolean |
noPeepOptGCAssertFalse
|
boolean |
noSemicolonWarnings
JML requires semicolons to terminate annotations. |
boolean |
noVarCheckDeclsAndUses
|
boolean |
nvcg
|
boolean |
nvcgpi
|
boolean |
nvu
|
boolean |
parsePlus
When true, parses pragmas that begin with /*+@, which are normally parsed only by JML; this allows test runs in which everything JML parses is parsed by escjava, to see if we have full coverage of all of JML. |
boolean |
passify
|
boolean |
pcc
|
boolean |
pdsa
|
boolean |
peepOptE
|
boolean |
peepOptGC
|
boolean |
pgc
|
boolean |
pjt
|
boolean |
plainWarning
|
boolean |
pPvs
|
boolean |
preciseTargets
|
boolean |
predAbstract
|
boolean |
prettyPrintVC
When set, pretty-prints the VCs that are obtained with verbose output or in the log (-sxLog) |
boolean |
printAssumers
|
boolean |
printCompilationUnitsOnLoad
|
boolean |
pSimplify
|
boolean |
pvc
|
boolean |
pvsProof
|
int |
rewriteDepth
|
Set |
routinesToCheck
|
Set |
routinesToSkip
|
boolean |
showCallDetails
|
boolean |
showFields
|
boolean |
showLoopDetails
|
java.lang.String |
simplify
|
java.lang.String |
specspath
The dirpath or jar file of system specs to use. |
boolean |
spvc
|
int |
stages
Number of stages to run. |
int |
startLine
|
boolean |
statsQuantifierComplexity
|
boolean |
statsSpace
|
boolean |
statsTermComplexity
|
boolean |
statsTime
|
boolean |
statsVariableComplexity
|
boolean |
strictExceptions
|
int |
strongAssertPost
The following values are used: 0-never, 1-atomic (default), 2-always |
boolean |
suggest
|
java.lang.String |
sxLog
|
boolean |
testRef
When true, pretty prints each compilation unit on the command-line; this is only used for testing, to test the combining of refinements. |
int |
traceInfo
|
boolean |
trackReadChars
|
java.lang.String |
univBackPredFile
|
boolean |
useAllInvPostBody
|
boolean |
useAllInvPostCall
|
boolean |
useAllInvPreBody
|
boolean |
useDefpred
|
boolean |
useFcnsForAllocations
|
boolean |
useFcnsForMethods
|
boolean |
useFcnsForModelVars
|
boolean |
useHarvey
|
boolean |
useIntQuantAntecedents
|
boolean |
useOldStringHandling
|
boolean |
useSammy
|
boolean |
useSimplify
|
boolean |
useThrowable
JML allows only subtypes of Exception in signals clauses. |
boolean |
vc2dot
|
int |
vclimit
|
int |
wpnxw
|
boolean |
wpp
|
Fields inherited from class javafe.SrcToolOptions |
allowAvoidSpec, allowDepend, avoidSpec, processRecursively |
Fields inherited from class javafe.Options |
assertionsEnabled, assertIsKeyword, currentdir, eol, fileOrigin, inputEntries, issueUsage, NEVER_BINARY, NEVER_SOURCE, noCautions, PREFER_BINARY, PREFER_RECENT, PREFER_SOURCE, quiet, showErrorLocation, sysPath, testMode, userPath, userSourcePath, v |
Constructor Summary | |
Options()
|
Method Summary | |
java.lang.String |
nowarnOptionString()
|
int |
processOption(java.lang.String option,
java.lang.String[] args,
int offset)
Process next tool option. |
private java.util.Vector |
readFile(java.lang.String filename)
|
java.lang.String |
showNonOptions()
Print non-option usage info to System.err . |
java.lang.String |
showOptions(boolean all)
Generate all command-line option information. |
Methods inherited from class javafe.Options |
checkMoreArguments, format, processFileOfArgs, processOptions, processOptionsLoop, showOptionArray, usage |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
final java.lang.String[][] escPublicOptionData
final java.lang.String[][] escPrivateOptionData
public java.lang.String simplify
public boolean useSimplify
public boolean useSammy
public boolean useHarvey
public boolean pvsProof
public boolean nvcg
public boolean nvcgpi
public boolean pSimplify
public boolean pPvs
public boolean vc2dot
public boolean ifpvc2dot
public boolean suggest
public boolean pjt
public boolean nvu
public boolean pgc
public boolean pdsa
public boolean pvc
public boolean pcc
public boolean counterexample
public boolean statsTime
public boolean statsSpace
public boolean statsTermComplexity
public boolean statsVariableComplexity
public boolean statsQuantifierComplexity
public boolean plainWarning
public boolean useOldStringHandling
public boolean useThrowable
public java.lang.String specspath
public boolean checkRedundantSpecs
public int traceInfo
public boolean prettyPrintVC
public boolean desugaredSpecs
public boolean testRef
public boolean checkPurity
public boolean strictExceptions
public boolean parsePlus
public boolean noNotCheckedWarnings
public boolean noSemicolonWarnings
public int rewriteDepth
public boolean spvc
public boolean dsa
public boolean passify
public boolean wpp
public boolean useDefpred
public int wpnxw
public int namePCsize
public boolean peepOptE
public boolean peepOptGC
public boolean lazySubst
public boolean mergeInv
public static final int JAVA_ASSERTIONS
public static final int JML_ASSERTIONS
public int assertionMode
public boolean useAllInvPostCall
public boolean useAllInvPostBody
public boolean useAllInvPreBody
public boolean allocUseOpt
public static final int LOOP_FAST
public static final int LOOP_SAFE
public static final int LOOP_FALL_THRU
public int loopTranslation
public int loopUnrollCount
public boolean loopUnrollHalf
public int mapsUnrollCount
public boolean preciseTargets
public boolean predAbstract
public boolean inferPredicates
public boolean noDirectTargetsOpt
public boolean nestQuantifiers
public boolean lastVarUseOpt
public boolean noVarCheckDeclsAndUses
public boolean useIntQuantAntecedents
public boolean excuseNullInitializers
public int strongAssertPost
public boolean showCallDetails
public boolean showLoopDetails
public boolean bubbleNotDown
public int startLine
public int vclimit
public boolean checkSpecs
public boolean noOutCalls
public boolean printAssumers
public boolean noPeepOptGCAssertFalse
public boolean assertContinue
public boolean trackReadChars
public boolean guardedVC
public java.lang.String guardedVCDir
public java.lang.String guardedVCFileNumbers
public java.lang.String guardedVCGuardFile
public java.lang.String guardedVCPrefix
public java.lang.String guardedVCFileExt
public Set guardVars
public java.lang.String ClassVCPrefix
public java.lang.String MethodVCPrefix
public Set ignoreAnnSet
public boolean printCompilationUnitsOnLoad
public boolean useFcnsForModelVars
public boolean useFcnsForMethods
public boolean useFcnsForAllocations
public boolean filterInvariants
public boolean filterMethodSpecs
public Set routinesToCheck
public Set routinesToSkip
public boolean inlineConstructors
public boolean inlineDepthFlags
public boolean inlineFromConstructors
public java.lang.String sxLog
public boolean allowAlsoRequires
public boolean showFields
public int stages
1. loading, parsing, and type checking 2. generating the type-specific background predicate 3. translating from Java to GC 4. translating from GC to DSA 5. generating the VC from the GC 6. calling the theorem prover to verify the VC
Defaults to running all stages (6); must be positive.
-nocheck sets stages
to run all but the last
stage (5). The -stages option can be used to set
stages
to a particular value.
public java.lang.String univBackPredFile
public boolean nne
Constructor Detail |
public Options()
Method Detail |
public java.lang.String showOptions(boolean all)
showOptions
in class SrcToolOptions
all
- if true show all non-public (experimental) switches as well.
public java.lang.String showNonOptions()
SrcToolOptions
System.err
. Output
must include at least one newline.
showNonOptions
in class SrcToolOptions
public int processOption(java.lang.String option, java.lang.String[] args, int offset) throws UsageError
See Options.processOptions(String [])
for the complete
specification of this routine.
processOption
in class SrcToolOptions
UsageError
private java.util.Vector readFile(java.lang.String filename)
public java.lang.String nowarnOptionString()
|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |