JML

org.jmlspecs.jmlrac
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.jmlrac.Main
All Implemented Interfaces:
Cloneable, TroubleReporter
Direct Known Subclasses:
Main

public class Main
extends Main

A class implementing the entry point of the JML RAC compiler.

See Also:
Main, Main

Nested Class Summary
 class Main.JavaParseTask
          A parser class for the seconding round compilation.
 class Main.JmlGenerateAssertionTask
          A task for generating runtime assertion checker (RAC) code.
 class Main.JmlPrettyPrintTask
          A task class for pretty-printing the trees in the AST forest.
 class Main.JmlWriteAssertionTask
          A task class for generating RAC code.
 
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  boolean isSecondRound
          Indicates whether we are in the first or second round of compilation.
static ModifierUtility modUtil
          Default modifier utility to use.
static int PRI_GENERATE_ASSERTION
          Task priorities for tasks defined in this class.
static int PRI_GENERATE_SYMBOL
           
private  Map racFileMap
          Map from temp RAC file names to their original file names
static RacOptions racOptions
          Command-line options.
 
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()
          Constructs a JML RAC compiler with a default modifier utility.
protected Main(ModifierUtility modUtil)
          Constructs a JML RAC compiler with the given modifier utility, modUtil.
 
Method Summary
 void classToGenerate(CSourceClass clazz)
          Adds a class to the list of classes to be generated in bytecode.
static boolean compile(String[] args)
          Runs a JML RAC compiler on the given arguments.
static boolean compile(String[] args, RacOptions opt, OutputStream os)
          Entry point for the GUI
 CCompilationUnitContextType createCompilationUnitContext(JCompilationUnitType jc, CCompilationUnit cunit)
          Creates a compilation unit context for this compiler.
protected  JmlRacGenerator createRacGenerator(RacOptions opt, Main main)
           
protected  Main.Task createTaskAfter(Main.Task oldTask)
          Returns the next task to be performed after oldTask.
protected  void exposeOptions(JmlCommonOptions opt)
          Sets the static field, jmlOptions, to the given arugment so that typechecking routines can access command-line options.
private static JmlCompilationUnit[] filterOut(CompilerPassEnterable[] trees)
          Filter out files that aren't to be processed; we do however keep non-.java files, whatever their suffix.
 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  Map getFileMap()
          Accessor method to racFileMap.
protected  MjcCommonOptions getOptionsInstance(MjcCommonOptions opt)
          Assigns opt to the local instance of RacOptions, assigns opt to an instance of jmlOptions in the checker, and returns opt as an instance of MjcCommonOptions so it can be assigned to the options variable in mjc's Main.
static boolean hasOptionXsymr()
           
static boolean hasOptionXsymw()
           
protected  void initSecondSession()
          Initializes the "class loader" for the second round of compilation.
static boolean isSpecMode(JmlTypeDeclaration decl)
          Returns true if this type should be processed in spec mode - that is if methods and constructors without bodies are allowed.
static void main(String[] args)
          Runs a JML RAC compiler on the command line arguments.
protected  MjcCommonOptions makeOptionsInstance()
          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).
protected  void prepareSecondRound()
          Prepares the second round of compilation by cleaning side-effects done by the first round.
protected  void setFileMap(Map map)
           
 
Methods inherited from class org.jmlspecs.checker.Main
canStopSequenceBeforeAllPasses, catchUpRefinedFile, catchUpTask, compile, filenameFilter, getDefaultFilter, getWarningFilterNameFromOptions, hasOptionXobspure, hasUnsafeOpWarningOption, includeAllRefinedCUnits, initialize, initSession, isCommandLineFile, isSpecOrJmlMode, jmlNoBodyOK, makeRelative, parseArguments
 
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

PRI_GENERATE_ASSERTION

public static final int PRI_GENERATE_ASSERTION
Task priorities for tasks defined in this class.


PRI_GENERATE_SYMBOL

public static final int PRI_GENERATE_SYMBOL

racFileMap

private Map racFileMap
Map from temp RAC file names to their original file names


modUtil

public static final ModifierUtility modUtil
Default modifier utility to use.


isSecondRound

protected boolean isSecondRound
Indicates whether we are in the first or second round of compilation.


racOptions

public static RacOptions racOptions
Command-line options.

 invariant racOptions == options;
 

Constructor Detail

Main

public Main()
Constructs a JML RAC compiler with a default modifier utility.


Main

protected Main(ModifierUtility modUtil)
Constructs a JML RAC compiler with the given modifier utility, modUtil.

Method Detail

main

public static void main(String[] args)
Runs a JML RAC compiler on the command line arguments.


compile

public static boolean compile(String[] args)
Runs a JML RAC compiler on the given arguments.


compile

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

isSpecMode

public static boolean isSpecMode(JmlTypeDeclaration decl)
Returns true if this type should be processed in spec mode - that is if methods and constructors without bodies are allowed. This is the case if it is the declaration of a class and the file name containing the declaration does not end in .java.


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 method returns JML parser if this is the first round; otherwise, this method returns Java parser.

Overrides:
firstTask in class Main

makeOptionsInstance

protected MjcCommonOptions makeOptionsInstance()
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 RacOptions object, in order to parse some new options specific to this compiler (cf. RacOptions.opt).

Overrides:
makeOptionsInstance in class Main
See Also:
RacOptions

getOptionsInstance

protected MjcCommonOptions getOptionsInstance(MjcCommonOptions opt)
Assigns opt to the local instance of RacOptions, assigns opt to an instance of jmlOptions in the checker, 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.

 also
   assignable jmlOptions;
   ensures jmlOptions == opt;
 

Overrides:
exposeOptions 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

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

prepareSecondRound

protected void prepareSecondRound()
Prepares the second round of compilation by cleaning side-effects done by the first round.


initSecondSession

protected void initSecondSession()
Initializes the "class loader" for the second round of compilation.


createTaskAfter

protected Main.Task createTaskAfter(Main.Task oldTask)
Returns the next task to be performed after 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. It is overriden here to add JML RAC specific tasks.

 also
   requires oldTask != null;
 

Overrides:
createTaskAfter in class Main

filterOut

private static JmlCompilationUnit[] filterOut(CompilerPassEnterable[] trees)
Filter out files that aren't to be processed; we do however keep non-.java files, whatever their suffix. Filters out non-RACable files. E.g., ".jml" files.


createRacGenerator

protected JmlRacGenerator createRacGenerator(RacOptions opt,
                                             Main main)

getFileMap

protected Map getFileMap()
Accessor method to racFileMap. This is used by the wrappers Main class to compile all the generated files.


setFileMap

protected void setFileMap(Map map)

hasOptionXsymr

public static boolean hasOptionXsymr()
Description copied from class: Main
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()
Description copied from class: Main
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.


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.