org.jmlspecs.jmlspec
Class Main

java.lang.Object
  org.multijava.util.Utils
      org.multijava.util.compiler.Compiler
          org.multijava.mjc.Main
              org.jmlspecs.jmlspec.Main

All Implemented Interfaces:

Cloneable, Constants, Constants, TroubleReporter

public class Main

extends Main

implements Constants

A class implementing the entry point of the jmlspec specification skeleton generator/comparator. Use java org.jmlspecs.jmlspec.Main --help to get usage options.

Version:

$Revision: 1.27 $

Author:

David Cok

Nested Class Summary
class	Main.JspBinaryPrinterTask
class	Main.JspCompareTask           A task for generating specification skeletons.
class	Main.JspParseTask           A task for generating specification skeletons.
class	Main.JspPrettyPrinterTask           A task for generating specification skeletons.
(package private) static class	Main.SuffixFilter           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 a valid suffix.

 

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.Filter, Main.ParseTask, Main.PreprocessTask, Main.PrettyPrintTask, Main.ResolveSpecializerTask, Main.ResolveTopMethodTask, Main.Task, Main.TaskTimes, Main.TranslateMJTask, Main.TreeProcessingTask, Main.Trees, Main.TypecheckTask

 

Field Summary
(package private) static String[]	also
protected static String[]	annotation
(package private)  ArrayList	binaries
protected static String[]	classAnnotation
(package private) static String[]	comment
static int	javaSuffixIndex
(package private)  Map	map           Map of fully-qualified class names (/-separated) to the arrays of ASTs that hold the parsed versions of all of the refinement files.
(package private) static String[]	nocomment
static int	PRI_SKELETON_GENERATION           The task priority for generating test class.
static String[]	validSuffixes           Valid suffixes for specification files.

 

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

 

Fields inherited from interface org.multijava.mjc.Constants

ACC_MODIFIER_FLAGS_MASK, ACC_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_PURE, ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, IMPLICITLY_NON_NULL, JAV_ASSERTION_ERROR, JAV_CLASS, JAV_CLASSLOADER, JAV_CLASSNOTFOUND_EXCEPTION, JAV_CLONE, JAV_CLONEABLE, JAV_CONSTRUCTOR, JAV_ERROR, JAV_EXCEPTION, JAV_INIT, JAV_LENGTH, JAV_NAME_SEPARATOR, JAV_NOCLASSDEFFOUND_ERROR, JAV_OBJECT, JAV_OUTER_THIS, JAV_RMJ_RUNTIME_EXCEPTION, JAV_RUNTIME, JAV_RUNTIME_EXCEPTION, JAV_SERIALIZABLE, JAV_STATIC_INIT, JAV_STRING, JAV_STRINGBUFFER, JAV_SUPER, JAV_THIS, JAV_THROWABLE, MJ_ANCHOR, NULLITY_MODS, OPE_BAND, OPE_BNOT, OPE_BOR, OPE_BSR, OPE_BXOR, OPE_EQ, OPE_GE, OPE_GT, OPE_LAND, OPE_LE, OPE_LNOT, OPE_LOR, OPE_LT, OPE_MINUS, OPE_NE, OPE_PERCENT, OPE_PLUS, OPE_POSTDEC, OPE_POSTINC, OPE_PREDEC, OPE_PREINC, OPE_SIMPLE, OPE_SL, OPE_SLASH, OPE_SR, OPE_STAR, TID_ARRAY, TID_BOOLEAN, TID_BYTE, TID_CHAR, TID_CLASS, TID_DOUBLE, TID_FLOAT, TID_INT, TID_LONG, TID_MAX, TID_SHORT, TID_VOID, UNIV_ARRAY_TMP, UNIV_TMP

 

Fields inherited from interface org.multijava.util.classfile.Constants

ACC_ABSTRACT, ACC_FINAL, ACC_INTERFACE, ACC_NATIVE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, ACC_STRICT, ACC_SUPER, ACC_SYNCHRONIZED, ACC_SYNTHETIC, ACC_TRANSIENT, ACC_VOLATILE, ATT_ANCHOR, ATT_BRIDGE, ATT_CODE, ATT_CONSTANTVALUE, ATT_DEPRECATED, ATT_DISPATCHER, ATT_EXCEPTIONS, ATT_GENERIC, ATT_GENERIC_FUNCTIONS, ATT_INNERCLASSES, ATT_LINENUMBERTABLE, ATT_LOCALVARIABLETABLE, ATT_MM_BODY, ATT_REDIRECTOR, ATT_RMJ_GLUE, ATT_RMJ_SIGNATURE, ATT_RUNTIME_VISIBLE_ANNOTATIONS, ATT_RUNTIME_VISIBLE_PARAMETER_ANNOTATIONS, ATT_SIGNATURE, ATT_SOURCEFILE, ATT_SYNTHETIC, ATT_UNIVERSE_FIELD, ATT_UNIVERSE_METHOD, ATT_UNIVERSE_VERSION, CST_CLASS, CST_DOUBLE, CST_FIELD, CST_FLOAT, CST_INTEGER, CST_INTERFACEMETHOD, CST_LONG, CST_METHOD, CST_NAMEANDTYPE, CST_STRING, CST_UTF8, ENV_DEBUG_MODE, ENV_USE_CACHE, JAVA_MAGIC, JAVA_MAJOR, JAVA_MINOR, MAX_CODE_PER_METHOD, opc_aaload, opc_aastore, opc_aconst_null, opc_aload, opc_aload_0, opc_aload_1, opc_aload_2, opc_aload_3, opc_anewarray, opc_areturn, opc_arraylength, opc_astore, opc_astore_0, opc_astore_1, opc_astore_2, opc_astore_3, opc_athrow, opc_baload, opc_bastore, opc_bipush, opc_caload, opc_castore, opc_checkcast, opc_d2f, opc_d2i, opc_d2l, opc_dadd, opc_daload, opc_dastore, opc_dcmpg, opc_dcmpl, opc_dconst_0, opc_dconst_1, opc_ddiv, opc_dload, opc_dload_0, opc_dload_1, opc_dload_2, opc_dload_3, opc_dmul, opc_dneg, opc_drem, opc_dreturn, opc_dstore, opc_dstore_0, opc_dstore_1, opc_dstore_2, opc_dstore_3, opc_dsub, opc_dup, opc_dup2, opc_dup2_x1, opc_dup2_x2, opc_dup_x1, opc_dup_x2, opc_f2d, opc_f2i, opc_f2l, opc_fadd, opc_faload, opc_fastore, opc_fcmpg, opc_fcmpl, opc_fconst_0, opc_fconst_1, opc_fconst_2, opc_fdiv, opc_fload, opc_fload_0, opc_fload_1, opc_fload_2, opc_fload_3, opc_fmul, opc_fneg, opc_frem, opc_freturn, opc_fstore, opc_fstore_0, opc_fstore_1, opc_fstore_2, opc_fstore_3, opc_fsub, opc_getfield, opc_getstatic, opc_goto, opc_goto_w, opc_i2b, opc_i2c, opc_i2d, opc_i2f, opc_i2l, opc_i2s, opc_iadd, opc_iaload, opc_iand, opc_iastore, opc_iconst_0, opc_iconst_1, opc_iconst_2, opc_iconst_3, opc_iconst_4, opc_iconst_5, opc_iconst_m1, opc_idiv, opc_if_acmpeq, opc_if_acmpne, opc_if_icmpeq, opc_if_icmpge, opc_if_icmpgt, opc_if_icmple, opc_if_icmplt, opc_if_icmpne, opc_ifeq, opc_ifge, opc_ifgt, opc_ifle, opc_iflt, opc_ifne, opc_ifnonnull, opc_ifnull, opc_iinc, opc_iload, opc_iload_0, opc_iload_1, opc_iload_2, opc_iload_3, opc_imul, opc_ineg, opc_instanceof, opc_invokeinterface, opc_invokespecial, opc_invokestatic, opc_invokevirtual, opc_ior, opc_irem, opc_ireturn, opc_ishl, opc_ishr, opc_istore, opc_istore_0, opc_istore_1, opc_istore_2, opc_istore_3, opc_isub, opc_iushr, opc_ixor, opc_jsr, opc_jsr_w, opc_l2d, opc_l2f, opc_l2i, opc_ladd, opc_laload, opc_land, opc_lastore, opc_lcmp, opc_lconst_0, opc_lconst_1, opc_ldc, opc_ldc2_w, opc_ldc_w, opc_ldiv, opc_lload, opc_lload_0, opc_lload_1, opc_lload_2, opc_lload_3, opc_lmul, opc_lneg, opc_lookupswitch, opc_lor, opc_lrem, opc_lreturn, opc_lshl, opc_lshr, opc_lstore, opc_lstore_0, opc_lstore_1, opc_lstore_2, opc_lstore_3, opc_lsub, opc_lushr, opc_lxor, opc_monitorenter, opc_monitorexit, opc_multianewarray, opc_new, opc_newarray, opc_nop, opc_pop, opc_pop2, opc_putfield, opc_putstatic, opc_ret, opc_return, opc_saload, opc_sastore, opc_sipush, opc_swap, opc_tableswitch, opc_wide, opc_xxxunusedxxx, POO_ASCII_CONSTANT, POO_CLASS_CONSTANT, POO_DOUBLE_CONSTANT, POO_FLOAT_CONSTANT, POO_INTEGER_CONSTANT, POO_LONG_CONSTANT, POO_NAT_CONSTANT, POO_REF_CONSTANT, POO_STRING_CONSTANT, TYP_ADDRESS, TYP_DOUBLE, TYP_FLOAT, TYP_INT, TYP_LONG, TYP_REFERENCE, TYP_VOID

 

Constructor Summary

Main()

 

Method Summary
String	checkPackageName(String packageName, boolean quiet)           Checks whether a syntactically valid package name actually exists, and returns the directory location of the root of the package or null if there is no package by that name on the sourcepath or classpath.
static boolean	compile(String[] args)           Generates JML skeleton with the given argument, args, and returns true if all the skeletons are successfully generated.
static boolean	compile(String[] args, JspOptions opt, OutputStream os)           Entry point for the GUI
protected  Main.Task	createTaskAfter(Main.Task oldTask)           Adds JspPrettyPrinterTask or JspCompareTask after the regular parsing.
void	doBinaries()
protected  FilenameFilter	filenameFilter()           This filter returns all the files that are processed when a directory or package is named on the command-line.
(package private)  File	findFile(String qname, String suffix)
static int	findSuffixIndex(String s)           Generates an int corresponding to the suffix; no particular order, just has to be unique - used as the index into an array.
Main.ParseTask	firstTask(ArrayList infiles)           Generates the first task in the compilation sequence.
protected  MjcCommonOptions	getOptionsInstance(MjcCommonOptions opt)           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.
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.
static void	main(String[] args)           An entry point when starting 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).
protected  boolean	runInitialization(String[] args)           Invoked from within the method run to do the argument parsing and compiler setup prior to actually parsing files via the task mechanism; returns true if no errors are encountered during initialization; if false is returned the initialization is not necessarily complete.
protected  void	runSetInitialTasks(ArrayList infiles)           Sets up the initial tasks that start the parsing.
void	setTemplates(JspOptions options)

 

Methods inherited from class org.multijava.mjc.Main

activeSequenceID, adoptCompilationUnitContext, bugReportBoilerplate, bugReportProperty, bugReportRequest, catchUp, catchUp, catchUpGF, catchUpType, classToGenerate, compile, contextBehavior, createCompilationUnitContext, currentlyParsingFor, expandAtFiles, experimentalArrayHandling, failedParsing, firstCheckingTask, firstTask, genCode, Generic, Generic, getClasses, getDefaultFilter, getFilter, handleDirectories, handleNonOptions, handlePackageName, hasAlreadyFailedToParseFor, hasAlreadySuccessfullyParsed, initialize, initSession, initSession, interruptCompilation, isAnExpectedResult, isCurrentlyParsingFor, mainSequenceID, nonNullTypes, noteError, optimizeCode, options, parseArguments, parseAtFile, parseComments, prettyPrint, processTaskQueue, quietMode, RecommendedWarning, reportTrouble, reportTroubleFiltered, RMJ, run, run, runCompilation, runParser, 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

binaries

ArrayList binaries

map

Map map

Map of fully-qualified class names (/-separated) to the arrays of ASTs that hold the parsed versions of all of the refinement files.

PRI_SKELETON_GENERATION

public static final int PRI_SKELETON_GENERATION

The task priority for generating test class.

validSuffixes

public static final String[] validSuffixes

Valid suffixes for specification files.

javaSuffixIndex

public static final int javaSuffixIndex

annotation

protected static String[] annotation

classAnnotation

protected static String[] classAnnotation

nocomment

static final String[] nocomment

comment

static final String[] comment

also

static final String[] also

Main

public Main()

main

public static void main(String[] args)

An entry point when starting from the command line.

Parameters:

args - The command line arguments

compile

public static boolean compile(String[] args)

Generates JML skeleton with the given argument, args, and returns true if all the skeletons are successfully generated.

compile

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

runInitialization

protected boolean runInitialization(String[] args)

Description copied from class: Main

Invoked from within the method run to do the argument parsing and compiler setup prior to actually parsing files via the task mechanism; returns true if no errors are encountered during initialization; if false is returned the initialization is not necessarily complete.

Overrides:

runInitialization in class Main

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

checkPackageName

public String checkPackageName(String packageName,
                               boolean quiet)

Description copied from class: Main

Checks whether a syntactically valid package name actually exists, and returns the directory location of the root of the package or null if there is no package by that name on the sourcepath or classpath.

Overrides:

checkPackageName in class Main

filenameFilter

protected FilenameFilter filenameFilter()

This filter returns all the files that are processed when a directory or package is named on the command-line.

Overrides:

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

Overrides:

makeOptionsInstance in class Main

See Also:

JspOptions

getOptionsInstance

protected MjcCommonOptions getOptionsInstance(MjcCommonOptions opt)

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

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

firstTask

public Main.ParseTask firstTask(ArrayList infiles)

Description copied from class: Main

Generates the first task in the compilation sequence. This is a method so subclasses can modify the task sequence.

 requires infiles != null && (\forall Object o; infiles.contains(o);
                                  o instanceof String);
 

Overrides:

firstTask in class Main

runSetInitialTasks

protected void runSetInitialTasks(ArrayList infiles)

Description copied from class: Main

Sets up the initial tasks that start the parsing. Additional tasks may be generated if these files reference other classes that need parsing.

Overrides:

runSetInitialTasks in class Main

createTaskAfter

protected Main.Task createTaskAfter(Main.Task oldTask)

Adds JspPrettyPrinterTask or JspCompareTask after the regular parsing. Note that we only do the parsing, no other checking.

Overrides:

createTaskAfter in class Main

doBinaries

public void doBinaries()

findFile

File findFile(String qname,
              String suffix)

findSuffixIndex

public static int findSuffixIndex(String s)

Generates an int corresponding to the suffix; no particular order, just has to be unique - used as the index into an array.

setTemplates

public void setTemplates(JspOptions options)