org.jmlspecs.jml4.compiler
Class JmlCompilerOptions

java.lang.Object
  org.eclipse.jdt.internal.compiler.impl.CompilerOptions
      org.jmlspecs.jml4.compiler.JmlCompilerOptions

public class JmlCompilerOptions
extends CompilerOptions

Field Summary

static java.lang.String	NON_NULL
static java.lang.String	NULLABLE Possible values for configurable options
static java.lang.String	OPTION_DefaultNullity
static java.lang.String	OPTION_EnableCounts
static java.lang.String	OPTION_EnableEsc2EchoOutput
static java.lang.String	OPTION_EnableJml Option IDs
static java.lang.String	OPTION_EnableJml2Checker
static java.lang.Object	OPTION_EnableJml2Compiler
static java.lang.String	OPTION_EnableJmlDbc
static java.lang.String	OPTION_EnableJmlEsc
static java.lang.String	OPTION_EnableJmlEsc2
static java.lang.String	OPTION_EnableJmlFspv
static java.lang.String	OPTION_EnableJmlNewLoopSemantics
static java.lang.String	OPTION_EnableRac
static java.lang.String	OPTION_ExplicitNullityAnnotations
static java.lang.String	OPTION_JmlEsc2CommandLineArgs
static java.lang.String	OPTION_ReportJmlCommentDisabled
static java.lang.String	OPTION_ReportNonNullTypeSystem
static java.lang.String	OPTION_SimplifyPath
static java.lang.String	OPTION_SpecPath
static long	ReportJmlCommentDisabled
static long	ReportNonNullTypeSystem Bit mask for configurable problems (error/warning threshold) BEWARE: Keep an eye on the bits used by the JDT.
static long	ReqExplicitNullityAnnotations

Fields inherited from class org.eclipse.jdt.internal.compiler.impl.CompilerOptions

AccessEmulation, AccidentalBooleanAssign, ALL_STANDARD_TAGS, AnnotationSuperInterface, AssertUsedAsAnIdentifier, AutoBoxing, complianceLevel, DEFAULT, defaultEncoding, DISABLED, DiscouragedReference, DO_NOT_GENERATE, docCommentSupport, EmptyStatement, ENABLED, EnumUsedAsAnIdentifier, ERROR, errorThreshold, FallthroughCase, FieldHiding, FinallyBlockNotCompleting, FinalParameterBound, ForbiddenReference, GENERATE, generateClassFiles, IGNORE, IncompatibleNonInheritedInterfaceMethod, IncompleteEnumSwitch, IndirectStaticAccess, inlineJsrBytecode, InvalidJavadoc, isTaskCaseSensitive, jml2CheckerEnabled, jml2CompilerEnabled, jmlDbcEnabled, jmlDefaultIsNonNull, jmlEnabled, jmlEsc2CommandLineArgs, jmlEsc2EchoOutputEnabled, jmlEsc2Enabled, jmlEscEnabled, jmlEscGovernsRac, jmlEscProverStrategy, jmlFspvEnabled, jmlNewLoopSemanticsEnabled, jmlNullityCountsEnabled, jmlRacEnabled, jmlSimplifyPath, jmlSpecPath, LocalVariableHiding, MaskedCatchBlock, maxProblemsPerUnit, MethodWithConstructorName, MissingDeprecatedAnnotation, MissingJavadocComments, MissingJavadocTagDescription, MissingJavadocTags, MissingOverrideAnnotation, MissingSerialVersion, NO_TAG, NoEffectAssignment, NoImplicitStringConversion, NonExternalizedString, NonStaticAccessToStatic, NullReference, OPTIMIZE_OUT, OPTION_Compliance, OPTION_DocCommentSupport, OPTION_Encoding, OPTION_FatalOptionalError, OPTION_GenerateClassFiles, OPTION_InlineJsr, OPTION_LineNumberAttribute, OPTION_LocalVariableAttribute, OPTION_MaxProblemPerUnit, OPTION_PreserveUnusedLocal, OPTION_Process_Annotations, OPTION_ReportAnnotationSuperInterface, OPTION_ReportAssertIdentifier, OPTION_ReportAutoboxing, OPTION_ReportDeprecation, OPTION_ReportDeprecationInDeprecatedCode, OPTION_ReportDeprecationWhenOverridingDeprecatedMethod, OPTION_ReportDiscouragedReference, OPTION_ReportEmptyStatement, OPTION_ReportEnumIdentifier, OPTION_ReportFallthroughCase, OPTION_ReportFieldHiding, OPTION_ReportFinallyBlockNotCompletingNormally, OPTION_ReportFinalParameterBound, OPTION_ReportForbiddenReference, OPTION_ReportHiddenCatchBlock, OPTION_ReportIncompatibleNonInheritedInterfaceMethod, OPTION_ReportIncompleteEnumSwitch, OPTION_ReportIndirectStaticAccess, OPTION_ReportInvalidAnnotation, OPTION_ReportInvalidJavadoc, OPTION_ReportInvalidJavadocTags, OPTION_ReportInvalidJavadocTagsDeprecatedRef, OPTION_ReportInvalidJavadocTagsNotVisibleRef, OPTION_ReportInvalidJavadocTagsVisibility, OPTION_ReportLocalVariableHiding, OPTION_ReportMethodWithConstructorName, OPTION_ReportMissingAnnotation, OPTION_ReportMissingDeprecatedAnnotation, OPTION_ReportMissingJavadoc, OPTION_ReportMissingJavadocComments, OPTION_ReportMissingJavadocCommentsOverriding, OPTION_ReportMissingJavadocCommentsVisibility, OPTION_ReportMissingJavadocTagDescription, OPTION_ReportMissingJavadocTags, OPTION_ReportMissingJavadocTagsOverriding, OPTION_ReportMissingJavadocTagsVisibility, OPTION_ReportMissingOverrideAnnotation, OPTION_ReportMissingSerialVersion, OPTION_ReportNoEffectAssignment, OPTION_ReportNoImplicitStringConversion, OPTION_ReportNonExternalizedStringLiteral, OPTION_ReportNonStaticAccessToStatic, OPTION_ReportNullReference, OPTION_ReportOverridingMethodWithoutSuperInvocation, OPTION_ReportOverridingPackageDefaultMethod, OPTION_ReportParameterAssignment, OPTION_ReportPossibleAccidentalBooleanAssignment, OPTION_ReportPotentialNullReference, OPTION_ReportRawTypeReference, OPTION_ReportRedundantNullCheck, OPTION_ReportRedundantSuperinterface, OPTION_ReportSpecialParameterHidingField, OPTION_ReportSyntheticAccessEmulation, OPTION_ReportTypeParameterHiding, OPTION_ReportUncheckedTypeOperation, OPTION_ReportUndocumentedEmptyBlock, OPTION_ReportUnhandledWarningToken, OPTION_ReportUnnecessaryElse, OPTION_ReportUnnecessaryTypeCheck, OPTION_ReportUnqualifiedFieldAccess, OPTION_ReportUnusedDeclaredThrownException, OPTION_ReportUnusedDeclaredThrownExceptionExemptExceptionAndThrowable, OPTION_ReportUnusedDeclaredThrownExceptionIncludeDocCommentReference, OPTION_ReportUnusedDeclaredThrownExceptionWhenOverriding, OPTION_ReportUnusedImport, OPTION_ReportUnusedLabel, OPTION_ReportUnusedLocal, OPTION_ReportUnusedParameter, OPTION_ReportUnusedParameterIncludeDocCommentReference, OPTION_ReportUnusedParameterWhenImplementingAbstract, OPTION_ReportUnusedParameterWhenOverridingConcrete, OPTION_ReportUnusedPrivateMember, OPTION_ReportUnusedTypeArgumentsForMethodInvocation, OPTION_ReportUnusedWarningToken, OPTION_ReportVarargsArgumentNeedCast, OPTION_Source, OPTION_SourceFileAttribute, OPTION_SuppressWarnings, OPTION_TargetPlatform, OPTION_TaskCaseSensitive, OPTION_TaskPriorities, OPTION_TaskTags, OverriddenPackageDefaultMethod, OverridingMethodWithoutSuperInvocation, ParameterAssignment, parseLiteralExpressionsAsConstants, performMethodsFullRecovery, performStatementsRecovery, PotentialNullReference, PRESERVE, preserveAllLocalVariables, PRIVATE, processAnnotations, produceDebugAttributes, produceReferenceInfo, PROTECTED, PUBLIC, RawTypeReference, RedundantNullCheck, RedundantSuperinterface, reportDeprecationInsideDeprecatedCode, reportDeprecationWhenOverridingDeprecatedMethod, reportInvalidJavadocTags, reportInvalidJavadocTagsDeprecatedRef, reportInvalidJavadocTagsNotVisibleRef, reportInvalidJavadocTagsVisibility, reportMissingJavadocCommentsOverriding, reportMissingJavadocCommentsVisibility, reportMissingJavadocTagDescription, reportMissingJavadocTagsOverriding, reportMissingJavadocTagsVisibility, reportSpecialParameterHidingField, reportUnusedDeclaredThrownExceptionExemptExceptionAndThrowable, reportUnusedDeclaredThrownExceptionIncludeDocCommentReference, reportUnusedDeclaredThrownExceptionWhenOverriding, reportUnusedParameterIncludeDocCommentReference, reportUnusedParameterWhenImplementingAbstract, reportUnusedParameterWhenOverridingConcrete, RETURN_TAG, sourceLevel, storeAnnotations, subOptions, suppressWarnings, targetJDK, Task, taskPriorites, taskTags, treatOptionalErrorAsFatal, TypeHiding, UncheckedTypeOperation, UndocumentedEmptyBlock, UnhandledWarningToken, UnnecessaryElse, UnnecessaryTypeCheck, UnqualifiedFieldAccess, UnusedArgument, UnusedDeclaredThrownException, UnusedImport, UnusedLabel, UnusedLocalVariable, UnusedPrivateMember, UnusedTypeArguments, UnusedWarningToken, UsingDeprecatedAPI, VarargsArgumentNeedCast, verbose, VERSION_1_1, VERSION_1_2, VERSION_1_3, VERSION_1_4, VERSION_1_5, VERSION_1_6, VERSION_1_7, VERSION_CLDC1_1, VERSION_JSR14, WARNING, warningThreshold, warningTokens

Constructor Summary

JmlCompilerOptions()

Method Summary

Methods inherited from class org.eclipse.jdt.internal.compiler.impl.CompilerOptions

getMap, getSeverity, getSeverityString, getVisibilityString, optionKeyFromIrritant, optionKeyToIrritant, set, toString, updateSeverity, useNonNullTypeSystem, versionFromJdkLevel, versionToJdkLevel, warningOptionNames, warningTokenFromIrritant, warningTokenToIrritants

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

OPTION_EnableJml

public static final java.lang.String OPTION_EnableJml

Option IDs

See Also:

Constant Field Values

OPTION_EnableJmlNewLoopSemantics

public static final java.lang.String OPTION_EnableJmlNewLoopSemantics

See Also:

Constant Field Values

OPTION_ReportJmlCommentDisabled

public static final java.lang.String OPTION_ReportJmlCommentDisabled

See Also:

Constant Field Values

OPTION_SpecPath

public static final java.lang.String OPTION_SpecPath

See Also:

Constant Field Values

OPTION_EnableJmlDbc

public static final java.lang.String OPTION_EnableJmlDbc

See Also:

Constant Field Values

OPTION_EnableJmlEsc

public static final java.lang.String OPTION_EnableJmlEsc

See Also:

Constant Field Values

OPTION_DefaultNullity

public static final java.lang.String OPTION_DefaultNullity

See Also:

Constant Field Values

OPTION_ReportNonNullTypeSystem

public static final java.lang.String OPTION_ReportNonNullTypeSystem

See Also:

Constant Field Values

OPTION_EnableCounts

public static final java.lang.String OPTION_EnableCounts

See Also:

Constant Field Values

OPTION_ExplicitNullityAnnotations

public static final java.lang.String OPTION_ExplicitNullityAnnotations

See Also:

Constant Field Values

OPTION_EnableRac

public static final java.lang.String OPTION_EnableRac

See Also:

Constant Field Values

OPTION_EnableJmlFspv

public static final java.lang.String OPTION_EnableJmlFspv

See Also:

Constant Field Values

OPTION_EnableJmlEsc2

public static final java.lang.String OPTION_EnableJmlEsc2

See Also:

Constant Field Values

OPTION_JmlEsc2CommandLineArgs

public static final java.lang.String OPTION_JmlEsc2CommandLineArgs

See Also:

Constant Field Values

OPTION_EnableEsc2EchoOutput

public static final java.lang.String OPTION_EnableEsc2EchoOutput

See Also:

Constant Field Values

OPTION_SimplifyPath

public static final java.lang.String OPTION_SimplifyPath

See Also:

Constant Field Values

OPTION_EnableJml2Checker

public static final java.lang.String OPTION_EnableJml2Checker

See Also:

Constant Field Values

OPTION_EnableJml2Compiler

public static final java.lang.Object OPTION_EnableJml2Compiler

NULLABLE

public static final java.lang.String NULLABLE

Possible values for configurable options

See Also:

Constant Field Values

NON_NULL

public static final java.lang.String NON_NULL

See Also:

Constant Field Values

ReportNonNullTypeSystem

public static final long ReportNonNullTypeSystem

Bit mask for configurable problems (error/warning threshold) BEWARE: Keep an eye on the bits used by the JDT. Ensure that the bits used by JML are not also used by the JDT.

See Also:

Constant Field Values

ReqExplicitNullityAnnotations

public static final long ReqExplicitNullityAnnotations

See Also:

Constant Field Values

ReportJmlCommentDisabled

public static final long ReportJmlCommentDisabled

See Also:

Constant Field Values

Constructor Detail

JmlCompilerOptions

public JmlCompilerOptions()