org.jmlspecs.jmldoc.jmldoc_142
Class Main

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

All Implemented Interfaces:

Cloneable, TroubleReporter

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
class	Main.JmlHtmlTask           This class jmlizes java files for each listed java file.
static class	Main.JmlPrivacyChecker
class	Main.MjdocTask           This class drives the generation of html files.

 

Nested classes inherited from class org.jmlspecs.checker.Main

Main.JmlCheckAssignableTask, Main.JmlParseTask, Main.JmlTypecheckTask

 

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
protected  JmlHtmlFactory	htmlGenerator           This object is used to generate html files.
protected  ArrayList	packageList

 

Fields inherited from class org.jmlspecs.checker.Main

jmlOptions, refinedFileSequenceSet

 

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  void	addRecursivePackages(String packageName, File dir, ArrayList dirs)           This adds all subdirectories (recursively) as packages to be processed.
static boolean	compile(String[] args)           Second entry point.
static boolean	compile(String[] args, JmldocOptions opt, OutputStream os)           Entry point for the GUI
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  MjcCommonOptions	getOptionsInstance(MjcCommonOptions opt)           Assigns opt to the local instance of RacOptions and returns opt as an instance of MjcCommonOptions so it can be assigned to the options variable in mjc's Main.
protected  void	handleOptionInteractions()           Take care of some interactions among options.
void	handlePackages(ArrayList packages, ArrayList dirs, ArrayList infiles)           Processes all the package names found on the command-line, altering the list of directories or files as appropriate.
(package private) static void	init()
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).
boolean	parseArguments(String[] args, ArrayList infiles)           Parses the argument list.
boolean	runParser(String[] args, MjcCommonOptions opt, ArrayList infiles)           Runs the argument parser only so the GUI can process options from the command line
protected  void	taskQueueEmptied()           Implemented in jmldoc to cause the generation of all the html files by the appropriate call into the doclet api.

 

Methods inherited from class org.jmlspecs.checker.Main

canStopSequenceBeforeAllPasses, catchUpRefinedFile, catchUpTask, classToGenerate, compile, createCompilationUnitContext, exposeOptions, filenameFilter, firstTask, firstTask, getDefaultFilter, getWarningFilterNameFromOptions, hasOptionXobspure, hasOptionXsymr, hasOptionXsymw, hasUnsafeOpWarningOption, includeAllRefinedCUnits, initialize, initSession, isCommandLineFile, isSpecOrJmlMode, jmlNoBodyOK, makeRelative

 

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, hasAlreadyFailedToParseFor, hasAlreadySuccessfullyParsed, initSession, interruptCompilation, isAnExpectedResult, isCurrentlyParsingFor, mainSequenceID, nonNullTypes, noteError, optimizeCode, options, parseAtFile, parseComments, prettyPrint, processTaskQueue, quietMode, RecommendedWarning, reportTrouble, reportTroubleFiltered, RMJ, run, run, runCompilation, runInitialization, runSetInitialTasks, safeMath, setAllowUniverses, setContextBehavior, setMainSequenceID, setUniverseChecks, setUniversePurity, subdirectoryFilter, successfullyParsed, suppressWarning, 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

packageList

protected ArrayList packageList

htmlGenerator

protected JmlHtmlFactory htmlGenerator

This object is used to generate html files. Derived classes may initialize this variable with an alternate derivative of JmlHTML, if desired (do so in the derived class constructor).

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 own version of modifier utilities.

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.

runParser

public boolean runParser(String[] args,
                         MjcCommonOptions opt,
                         ArrayList infiles)

Runs the argument parser only so the GUI can process options from the command line

Overrides:

runParser in class Main

compile

public static boolean compile(String[] args,
                              JmldocOptions 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

init

static void init()

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 RacOptions 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

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

handleOptionInteractions

protected void handleOptionInteractions()

Take care of some interactions among options.

handlePackages

public void handlePackages(ArrayList packages,
                           ArrayList dirs,
                           ArrayList infiles)

Description copied from class: Main

Processes all the package names found on the command-line, altering the list of directories or files as appropriate. The implementation for mjc simply converts package names to the absolute path names of the directories in which they are found (per the sourcepath and classpath) and adds the directory to the list in dirs.

Overrides:

handlePackages in class Main

addRecursivePackages

protected void addRecursivePackages(String packageName,
                                    File dir,
                                    ArrayList dirs)

This adds all subdirectories (recursively) as packages to be processed.

createTaskAfter

protected Main.Task createTaskAfter(Main.Task oldTask)

Description copied from class: Main

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

taskQueueEmptied

protected void taskQueueEmptied()

Implemented in jmldoc to cause the generation of all the html files by the appropriate call into the doclet api. This method is called by #run(String[]) when all reentrant invocations of #processTaskQueue() have been exited and in this implementation the method finalizes the generation of the HTML. This method should be overridden by subclasses to perform final work after completion of all tasks.

Overrides:

taskQueueEmptied in class Main