edu.utep.cs.utjml.compiler
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
                      edu.utep.cs.utjml.compiler.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.UtJmlParseTask This class parses a group of files, given by filenames as strings, and generates a forest of ASTs.

Nested classes/interfaces inherited from class org.jmlspecs.jmlrac.Main

Main.JavaParseTask, Main.JmlGenerateAssertionTask, Main.JmlPrettyPrintTask, Main.JmlWriteAssertionTask

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

Main.JmlCheckAssignableTask, Main.JmlParseTask, Main.JmlTypecheckTask

Nested classes/interfaces 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

static UtJmlOptions

utjmlOptions Command-line options.

Fields inherited from class org.jmlspecs.jmlrac.Main

isSecondRound, modUtil, PRI_GENERATE_ASSERTION, PRI_GENERATE_SYMBOL, racOptions

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.

Method Summary

JCompilationUnitType	catchUpRefinedFile(File file) Parses a file and returns the AST.
static boolean	compile(String[] args) Second entry point.
static boolean	compile(String[] args, UtJmlOptions opt, OutputStream os) Entry point for the GUI
protected JmlRacGenerator	createRacGenerator(RacOptions opt, Main main)
protected void	exposeOptions(JmlCommonOptions opt) Sets the static field, jmlOptions, to the given arugment so that typechecking routines can access command-line options.
Main.ParseTask	firstTask(ArrayList infiles) Generates the first task in the compilation sequence.
Main.ParseTask	firstTask(File filename, Main.ExpectedResult expected) Generates the first task in the compilation sequence.
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	hasOptionXcs() Returns true if the -Xcs, call sequence, is specified.
static boolean	hasOptionXtgen() Returns true if the -Xtgen, test case generation, is specified.
protected void	initSession() Initializes the "class loader" for this compilation session.
static void	main(String[] args) The entry point when starting this program from the command line.
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).

Methods inherited from class org.jmlspecs.jmlrac.Main

classToGenerate, compile, createCompilationUnitContext, createTaskAfter, getFileMap, hasOptionXsymr, hasOptionXsymw, initSecondSession, isSpecMode, prepareSecondRound, setFileMap

Methods inherited from class org.jmlspecs.checker.Main

canStopSequenceBeforeAllPasses, catchUpTask, compile, filenameFilter, getDefaultFilter, getWarningFilterNameFromOptions, hasOptionXobspure, hasUnsafeOpWarningOption, includeAllRefinedCUnits, initialize, 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

utjmlOptions

public static UtJmlOptions utjmlOptions

Command-line options.

 invariant racOptions == options;
 

Constructor Detail

Main

public Main()

Constructs a JML RAC compiler with a default modifier utility.

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.

compile

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

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.

 assignable jmlOptions;
 ensures jmlOptions == opt;
 

Overrides:

exposeOptions in class Main

initSession

protected void initSession()

Initializes the "class loader" for this compilation session.

Overrides:

initSession in class Main

catchUpRefinedFile

public JCompilationUnitType catchUpRefinedFile(File file)

Parses a file and returns the AST.

 requires file != null;
 

Overrides:

catchUpRefinedFile in class Main

createRacGenerator

protected JmlRacGenerator createRacGenerator(RacOptions opt,
                                             Main main)

Overrides:

createRacGenerator in class Main

hasOptionXcs

public static boolean hasOptionXcs()

Returns true if the -Xcs, call sequence, is specified.

hasOptionXtgen

public static boolean hasOptionXtgen()

Returns true if the -Xtgen, test case generation, is specified.