JML

org.jmlspecs.checker
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
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;
 

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

Method Detail

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()

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.