org.jmlspecs.jmlunit
Class Main

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

All Implemented Interfaces:

Cloneable, Constants, Constants, Constants, TroubleReporter

public class Main

extends Main

implements Constants

A class implementing the entry point of the JML/JUnit test oracle generator. Use java org.jmlspecs.jmlunit.Main --help to get usage options.

Version:

$Revision: 1.31 $

Author:

Yoonsik Cheon, David R. Cok, Kristina Boysen, Gary T. Leavens

Class Specifications

Specifications inherited from class Main

invariant this.taskQueue != null ==> ( \forall java.lang.Object o; this.taskQueue.contains(o); o instanceof org.multijava.mjc.Main.Task); private invariant ( \forall org.multijava.mjc.Main.Task t; t != null; t.sequenceID() == this.mainSequenceID <==> (* t does not belong to a task sequence used to * catch up recursively loaded files *)); private invariant ( \forall java.lang.Object o; this.currentlyParsingRelation.containsValue(o); o instanceof java.util.Set); private invariant ( \forall java.lang.Object o; this.failedParsingRelation.containsValue(o); o instanceof java.util.Set); private invariant ( \forall java.lang.Object o; this.alreadyParsedSet.contains(o); o instanceof java.lang.String); invariant this.appName != null;

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Specifications inherited from interface Constants

invariant "junit.framework.".length() > 0 ==> "junit.framework.".charAt("junit.framework.".length()) == 46; invariant "org.jmlspecs.jmlrac.runtime.".length() > 0 ==> "org.jmlspecs.jmlrac.runtime.".charAt("org.jmlspecs.jmlrac.runtime.".length()) == 46; invariant "org.jmlspecs.jmlunit.".length() > 0 ==> "org.jmlspecs.jmlunit.".charAt("org.jmlspecs.jmlunit.".length()) == 46; invariant "org.jmlspecs.jmlunit.strategies.".length() > 0 ==> "org.jmlspecs.jmlunit.strategies.".charAt("org.jmlspecs.jmlunit.".length()) == 46;

Specifications inherited from interface Constants

public invariant true;

Nested Class Summary
class	Main.TestClassGenerationTask           A task for generating JML/JUnit test oracle classes.

 

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

 

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
static int	PRI_TEST_CLASS_GENERATION           The task priority for generating test class.

 

Fields inherited from class org.multijava.mjc.Main

activeSequenceID, activeTaskPriority, allowUniverseAnnotations, allowUniverseBytecode, allowUniverseChecks, allowUniverseDynChecks, allowUniverseKeywords, allowUniversePurity, alreadyParsedSet, appName, classes, codeGenNeeded, contextsCreated, currentlyParsingRelation, destination, errorFound, errorLimit, failedParsingRelation, 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.jmlspecs.jmlunit.Constants

DOT_JAVA, PKG_JMLRAC, PKG_JMLUNIT, PKG_JUNIT, PKG_STRATEGIES, TEST_CLASS_FILE_NAME_POSTFIX, TEST_CLASS_NAME_POSTFIX, TEST_DATA_FILE_NAME_POSTFIX, TEST_DATA_NAME_POSTFIX, TEST_METHOD_NAME_PREFIX

 

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()           Constructs an object for generating test oracles.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
static boolean	compile(String[] args)           Generates JML/JUnit test oracle classes with the given argument, args, and returns true if all the test classes are successfully generated.
static boolean	compile(String[] args, JntOptions opt, OutputStream os)           Entry point for the GUI
protected  Main.Task	createTaskAfter(Main.Task oldTask)           Returns the next task to be added to the task queue after the given task, oldTask, completes.
(package private) static String	genPackageName(JCompilationUnitType cunit, JntOptions options)
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.
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).

 

Methods inherited from class org.multijava.mjc.Main

activeSequenceID, adoptCompilationUnitContext, bugReportBoilerplate, bugReportProperty, bugReportRequest, catchUp, catchUp, catchUpGF, catchUpType, checkPackageName, classToGenerate, compile, contextBehavior, createCompilationUnitContext, currentlyParsingFor, expandAtFiles, experimentalArrayHandling, failedParsing, filenameFilter, firstCheckingTask, firstTask, firstTask, genCode, Generic, Generic, getClasses, getDefaultFilter, getFilter, handleDirectories, handleNonOptions, handlePackageName, handlePackages, 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, 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_TEST_CLASS_GENERATION

public static final int PRI_TEST_CLASS_GENERATION

The task priority for generating test class.

Main

public Main()

Constructs an object for generating test oracles.

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/JUnit test oracle classes with the given argument, args, and returns true if all the test classes are successfully generated.

compile

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

genPackageName

static String genPackageName(JCompilationUnitType cunit,
                             JntOptions options)

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

Overrides:

makeOptionsInstance in class Main

See Also:

JntOptions

Specifications inherited from overridden method in class Main:

ensures \result != null;

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

Specifications:

     also

requires opt instanceof org.jmlspecs.jmlunit.JntOptions;

Specifications inherited from overridden method in class Main:
      --- None ---

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

Specifications inherited from overridden method in class Main:
      --- None ---

createTaskAfter

protected Main.Task createTaskAfter(Main.Task oldTask)

Returns the next task to be added to the task queue after the given task, oldTask, completes.

Overrides:

createTaskAfter in class Main

Specifications:

     also

requires oldTask != null&&oldTask.completed;
ensures \result == null||(\result .sequenceID() == oldTask.sequenceID());

Specifications inherited from overridden method createTaskAfter(Main.Task oldTask) in class Main:

requires oldTask != null&&oldTask.completed;
ensures \result == null||(\result .sequenceID() == oldTask.sequenceID());