JML

org.jmlspecs.jmldoc.jmldoc_142
Class Main

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.util.compiler.Compiler
          extended byorg.multijava.mjc.Main
              extended byorg.jmlspecs.checker.Main
                  extended byorg.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).

Constructor Detail

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.

Method Detail

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

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.