org.jmlspecs.checker
Class Main

java.lang.Object
  org.multijava.util.Utils
      org.multijava.util.compiler.Compiler
          org.multijava.mjc.Main
              org.jmlspecs.checker.Main

All Implemented Interfaces:

Cloneable, TroubleReporter

Direct Known Subclasses:

Main, Main

public class Main

extends Main

This class implements the entry point of the JML compiler. Use java org.jmlspecs.checker.Main --help to get usage options.

Nested Class Summary
(package private) static class	Main.Filter           This class is used with the Directory.list method to list those files in a directory that this program is interested in processing - in this case, all those that end in '.java', '.jml' or '.spec'.
class	Main.JmlCheckAssignableTask           A task for checking assignable clauses; this task has to be done after type checking of assignable clauses of the super types so the fields can be combined with those of the subtype (the subtype is the one whose code is being checked against the assignable clauses but the inherited assignable clauses need to be type checked first).
class	Main.JmlParseTask           This class parses a group of files, given by filenames as strings, and generates a forest of ASTs.
class	Main.JmlTypecheckTask           This class typechecks the source code.
(package private) static class	Main.PTMode

 

Nested classes inherited from class org.multijava.mjc.Main

Main.CheckInitializerTask, Main.CheckInterfaceTask, Main.ContextBehavior, Main.DFilter, Main.ExpectedGF, Main.ExpectedIndifferent, Main.ExpectedResult, Main.ExpectedType, Main.ParseTask, Main.PreprocessTask, Main.PrettyPrintTask, Main.ResolveSpecializerTask, Main.ResolveTopMethodTask, Main.Task, Main.TaskTimes, Main.TranslateMJTask, Main.TreeProcessingTask, Main.Trees, Main.TypecheckTask

 

Field Summary
private  HashSet	commandLineFiles           The set of files specified on the command line to be processed during the current session.
(package private) static Main.PTMode	JAVA_MODE
(package private) static Main.PTMode	JML_MODE
static JmlCommonOptions	jmlOptions           Command-line options.
protected  HashSet	refinedFileSequenceSet           Tracks the set of task sequence IDs for tasks spawned to process files refined by files on the main task sequence.
(package private) static Main.PTMode	SPEC_MODE

 

Fields inherited from class org.multijava.mjc.Main

activeSequenceID, activeTaskPriority, allowUniverseAnnotations, allowUniverseBytecode, allowUniverseChecks, allowUniverseDynChecks, allowUniverseKeywords, allowUniversePurity, appName, classes, codeGenNeeded, contextsCreated, destination, errorFound, errorLimit, filesFound, mostSevereWarningIssued, options, parseJavadoc, PRI_CHECK_INITIALIZER, PRI_CHECK_INTERFACE, PRI_PARSE, PRI_PREPROCESS, PRI_PRETTY_PRINT, PRI_RESOLVE_SPECIALIZER, PRI_TOP_METHODS, PRI_TRANSLATE_MJ, PRI_TYPECHECK, taskQueue, uncheckedWarningsIssued, UNIVERSE_ANNOTATIONS, UNIVERSE_BYTECODE, UNIVERSE_CHECKS, UNIVERSE_DYNCHECKS, UNIVERSE_FULL, UNIVERSE_NO, UNIVERSE_PARSE, UNIVERSE_PURITY, universeVersion

 

Fields inherited from class org.multijava.util.compiler.Compiler

PRINT_TO_ERR, PRINT_TO_OUT

 

Fields inherited from class org.multijava.util.Utils

DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO

 

Constructor Summary
	Main()           The principal constructor for an object to do the work of the Jml compiler.
protected	Main(ModifierUtility modUtil)           Construct a JML compiler (an object of Main) that uses the given ModifierUtility.

 

Method Summary
protected  boolean	canStopSequenceBeforeAllPasses(Main.Task oldTask)           Returns true if it is OK to abort processing of the given task before it has been processed through all compilation passes.
JCompilationUnitType	catchUpRefinedFile(File file)           Parses a file and returns the AST.
void	catchUpTask(Main.Task task)           This version of catchUp reactivates the given task.
void	classToGenerate(CSourceClass clazz)           Adds a class to the list of classes to be generated in bytecode.
static boolean	compile(String[] args)           Second entry point.
static boolean	compile(String[] args, JmlOptions opt, OutputStream os)           Entry point for the GUI
CCompilationUnitContextType	createCompilationUnitContext(JCompilationUnitType jc, CCompilationUnit cunit)           Creates a compilation unit context for this compiler.
protected  Main.Task	createTaskAfter(Main.Task oldTask)           This method uses the dynamic type of oldTask along with the command line options to determine what task to add to the task queue after the given task completes.
protected  void	exposeOptions(JmlCommonOptions opt)           Sets the static field, jmlOptions, to the given arugment so that typechecking routines can access command-line options.
protected  FilenameFilter	filenameFilter()           Overridable method that provides a filter to list all the relevant files in a directory; for mjc this is all files whose names end in ".java".
Main.ParseTask	firstTask(File filename, Main.ExpectedResult expected)           Generates the first task in the compilation sequence.
Main.ParseTask	firstTask(ArrayList infiles)           Generates the first task in the compilation sequence.
protected  WarningFilter	getDefaultFilter()           Return an instance of the JML default warning filter.
protected  MjcCommonOptions	getOptionsInstance(MjcCommonOptions opt)           Assigns opt to the local instance of JmlCommonOptions and returns opt as an instance of MjcCommonOptions so it can be assigned to the options variable in mjc's Main.
protected  String	getWarningFilterNameFromOptions(MjcCommonOptions opts)           Get the warning filter's class name from the options structure.
static boolean	hasOptionXobspure()
static boolean	hasOptionXsymr()           Returns true iff the command-line option -Xsym or -Xsymr is specified.
static boolean	hasOptionXsymw()           Returns true iff the command-line option -Xsym or -Xsymw is specified.
static boolean	hasUnsafeOpWarningOption()
protected  CompilerPassEnterable[]	includeAllRefinedCUnits(CompilerPassEnterable[] trees)
protected  void	initialize()           Initialize the compiler (read classpath, initialize type descriptors)
protected  void	initSession()           Initializes the "class loader" for this compilation session.
boolean	isCommandLineFile(File f)           This method returns true iff the file f was specified on the command line.
static boolean	isSpecOrJmlMode(TokenReference t)
protected  boolean	jmlNoBodyOK(CContextType context)
static void	main(String[] args)           The entry point when starting this program from the command line.
protected  MjcCommonOptions	makeOptionsInstance()           This function creates an object to do the parsing of the command line arguments and to store the values of the flags and options so obtained (it does not actually do the argument parsing).
static String	makeRelative(String path, String referenceDir, String separator)           This function should return a path for the first argument that is relative to the second argument (which may be a directory or a file); if the paths are the same, an empty string is returned.
boolean	parseArguments(String[] args, ArrayList infiles)           Parses the argument list.

 

Methods inherited from class org.multijava.mjc.Main

activeSequenceID, adoptCompilationUnitContext, bugReportBoilerplate, bugReportProperty, bugReportRequest, catchUp, catchUp, catchUpGF, catchUpType, checkPackageName, compile, contextBehavior, currentlyParsingFor, expandAtFiles, experimentalArrayHandling, failedParsing, firstCheckingTask, genCode, Generic, Generic, getClasses, getFilter, handleDirectories, handleNonOptions, handlePackageName, handlePackages, hasAlreadyFailedToParseFor, hasAlreadySuccessfullyParsed, initSession, interruptCompilation, isAnExpectedResult, isCurrentlyParsingFor, mainSequenceID, nonNullTypes, noteError, optimizeCode, options, parseAtFile, parseComments, prettyPrint, processTaskQueue, quietMode, RecommendedWarning, reportTrouble, reportTroubleFiltered, RMJ, run, run, runCompilation, runInitialization, runParser, runSetInitialTasks, safeMath, setAllowUniverses, setContextBehavior, setMainSequenceID, setUniverseChecks, setUniversePurity, subdirectoryFilter, successfullyParsed, suppressWarning, taskQueueEmptied, universeBytecode, universeBytecodeAnnotations, universeChecks, universeDynChecks, universeKeywords, universePurity, universeVersion, validPackageName, verboseMode

 

Methods inherited from class org.multijava.util.compiler.Compiler

getTimestamp, inform, inform, inform, inform, inform, inform, inform, inform, inform, modUtil, run, setOutputStream, verifyFiles, verifyFiles

 

Methods inherited from class org.multijava.util.Utils

assertTrue, assertTrue, combineArrays, escapeString, escapeString, fail, fail, getFilePath, hasFlag, hasOtherFlags, parsePathParts, relativePathTo, splitQualifiedName, splitQualifiedName, stripJavaModifiers, stripNonJavaModifiers, stripPrivateModifier, unescapeString, vectorToArray, vectorToIntArray

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Field Detail

JAVA_MODE

static final Main.PTMode JAVA_MODE

SPEC_MODE

static final Main.PTMode SPEC_MODE

JML_MODE

static final Main.PTMode JML_MODE

refinedFileSequenceSet

protected HashSet refinedFileSequenceSet

Tracks the set of task sequence IDs for tasks spawned to process files refined by files on the main task sequence. Tasks with sequence IDs in this set should not be prematurely aborted but should be allowed to pass through all same compiler passes as main sequence tasks.

commandLineFiles

private HashSet commandLineFiles

The set of files specified on the command line to be processed during the current session.

jmlOptions

public static JmlCommonOptions jmlOptions

Command-line options.

 invariant jmlOptions == options;
 

Main

public Main()

The principal constructor for an object to do the work of the Jml compiler.

Main

protected Main(ModifierUtility modUtil)

Construct a JML compiler (an object of Main) that uses the given ModifierUtility. This constructor allows the subclasses to have their owen version of modifier utilities.

jmlNoBodyOK

protected boolean jmlNoBodyOK(CContextType context)

main

public static void main(String[] args)

The entry point when starting this program from the command line.

Parameters:

args - the command line arguments

compile

public static boolean compile(String[] args)

Second entry point. This function is overridden from mjc.Main so that we can * instantiate a derived class Main object.

compile

public static boolean compile(String[] args,
                              JmlOptions opt,
                              OutputStream os)

Entry point for the GUI

Parameters:

args - the file, package, and directory names

opt - the options for the tool

os - the output stream for the compiler messages

initSession

protected void initSession()

Initializes the "class loader" for this compilation session.

Overrides:

initSession in class Main

makeOptionsInstance

protected MjcCommonOptions makeOptionsInstance()

This function creates an object to do the parsing of the command line arguments and to store the values of the flags and options so obtained (it does not actually do the argument parsing). It is overridden here from mjc.Main so that we can instantiate a JmlOptions object, in order to parse some new options specific to this compiler (cf. JmlOptions.opt).

Overrides:

makeOptionsInstance in class Main

See Also:

JmlOptions

getOptionsInstance

protected MjcCommonOptions getOptionsInstance(MjcCommonOptions opt)

Assigns opt to the local instance of JmlCommonOptions and returns opt as an instance of MjcCommonOptions so it can be assigned to the options variable in mjc's Main. This is done so we can access options that are only processed in MjcCommonOptions.

Overrides:

getOptionsInstance in class Main

exposeOptions

protected void exposeOptions(JmlCommonOptions opt)

Sets the static field, jmlOptions, to the given arugment so that typechecking routines can access command-line options.

 assignable jmlOptions;
 ensures jmlOptions == opt;
 

parseArguments

public boolean parseArguments(String[] args,
                              ArrayList infiles)

Parses the argument list. Mutates infiles, options. Returns true if there were no problems parsing the arguments. The list of command line arguments is parsed per the options defined in JmlOptions.opt. Values of given options are stored in the protected variable super.options. Remaining command-line arguments are considered to be filenames or directories. Any directories are expanded to be all the *.java files in the directory (recursively including *.java files in subdirectories if the --recursive flag is set). The resulting list of files to be processed is stored in the ArrayList infiles.

Overrides:

parseArguments in class Main

createCompilationUnitContext

public CCompilationUnitContextType createCompilationUnitContext(JCompilationUnitType jc,
                                                                CCompilationUnit cunit)

Creates a compilation unit context for this compiler.

 also
   requires cunit != null;
   ensures \result != null && contextsCreated.contains(\result);
 

Overrides:

createCompilationUnitContext in class Main

isSpecOrJmlMode

public static boolean isSpecOrJmlMode(TokenReference t)

firstTask

public Main.ParseTask firstTask(ArrayList infiles)

Generates the first task in the compilation sequence. This is a method so subclasses can modify the task sequence.

 also
   requires infiles != null && (\forall Object o; infiles.contains(o);
                                  o instanceof String);
 

Overrides:

firstTask in class Main

firstTask

public Main.ParseTask firstTask(File filename,
                                Main.ExpectedResult expected)

Generates the first task in the compilation sequence. This is a method so subclasses can modify the task sequence.

Overrides:

firstTask in class Main

getWarningFilterNameFromOptions

protected String getWarningFilterNameFromOptions(MjcCommonOptions opts)

Description copied from class: Main

Get the warning filter's class name from the options structure. This is a hook method that can be overridden by subclasses.

Overrides:

getWarningFilterNameFromOptions in class Main

getDefaultFilter

protected WarningFilter getDefaultFilter()

Return an instance of the JML default warning filter.

Overrides:

getDefaultFilter in class Main

filenameFilter

protected FilenameFilter filenameFilter()

Description copied from class: Main

Overridable method that provides a filter to list all the relevant files in a directory; for mjc this is all files whose names end in ".java".

Overrides:

filenameFilter in class Main

classToGenerate

public void classToGenerate(CSourceClass clazz)

Adds a class to the list of classes to be generated in bytecode. It is overridden here from mjc.Main to ignore model classes and interfaces, and to work only during the second round of compilation.

 also
   requires clazz != null;
   assignable classes;
   ensures classes.contains(clazz);
 

Overrides:

classToGenerate in class Main

isCommandLineFile

public boolean isCommandLineFile(File f)

This method returns true iff the file f was specified on the command line.

catchUpTask

public void catchUpTask(Main.Task task)

This version of catchUp reactivates the given task. TaskQueue passes as far as other files have been processed.

 requires task != null;
 

catchUpRefinedFile

public JCompilationUnitType catchUpRefinedFile(File file)

Parses a file and returns the AST.

 requires file != null;
 

canStopSequenceBeforeAllPasses

protected boolean canStopSequenceBeforeAllPasses(Main.Task oldTask)

Returns true if it is OK to abort processing of the given task before it has been processed through all compilation passes.

createTaskAfter

protected Main.Task createTaskAfter(Main.Task oldTask)

This method uses the dynamic type of oldTask along with the command line options to determine what task to add to the task queue after the given task completes.

 also
   requires oldTask != null && oldTask.completed;
   ensures \result == null || 
           (\result.sequenceID() == oldTask.sequenceID());
 

Overrides:

createTaskAfter in class Main

initialize

protected void initialize()

Initialize the compiler (read classpath, initialize type descriptors)

Overrides:

initialize in class Main

includeAllRefinedCUnits

protected CompilerPassEnterable[] includeAllRefinedCUnits(CompilerPassEnterable[] trees)

makeRelative

public static String makeRelative(String path,
                                  String referenceDir,
                                  String separator)

This function should return a path for the first argument that is relative to the second argument (which may be a directory or a file); if the paths are the same, an empty string is returned.

hasOptionXobspure

public static boolean hasOptionXobspure()

hasOptionXsymr

public static boolean hasOptionXsymr()

Returns true iff the command-line option -Xsym or -Xsymr is specified. This option lets the compiler to parse external symbol table files instead of the source files.

hasOptionXsymw

public static boolean hasOptionXsymw()

Returns true iff the command-line option -Xsym or -Xsymw is specified. This option lets the compiler to generate external symbol table files as the compilation result.

hasUnsafeOpWarningOption

public static boolean hasUnsafeOpWarningOption()