org.jmlspecs.jmlrac
Class Main

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

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.

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.