From: <js...@us...> - 2006-11-24 07:36:09
|
Revision: 18 http://svn.sourceforge.net/jcontracts/?rev=18&view=rev Author: jstuyts Date: 2006-11-23 23:36:06 -0800 (Thu, 23 Nov 2006) Log Message: ----------- Changed name 'iContract' to 'Java Contract Suite'. Modified Paths: -------------- trunk/source/java/net/sf/jcontracts/icontract/ArgMetaclassFactory.java trunk/source/java/net/sf/jcontracts/icontract/Class.java trunk/source/java/net/sf/jcontracts/icontract/CompilerOption.java trunk/source/java/net/sf/jcontracts/icontract/FileTarget.java trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java trunk/source/java/net/sf/jcontracts/icontract/Interface.java trunk/source/java/net/sf/jcontracts/icontract/MergeOption.java trunk/source/java/net/sf/jcontracts/icontract/Method.java trunk/source/java/net/sf/jcontracts/icontract/NoInitialCompilationOption.java trunk/source/java/net/sf/jcontracts/icontract/NoRepositoryCompilationOption.java trunk/source/java/net/sf/jcontracts/icontract/OutputOption.java trunk/source/java/net/sf/jcontracts/icontract/Repository.java trunk/source/java/net/sf/jcontracts/icontract/RepositoryOutputOption.java trunk/source/java/net/sf/jcontracts/icontract/SourceCompilerOption.java trunk/source/java/net/sf/jcontracts/icontract/Tool.java trunk/source/java/net/sf/jcontracts/icontract/Variable.java trunk/source/java/net/sf/jcontracts/icontract/VerboseOption.java Modified: trunk/source/java/net/sf/jcontracts/icontract/ArgMetaclassFactory.java =================================================================== --- trunk/source/java/net/sf/jcontracts/icontract/ArgMetaclassFactory.java 2006-11-23 17:23:27 UTC (rev 17) +++ trunk/source/java/net/sf/jcontracts/icontract/ArgMetaclassFactory.java 2006-11-24 07:36:06 UTC (rev 18) @@ -66,7 +66,7 @@ if (name.compareTo("j") == 0) { o = new NoInitialCompilationOption(name, parameters); } else { - throw new RuntimeException("icontract: error: unknown option -" + name); + throw new RuntimeException("Java Contract Suite: error: unknown option -" + name); } } catch (NoClassDefFoundError _ex) { Modified: trunk/source/java/net/sf/jcontracts/icontract/Class.java =================================================================== --- trunk/source/java/net/sf/jcontracts/icontract/Class.java 2006-11-23 17:23:27 UTC (rev 17) +++ trunk/source/java/net/sf/jcontracts/icontract/Class.java 2006-11-24 07:36:06 UTC (rev 18) @@ -14,8 +14,8 @@ implements InvCheck, PrePostCheck { private static final Logger log = Logger.getLogger(Class.class); public static final String REP_PREFIX = "__REP_"; - private static final String INV_GET_METHOD = "__iContract__getInvariantList"; - private static final String INV_SO_GET_METHOD = "__iContract__getInvariantSourceList"; + private static final String INV_GET_METHOD = "__JContractS__getInvariantList"; + private static final String INV_SO_GET_METHOD = "__JContractS__getInvariantSourceList"; private static final String INVARIANT_TAG_NAME = "invariant"; public static final String INVARIANT_CHECK_METHOD_NAME = "__check_invariant__"; public static final String INVARIANT_CHECK_AT_ENTRY = "__inv_check_at_entry__"; @@ -242,7 +242,7 @@ } } if (sig.length > 4) { - throw new RuntimeException("iContract:error: more than 4 arguments (" + f + ") not supported at the moment [991]. Easy to be added though."); + throw new RuntimeException("Java Contract Suite:error: more than 4 arguments (" + f + ") not supported at the moment [991]. Easy to be added though."); } else { return m; } @@ -348,7 +348,7 @@ if (isStatic()) { if (inv_conds.size() != 0) { - log.warn(getLocationDescription() + "icontract: WARNING: the invariants (" + inv_conds + ") associated with the static class " + getSignature() + " will not be enforced (not instrumented and no repository entry) due to the static modifier!"); + log.warn(getLocationDescription() + "Java Contract Suite: WARNING: the invariants (" + inv_conds + ") associated with the static class " + getSignature() + " will not be enforced (not instrumented and no repository entry) due to the static modifier!"); } return ""; } @@ -364,7 +364,7 @@ repositoryName = repositoryName + superclassName.substring(superclassName.lastIndexOf(".") + 1, superclassName.length()); } if (repositoryForInvExists(repositoryName)) { - body = body + " Vector super_vec = " + repositoryName + "." + "__iContract__getInvariantList" + "();\n"; + body = body + " Vector super_vec = " + repositoryName + "." + "__JContractS__getInvariantList" + "();\n"; body = body + " for (Enumeration e = super_vec.elements(); e.hasMoreElements(); ) {\n"; body = body + " vec.addElement( e.nextElement() );\n"; body = body + " }\n"; @@ -372,7 +372,7 @@ body = body + " // Repository for superclass " + superclassName + " (" + repositoryName + ") "; body = body + "does not exist or is not accessible.\n"; if (!superclassName.startsWith("java.")) { - log.error(getLocationDescription() + "icontract: WARNING: the repository of " + getSignature() + " will contain it's own invariants ONLY -- this is because the superclass of " + getSignature() + " (" + superclassName + ") may" + " either not have been " + "instrumented for invariants (or the repository file " + repositoryName + ".class is missing, e.g. was not compiled) !\n"); + log.error(getLocationDescription() + "Java Contract Suite: WARNING: the repository of " + getSignature() + " will contain it's own invariants ONLY -- this is because the superclass of " + getSignature() + " (" + superclassName + ") may" + " either not have been " + "instrumented for invariants (or the repository file " + repositoryName + ".class is missing, e.g. was not compiled) !\n"); } } } else { @@ -393,7 +393,7 @@ } String header = " /**This repository method captures the invariants of\n * class " + getSignature() + " and it's superclass " + superclassName + ".\n"; header = header + " */\n"; - header = header + " public static final Vector __iContract__getInvariantList() {"; + header = header + " public static final Vector __JContractS__getInvariantList() {"; String code = header + "\n Vector vec = new Vector();\n" + body + " return vec;\n" + " }\n"; body = ""; if (superclassName != null) { @@ -406,7 +406,7 @@ repositoryName = repositoryName + superclassName.substring(superclassName.lastIndexOf(".") + 1, superclassName.length()); } if (repositoryForInvExists(repositoryName)) { - body = body + " Vector super_vec = " + repositoryName + "." + "__iContract__getInvariantSourceList" + "();\n"; + body = body + " Vector super_vec = " + repositoryName + "." + "__JContractS__getInvariantSourceList" + "();\n"; body = body + " for (Enumeration e = super_vec.elements(); e.hasMoreElements(); ) {\n"; body = body + " vec.addElement( e.nextElement() );\n"; body = body + " }\n"; @@ -432,7 +432,7 @@ } header = " /**This repository method captures the source of invariants of\n * class " + getSignature() + " and it's superclass " + superclassName + ".\n"; header = header + " */\n"; - header = header + " public static final Vector __iContract__getInvariantSourceList() {"; + header = header + " public static final Vector __JContractS__getInvariantSourceList() {"; code = code + "\n" + header + "\n Vector vec = new Vector();\n" + body + " return vec;\n" + " }\n"; return code; } @@ -471,7 +471,7 @@ } } - System.err.println(getLocationDescription() + "iContract:WARNING: could not find " + ": " + short_name); + System.err.println(getLocationDescription() + "Java Contract Suite:WARNING: could not find " + ": " + short_name); return short_name; } @@ -518,13 +518,13 @@ } catch (NoSuchMethodException e) { if (!supercName.startsWith("java.")) { - log.error(getLocationDescription() + "iContract: WARNING: " + getSignature() + " can not delegate the invariant check of the superclass (" + supercName + ") to the appropriate method (method not found, see exception detailts below) because either (i) the superclass is not instrumented, (ii) the instrumented superclass is not compiled or (iii) the sourcecode of the superclass is not accessible -- SEMANTIC ATTENTION: trying to read the superclass' invariant from its repository (" + supercName + ") -- invariant may therefore not access private superclass information!" + "[caught exception: " + e + "]"); + log.error(getLocationDescription() + "Java Contract Suite: WARNING: " + getSignature() + " can not delegate the invariant check of the superclass (" + supercName + ") to the appropriate method (method not found, see exception detailts below) because either (i) the superclass is not instrumented, (ii) the instrumented superclass is not compiled or (iii) the sourcecode of the superclass is not accessible -- SEMANTIC ATTENTION: trying to read the superclass' invariant from its repository (" + supercName + ") -- invariant may therefore not access private superclass information!" + "[caught exception: " + e + "]"); } } } catch (ClassNotFoundException e) { if (!supercName.startsWith("java.")) { - log.error(getLocationDescription() + "iContract: WARNING: " + getSignature() + " can not delegate the invariant check of the superclass (" + supercName + ") to the appropriate method (method's clas not found, see exception detailts below) because either (i) the superclass is not instrumented, (ii) the instrumented superclass is not compiled or (iii) the sourcecode of the superclass is not accessible -- SEMANTIC ATTENTION: trying to read the superclass' invariant from its repository (" + supercName + ") -- invariant may therefore not access private superclass information!" + "[caught exception: " + e + "]"); + log.error(getLocationDescription() + "Java Contract Suite: WARNING: " + getSignature() + " can not delegate the invariant check of the superclass (" + supercName + ") to the appropriate method (method's clas not found, see exception detailts below) because either (i) the superclass is not instrumented, (ii) the instrumented superclass is not compiled or (iii) the sourcecode of the superclass is not accessible -- SEMANTIC ATTENTION: trying to read the superclass' invariant from its repository (" + supercName + ") -- invariant may therefore not access private superclass information!" + "[caught exception: " + e + "]"); } } } @@ -554,8 +554,8 @@ java.lang.Class c = java.lang.Class.forName(repositoryName); java.lang.Class noArgArray[] = new java.lang.Class[0]; try { - Method theIGMethod = c.getMethod("__iContract__getInvariantList", noArgArray); - Method theISGMethod = c.getMethod("__iContract__getInvariantSourceList", noArgArray); + Method theIGMethod = c.getMethod("__JContractS__getInvariantList", noArgArray); + Method theISGMethod = c.getMethod("__JContractS__getInvariantSourceList", noArgArray); try { Vector invs = (Vector)theIGMethod.invoke(c, noArgArray); for (Enumeration e = invs.elements(); e.hasMoreElements(); inv_conds.addElement(e.nextElement())) { } @@ -563,20 +563,20 @@ for (Enumeration e = invs_s.elements(); e.hasMoreElements(); inv_source.addElement(e.nextElement())) { } } catch (InvocationTargetException e) { - log.error("iContract: WARNING: while instrumenting invariants in class " + getSignature() + " execution of\n" + repositoryName + "::" + "__iContract__getInvariantList" + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE INVARIANTS OF " + superclassName + " ARE IGNORED !"); + log.error("Java Contract Suite: WARNING: while instrumenting invariants in class " + getSignature() + " execution of\n" + repositoryName + "::" + "__JContractS__getInvariantList" + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE INVARIANTS OF " + superclassName + " ARE IGNORED !"); } catch (IllegalArgumentException e) { - log.error("iContract: WARNING: while instrumenting invariants in class " + getSignature() + " execution of\n" + repositoryName + "::" + "__iContract__getInvariantList" + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE INVARIANTS OF " + superclassName + " ARE IGNORED !"); + log.error("Java Contract Suite: WARNING: while instrumenting invariants in class " + getSignature() + " execution of\n" + repositoryName + "::" + "__JContractS__getInvariantList" + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE INVARIANTS OF " + superclassName + " ARE IGNORED !"); } catch (IllegalAccessException e) { - log.error("iContract: WARNING: while instrumenting invariants in class " + getSignature() + " execution of\n" + repositoryName + "::" + "__iContract__getInvariantList" + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE INVARIANTS OF " + superclassName + " ARE IGNORED !"); + log.error("Java Contract Suite: WARNING: while instrumenting invariants in class " + getSignature() + " execution of\n" + repositoryName + "::" + "__JContractS__getInvariantList" + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE INVARIANTS OF " + superclassName + " ARE IGNORED !"); } } catch (NoSuchMethodException _ex) { } } catch (ClassNotFoundException e) { if (!superclassName.startsWith("java.")) { - log.error(getLocationDescription() + "icontract: WARNING: " + getSignature() + " will be instrumented with it's own invariants ONLY -- this is because the superclass of " + getSignature() + " (" + superclassName + ") may" + " either not have been " + "instrumented for invariants (or the repository file " + repositoryName + ".class is missing, e.g. was not compiled) !\n" + "[caught exception: " + e + "]"); + log.error(getLocationDescription() + "Java Contract Suite: WARNING: " + getSignature() + " will be instrumented with it's own invariants ONLY -- this is because the superclass of " + getSignature() + " (" + superclassName + ") may" + " either not have been " + "instrumented for invariants (or the repository file " + repositoryName + ".class is missing, e.g. was not compiled) !\n" + "[caught exception: " + e + "]"); } } } @@ -620,7 +620,7 @@ inst_var_decl = inst_var_decl + "// Stores bookkeeping information -- key: thread, value: call level\n"; boolean do_not_enforce_precompilation_of_source = Boolean.getBoolean("jcontracts.internal.do_not_enforce_precompilation_of_source"); if (do_not_enforce_precompilation_of_source) { - System.err.println("iContract:SWITCH:jcontracts.internal.do_not_enforce_precompilation_of_source=true"); + System.err.println("Java Contract Suite:SWITCH:jcontracts.internal.do_not_enforce_precompilation_of_source=true"); } boolean icl_already_defined = false; if (!do_not_enforce_precompilation_of_source) { @@ -628,11 +628,11 @@ icl_already_defined = checkIfFieldExistsInSuperclassClosure(java.lang.Class.forName(getName()), "__icl_"); } catch (ClassNotFoundException _ex) { - throw new RuntimeException(getLocationDescription() + "iContract:ERROR: could not find " + getName() + ". Please compile the sourcefile, see -j option (net.sf.jcontracts.net.sf.jcontracts.iContract needs the compiled file to determine whether or not to create invariant bookkeeping variables (__icl_)). Exiting iContract.", _ex); + throw new RuntimeException(getLocationDescription() + "Java Contract Suite: ERROR: could not find " + getName() + ". Please compile the sourcefile, see -j option (Java Contract Suite needs the compiled file to determine whether or not to create invariant bookkeeping variables (__icl_)). Exiting Java Contract Suite.", _ex); } } if (do_not_enforce_precompilation_of_source) { - System.err.println("iContract:SWITCH:invariant bookkeeping may NOT work correctly because the check for the existence of the __icl_ variable in superclasses was disables. This means that there is an __icl_ varaible at each level of the inheritance rather than one and one only per inheritance chain! THIS IS ONLY SUITABLE FOR CERTAIN SPECIAL TESTCASES. REMOVE the 'java -Djcontracts.internal.do_not_enforce_precompilation_of_source' property to make net.sf.jcontracts.net.sf.jcontracts.iContract work in normal (correct) mode!"); + System.err.println("Java Contract Suite: SWITCH:invariant bookkeeping may NOT work correctly because the check for the existence of the __icl_ variable in superclasses was disables. This means that there is an __icl_ varaible at each level of the inheritance rather than one and one only per inheritance chain! THIS IS ONLY SUITABLE FOR CERTAIN SPECIAL TESTCASES. REMOVE the 'java -Djcontracts.internal.do_not_enforce_precompilation_of_source' property to make Java Contract Suite work in normal (correct) mode!"); } if (!icl_already_defined) { inst_var_decl = inst_var_decl + "protected transient java.util.Hashtable __icl_ = new java.util.Hashtable(1);\n"; @@ -980,18 +980,18 @@ last_type = "<<unknown-type " + last_type + "::" + section + ">>"; log.debug("getTypeOfValue:last_type=" + last_type); stop = true; - throw new UnableToDetermineTypeException(getLocationDescription() + "::iContract:error: could not infere the type of (" + last_type + "::" + section + ") as the class " + last_type + " is not in the local not in any of the imported packages. Occured in " + this + "\n"); + throw new UnableToDetermineTypeException(getLocationDescription() + "::Java Contract Suite: ERROR: could not infere the type of (" + last_type + "::" + section + ") as the class " + last_type + " is not in the local not in any of the imported packages. Occured in " + this + "\n"); } } catch (NoSuchMethodException _ex) { - throw new UnableToDetermineTypeException("iContract:error: method " + last_type + "." + pure_function_name + "(" + sig + ") not found via reflection !\n"); + throw new UnableToDetermineTypeException("Java Contract Suite: ERROR: method " + last_type + "." + pure_function_name + "(" + sig + ") not found via reflection !\n"); } } catch (ClassNotFoundException _ex) { last_type = "<<unknown-type " + last_type + "::" + section + " (class " + last_type + " not found. Occured in " + this + ")>>"; log.debug("getTypeOfValue:last_type=" + last_type); stop = true; - throw new UnableToDetermineTypeException(getLocationDescription() + "::iContract:error: could not infere the type of (" + last_type + "::" + section + ") as the class " + last_type + " is not in the local not in any of the imported packages. Occured in " + this + "\n"); + throw new UnableToDetermineTypeException(getLocationDescription() + "::Java Contract Suite: ERROR: could not infere the type of (" + last_type + "::" + section + ") as the class " + last_type + " is not in the local not in any of the imported packages. Occured in " + this + "\n"); } } } @@ -1100,14 +1100,14 @@ } } catch (NoSuchMethodException _ex) { - throw new UnableToDetermineTypeException("iContract:error: method " + last_type + "." + pure_function_name + "(" + sig + ") not found via reflection !\n"); + throw new UnableToDetermineTypeException("Java Contract Suite: ERROR: method " + last_type + "." + pure_function_name + "(" + sig + ") not found via reflection !\n"); } } catch (ClassNotFoundException _ex) { last_type = "<<unknown-type " + last_type + "::" + section + " (class " + last_type + " not found. Occured in " + this + ")>>"; log.debug("getTypeOfValue:last_type=" + last_type); stop = true; - throw new UnableToDetermineTypeException(getLocationDescription() + "::iContract:error: could not infere the type of (" + last_type + "::" + section + ") as the class " + last_type + " is not in the local not in any of the imported packages. Occured in " + this + "\n"); + throw new UnableToDetermineTypeException(getLocationDescription() + "::Java Contract Suite: ERROR: could not infere the type of (" + last_type + "::" + section + ") as the class " + last_type + " is not in the local not in any of the imported packages. Occured in " + this + "\n"); } } current_pos = next_dot_pos + 1; @@ -1142,27 +1142,27 @@ java.lang.Class c = java.lang.Class.forName(repositoryName); java.lang.Class noArgArray[] = new java.lang.Class[0]; try { - Method theIGMethod = c.getMethod("__iContract__getInvariantList", noArgArray); - c.getMethod("__iContract__getInvariantSourceList", noArgArray); + Method theIGMethod = c.getMethod("__JContractS__getInvariantList", noArgArray); + c.getMethod("__JContractS__getInvariantSourceList", noArgArray); try { Vector invs = (Vector)theIGMethod.invoke(c, noArgArray); for (Enumeration e = invs.elements(); e.hasMoreElements(); inv_conds.addElement(e.nextElement())) { } } catch (InvocationTargetException e) { - log.error("iContract: WARNING: while instrumenting invariants in class " + getSignature() + " execution of\n" + repositoryName + "::" + "__iContract__getInvariantList" + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE INVARIANTS OF " + superclassName + " ARE IGNORED !"); + log.error("Java Contract Suite: WARNING: while instrumenting invariants in class " + getSignature() + " execution of\n" + repositoryName + "::" + "__JContractS__getInvariantList" + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE INVARIANTS OF " + superclassName + " ARE IGNORED !"); } catch (IllegalArgumentException e) { - log.error("iContract: WARNING: while instrumenting invariants in class " + getSignature() + " execution of\n" + repositoryName + "::" + "__iContract__getInvariantList" + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE INVARIANTS OF " + superclassName + " ARE IGNORED !"); + log.error("Java Contract Suite: WARNING: while instrumenting invariants in class " + getSignature() + " execution of\n" + repositoryName + "::" + "__JContractS__getInvariantList" + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE INVARIANTS OF " + superclassName + " ARE IGNORED !"); } catch (IllegalAccessException e) { - log.error("iContract: WARNING: while instrumenting invariants in class " + getSignature() + " execution of\n" + repositoryName + "::" + "__iContract__getInvariantList" + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE INVARIANTS OF " + superclassName + " ARE IGNORED !"); + log.error("Java Contract Suite: WARNING: while instrumenting invariants in class " + getSignature() + " execution of\n" + repositoryName + "::" + "__JContractS__getInvariantList" + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE INVARIANTS OF " + superclassName + " ARE IGNORED !"); } } catch (NoSuchMethodException _ex) { } } catch (ClassNotFoundException e) { if (!superclassName.startsWith("java.")) { - log.error(getLocationDescription() + "icontract: WARNING: " + getSignature() + " will be instrumented with it's own invariants ONLY -- this is because the superclass of " + getSignature() + " (" + superclassName + ") may" + " either not have been " + "instrumented for invariants (or the repository file " + repositoryName + ".class is missing, e.g. was not compiled) !\n" + "[caught exception: " + e + "]"); + log.error(getLocationDescription() + "Java Contract Suite: WARNING: " + getSignature() + " will be instrumented with it's own invariants ONLY -- this is because the superclass of " + getSignature() + " (" + superclassName + ") may" + " either not have been " + "instrumented for invariants (or the repository file " + repositoryName + ".class is missing, e.g. was not compiled) !\n" + "[caught exception: " + e + "]"); } } } @@ -1256,7 +1256,7 @@ java.lang.Class c = java.lang.Class.forName(className); java.lang.Class noArgArray[] = new java.lang.Class[0]; try { - Method theIGMethod = c.getMethod("__iContract__getInvariantList", noArgArray); + Method theIGMethod = c.getMethod("__JContractS__getInvariantList", noArgArray); try { Vector _tmp = (Vector)theIGMethod.invoke(c, noArgArray); res = true; Modified: trunk/source/java/net/sf/jcontracts/icontract/CompilerOption.java =================================================================== --- trunk/source/java/net/sf/jcontracts/icontract/CompilerOption.java 2006-11-23 17:23:27 UTC (rev 17) +++ trunk/source/java/net/sf/jcontracts/icontract/CompilerOption.java 2006-11-24 07:36:06 UTC (rev 18) @@ -64,7 +64,7 @@ Main theCompiler = new Main(javacout, ""); result = theCompiler.compile(fargs); if (!result) { - System.err.println("\niContract: error: compilation failed " + javacout.toString()); + System.err.println("\nJava Contract Suite: ERROR: compilation failed " + javacout.toString()); } } catch (NoClassDefFoundError _ex) { @@ -103,17 +103,17 @@ outmsg.append(" <could not open out stream of compiler!>"); } if (child.waitFor() != 0) { - System.err.println("\niContract: error: compilation failed(error code: " + child.exitValue() + ") " + errmsg.toString() + " " + outmsg.toString()); + System.err.println("\nJava Contract Suite: ERROR: compilation failed(error code: " + child.exitValue() + ") " + errmsg.toString() + " " + outmsg.toString()); result = false; } } catch (InterruptedException _ex) { result = false; - System.err.println("\niContract: error: compilation failed."); + System.err.println("\nJava Contract Suite: ERROR: compilation failed."); } catch (IOException _ex) { result = false; - System.err.println("\niContract: error: compilation failed."); + System.err.println("\nJava Contract Suite: ERROR: compilation failed."); } } if (!result) { Modified: trunk/source/java/net/sf/jcontracts/icontract/FileTarget.java =================================================================== --- trunk/source/java/net/sf/jcontracts/icontract/FileTarget.java 2006-11-23 17:23:27 UTC (rev 17) +++ trunk/source/java/net/sf/jcontracts/icontract/FileTarget.java 2006-11-24 07:36:06 UTC (rev 18) @@ -82,7 +82,7 @@ String fn = getName().substring(1, getName().length()); File file = new File(fn); if (!file.exists()) { - throw new RuntimeException("iContract: error file " + fn + " not found!"); + throw new RuntimeException("Java Contract Suite: error file " + fn + " not found!"); } try { BufferedReader f = new BufferedReader(new FileReader(fn)); @@ -157,7 +157,7 @@ } if (cleanOption != null) { - System.err.println("iContract: -r option enabled -- create a file " + getName() + ".clean" + " with all instrumentation code from previous run removed. Also the cleaned file will be the input to the new instrumentation run."); + System.err.println("Java Contract Suite: -r option enabled -- create a file " + getName() + ".clean" + " with all instrumentation code from previous run removed. Also the cleaned file will be the input to the new instrumentation run."); is = createStreamForCodeParsing(); } else { is = new FileInputStream(getName()); Modified: trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java =================================================================== --- trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java 2006-11-23 17:23:27 UTC (rev 17) +++ trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java 2006-11-24 07:36:06 UTC (rev 18) @@ -6,7 +6,7 @@ public class HelpOption extends ParameterOption { - public static final String VERSION = "for JDK 1.5, iContract v2.0"; + public static final String VERSION = "for JDK 1.5, Java Contract Suite v1.01.00b02-dev"; public static final String NAME = "h"; public HelpOption(String name, Vector arguments) { @@ -14,7 +14,7 @@ } protected void activateOnTargets(Vector targets) { - System.out.println("NAME: iContract, Version " + VERSION); + System.out.println("NAME: Java Contract Suite, Version " + VERSION); System.out.println("AUTHOR: Copyright (C), 1997,98,99 Reto Kramer <in...@re...>"); System.out.println("SYNOPSIS: java net.sf.jcontracts.icontract.Tool {option} {file}"); System.out.println("DESCRIPTION: Provides Java with full support for \"Design by Contract\"."); @@ -22,14 +22,14 @@ System.out.println(" - method pre- and post-conditions"); System.out.println(" - class/interface invariants"); System.out.println(" based on comments in the code (@pre, @post, @invariant)."); - System.out.println(" net.sf.jcontracts.net.sf.jcontracts.iContract operates on classes, interfaces, and methods."); + System.out.println(" Java Contract Suite operates on classes, interfaces, and methods."); System.out.println(" file: Is a list of java sourcecode files (space separated)."); System.out.println(" If a name of the form @file is in the list, each line in file"); System.out.println(" is interpreted as a filename."); System.out.println(" If a name is a pattern (e.g. ./x/*.java), all files in x and"); System.out.println(" subdirectories thereof are searched for *.java files."); - System.out.println(" {option}: Is a list of options, net.sf.jcontracts.net.sf.jcontracts.iContract accepts the following options:"); - System.out.println(" (if no option is given, net.sf.jcontracts.net.sf.jcontracts.iContract uses the -h option)"); + System.out.println(" {option}: Is a list of options, Java Contract Suite accepts the following options:"); + System.out.println(" (if no option is given, Java Contract Suite uses the -h option)"); System.out.println(""); System.out.println(" GENERAL:"); System.out.println(" -h prints version, synopsis and a brief description."); Modified: trunk/source/java/net/sf/jcontracts/icontract/Interface.java =================================================================== --- trunk/source/java/net/sf/jcontracts/icontract/Interface.java 2006-11-23 17:23:27 UTC (rev 17) +++ trunk/source/java/net/sf/jcontracts/icontract/Interface.java 2006-11-24 07:36:06 UTC (rev 18) @@ -14,8 +14,8 @@ implements PrePostCheck, InvCheck { private static final Logger log = Logger.getLogger(Interface.class); public static final String REP_PREFIX = "__REP_"; - private static final String INV_GET_METHOD = "__iContract__getInvariantList"; - private static final String INV_SO_GET_METHOD = "__iContract__getInvariantSourceList"; + private static final String INV_GET_METHOD = " __JContractS__getInvariantList"; + private static final String INV_SO_GET_METHOD = " __JContractS__getInvariantSourceList"; private static final String INVARIANT_TAG_NAME = "invariant"; public Interface(String name, String filename, int line_number) { @@ -185,7 +185,7 @@ } } if (sig.length > 4) { - throw new RuntimeException("iContract:error: more than 4 arguments (" + f + ") not supported at the moment [991]. Easy to be added though."); + throw new RuntimeException("Java Contract Suite: ERROR: more than 4 arguments (" + f + ") not supported at the moment [991]. Easy to be added though."); } else { return m; } @@ -265,7 +265,7 @@ if (isStatic()) { if (inv_conds.size() != 0) { - log.warn(getLocationDescription() + "icontract: WARNING: the invariants (" + inv_conds + ") associated with the static interface " + getSignature() + " will not be enforced (not instrumented and no repository entry) due to the static modifier!"); + log.warn(getLocationDescription() + "Java Contract Suite: WARNING: the invariants (" + inv_conds + ") associated with the static interface " + getSignature() + " will not be enforced (not instrumented and no repository entry) due to the static modifier!"); } return ""; } @@ -285,7 +285,7 @@ repositoryName = repositoryName + superclassName.substring(superclassName.lastIndexOf(".") + 1, superclassName.length()); } if (repositoryForInvExists(repositoryName)) { - body = body + " super_vec = " + repositoryName + "." + "__iContract__getInvariantList" + "();\n"; + body = body + " super_vec = " + repositoryName + "." + " __JContractS__getInvariantList" + "();\n"; body = body + " for (Enumeration e = super_vec.elements(); e.hasMoreElements(); ) {\n"; body = body + " vec.addElement( e.nextElement() );\n"; body = body + " }\n"; @@ -293,7 +293,7 @@ body = body + " // Repository for super-interface " + superclassName + " (" + repositoryName + ") "; body = body + "does not exist or is not accessible (the total set of super-interfaces of " + getSignature() + "is " + super_interfaces + ").\n"; if (!superclassName.startsWith("java.")) { - log.error(getLocationDescription() + "icontract: WARNING: the repository of " + getSignature() + " will not contain invariants of one of its super-interfaces " + superclassName + " (total set of super-interfaces is " + super_interfaces + "). This may be because the super-interface " + superclassName + " may" + " not have been " + "instrumented for invariants (or the repository file " + repositoryName + ".class is missing, e.g. was not compiled) !\n"); + log.error(getLocationDescription() + "Java Contract Suite: WARNING: the repository of " + getSignature() + " will not contain invariants of one of its super-interfaces " + superclassName + " (total set of super-interfaces is " + super_interfaces + "). This may be because the super-interface " + superclassName + " may" + " not have been " + "instrumented for invariants (or the repository file " + repositoryName + ".class is missing, e.g. was not compiled) !\n"); } } } @@ -316,7 +316,7 @@ } String header = " /**This repository method captures the invariants of\n * interface " + getSignature() + " and it's super-interfaces " + super_interfaces + ".\n"; header = header + " */\n"; - header = header + " public static final Vector __iContract__getInvariantList() {"; + header = header + " public static final Vector __JContractS__getInvariantList() {"; String code = header + "\n Vector vec = new Vector();\n" + body + " return vec;\n" + " }\n"; body = ""; if (super_interfaces.size() != 0) { @@ -332,7 +332,7 @@ repositoryName = repositoryName + superclassName.substring(superclassName.lastIndexOf(".") + 1, superclassName.length()); } if (repositoryForInvExists(repositoryName)) { - body = body + " super_vec = " + repositoryName + "." + "__iContract__getInvariantSourceList" + "();\n"; + body = body + " super_vec = " + repositoryName + "." + " __JContractS__getInvariantSourceList" + "();\n"; body = body + " for (Enumeration e = super_vec.elements(); e.hasMoreElements(); ) {\n"; body = body + " vec.addElement( e.nextElement() );\n"; body = body + " }\n"; @@ -360,7 +360,7 @@ } header = " /**This repository method captures the source of invariants of\n * interface " + getSignature() + " and it's super-interfaces " + super_interfaces + ".\n"; header = header + " */\n"; - header = header + " public static final Vector __iContract__getInvariantSourceList() {"; + header = header + " public static final Vector __JContractS__getInvariantSourceList() {"; code = code + "\n" + header + "\n Vector vec = new Vector();\n" + body + " return vec;\n" + " }\n"; return code; } @@ -399,7 +399,7 @@ } } - System.err.println(getLocationDescription() + "iContract:WARNING: could not find " + ": " + short_name); + System.err.println(getLocationDescription() + "Java Contract Suite: WARNING: could not find " + ": " + short_name); return short_name; } @@ -549,18 +549,18 @@ last_type = "<<unknown-type " + last_type + "::" + section + ">>"; log.debug("getTypeOfValue:last_type=" + last_type); stop = true; - throw new UnableToDetermineTypeException(getLocationDescription() + "::iContract:error: could not infere the type of (" + last_type + "::" + section + ") as the class " + last_type + " is not in the local not in any of the imported packages. Occured in " + this + "\n"); + throw new UnableToDetermineTypeException(getLocationDescription() + "::Java Contract Suite: ERROR: could not infere the type of (" + last_type + "::" + section + ") as the class " + last_type + " is not in the local not in any of the imported packages. Occured in " + this + "\n"); } } catch (NoSuchMethodException _ex) { - throw new UnableToDetermineTypeException("iContract:error: method " + last_type + "." + pure_function_name + "(" + sig + ") not found via reflection !\n"); + throw new UnableToDetermineTypeException("Java Contract Suite: ERROR: method " + last_type + "." + pure_function_name + "(" + sig + ") not found via reflection !\n"); } } catch (ClassNotFoundException _ex) { last_type = "<<unknown-type " + last_type + "::" + section + " (class " + last_type + " not found. Occured in " + this + ")>>"; log.debug("getTypeOfValue:last_type=" + last_type); stop = true; - throw new UnableToDetermineTypeException(getLocationDescription() + "::iContract:error: could not infere the type of (" + last_type + "::" + section + ") as the class " + last_type + " is not in the local not in any of the imported packages. Occured in " + this + "\n"); + throw new UnableToDetermineTypeException(getLocationDescription() + "::Java Contract Suite: ERROR: could not infere the type of (" + last_type + "::" + section + ") as the class " + last_type + " is not in the local not in any of the imported packages. Occured in " + this + "\n"); } } } @@ -669,14 +669,14 @@ } } catch (NoSuchMethodException _ex) { - throw new UnableToDetermineTypeException("iContract:error: method " + last_type + "." + pure_function_name + "(" + sig + ") not found via reflection !\n"); + throw new UnableToDetermineTypeException("Java Contract Suite: ERROR: method " + last_type + "." + pure_function_name + "(" + sig + ") not found via reflection !\n"); } } catch (ClassNotFoundException _ex) { last_type = "<<unknown-type " + last_type + "::" + section + " (class " + last_type + " not found. Occured in " + this + ")>>"; log.debug("getTypeOfValue:last_type=" + last_type); stop = true; - throw new UnableToDetermineTypeException(getLocationDescription() + "::iContract:error: could not infere the type of (" + last_type + "::" + section + ") as the class " + last_type + " is not in the local not in any of the imported packages. Occured in " + this + "\n"); + throw new UnableToDetermineTypeException(getLocationDescription() + "::Java Contract Suite: ERROR: could not infere the type of (" + last_type + "::" + section + ") as the class " + last_type + " is not in the local not in any of the imported packages. Occured in " + this + "\n"); } } current_pos = next_dot_pos + 1; @@ -722,7 +722,7 @@ java.lang.Class c = java.lang.Class.forName(className); java.lang.Class noArgArray[] = new java.lang.Class[0]; try { - Method theIGMethod = c.getMethod("__iContract__getInvariantList", noArgArray); + Method theIGMethod = c.getMethod(" __JContractS__getInvariantList", noArgArray); try { Vector _tmp = (Vector)theIGMethod.invoke(c, noArgArray); res = true; Modified: trunk/source/java/net/sf/jcontracts/icontract/MergeOption.java =================================================================== --- trunk/source/java/net/sf/jcontracts/icontract/MergeOption.java 2006-11-23 17:23:27 UTC (rev 17) +++ trunk/source/java/net/sf/jcontracts/icontract/MergeOption.java 2006-11-24 07:36:06 UTC (rev 18) @@ -232,7 +232,7 @@ repOutputDirectory = repOutputDirectory + File.separator; } else { if (!outputOption.hasParameter()) { - throw new RuntimeException("icontract:error: repository output directory option (-k) requires directory F (e.g. -kF) [note F may also be @p which will be substituted for with the path of the source file]."); + throw new RuntimeException("Java Contract Suite: ERROR: repository output directory option (-k) requires directory F (e.g. -kF) [note F may also be @p which will be substituted for with the path of the source file]."); } String pattern = (String)repOutputOption.getArguments().firstElement(); if (pattern.indexOf("@f") != -1 || pattern.indexOf("@e") != -1) { @@ -271,7 +271,7 @@ String fn = entry.substring(1, entry.length()); File file = new File(fn); if (!file.exists()) { - throw new RuntimeException("iContract: error file " + fn + " not found !"); + throw new RuntimeException("Java Contract Suite: error file " + fn + " not found !"); } try { BufferedReader f = new BufferedReader(new FileReader(fn)); @@ -295,7 +295,7 @@ output_file = new PrintWriter(System.out); } else { if (!outputOption.hasParameter()) { - throw new RuntimeException("icontract:error: output option (-o) requires filename (e.g. -oFile.java)."); + throw new RuntimeException("Java Contract Suite: ERROR: output option (-o) requires filename (e.g. -oFile.java)."); } String fon = ""; if (cmc instanceof TypeMetaclass) { @@ -368,7 +368,7 @@ } } else { - System.err.println(type.getLocationDescription() + "icontract: WARNING: contract-checks (invariant) will NOT be instrumented for (local/anonymous class) " + type.getSignature() + " [this version of the tool does not support the instrumentation of methods in local and anonymous classes]"); + System.err.println(type.getLocationDescription() + "Java Contract Suite: WARNING: contract-checks (invariant) will NOT be instrumented for (local/anonymous class) " + type.getSignature() + " [this version of the tool does not support the instrumentation of methods in local and anonymous classes]"); } } PrePostCheck prepost_element = (PrePostCheck)annotations.elementAt(i); @@ -378,7 +378,7 @@ boolean do_instr = true; if (method.getParent() != null && ((TypeMetaclass)method.getParent()).isLocal()) { do_instr = false; - System.err.println(method.getLocationDescription() + "icontract: WARNING: contract-checks (pre,post) will NOT be instrumented for (method in local/anonymous class) " + method.getParent().getSignature() + "::" + method.getSignature() + " [this version of the tool does not support the instrumentation of methods in local and anonymous classes]"); + System.err.println(method.getLocationDescription() + "Java Contract Suite: WARNING: contract-checks (pre,post) will NOT be instrumented for (method in local/anonymous class) " + method.getParent().getSignature() + "::" + method.getSignature() + " [this version of the tool does not support the instrumentation of methods in local and anonymous classes]"); } if (do_instr) { if (method.hasBody()) { @@ -415,14 +415,14 @@ input_file.close(); } if (e.getMessage() != null) { - System.err.println("icontract:error: i/o-problem: " + e.getMessage()); + System.err.println("Java Contract Suite: ERROR: i/o-problem: " + e.getMessage()); } else { - System.err.println("icontract:error: i/o-problem: " + e); + System.err.println("Java Contract Suite: ERROR: i/o-problem: " + e); } throw e; } } else { - System.out.println("icontract: warning: no code to generate"); + System.out.println("Java Contract Suite: WARNING: no code to generate"); } return fileList; } @@ -433,7 +433,7 @@ for (Enumeration e = controlTable.elements(); !stop && e.hasMoreElements();) { String patternline = (String)e.nextElement(); if (patternline.indexOf(' ') == -1) { - throw new RuntimeException("iContract:error malformed -m config file entry: \"" + patternline + "\" missing a space character that separates the <package><type><method> from the list of pre,post and inv switches (e.g. \"net.sf.jcontracts.icontract.Tool<SPACE>pre\" enables pre)"); + throw new RuntimeException("Java Contract Suite:error malformed -m config file entry: \"" + patternline + "\" missing a space character that separates the <package><type><method> from the list of pre,post and inv switches (e.g. \"net.sf.jcontracts.icontract.Tool<SPACE>pre\" enables pre)"); } String pattern = patternline.substring(0, patternline.indexOf(' ')); if (match(item, pattern)) { Modified: trunk/source/java/net/sf/jcontracts/icontract/Method.java =================================================================== --- trunk/source/java/net/sf/jcontracts/icontract/Method.java 2006-11-23 17:23:27 UTC (rev 17) +++ trunk/source/java/net/sf/jcontracts/icontract/Method.java 2006-11-24 07:36:06 UTC (rev 18) @@ -18,8 +18,8 @@ private static final String POSTCONDITION_TAG_NAME_1 = "post"; private static final String POSTCONDITION_TAG_NAME_2 = "ensure"; public static final String REP_PREFIX = "__REP_"; - private static final String PRE_GET_METHOD = "__iContract__getPreList"; - private static final String POST_GET_METHOD = "__iContract__getPostList"; + private static final String PRE_GET_METHOD = " __JContractS__getPreList"; + private static final String POST_GET_METHOD = " __JContractS__getPostList"; private static final char EXCEPTION_CLASS_MARKER = 35; public static final String RETURN_VALUE_HOLDER_NAME = "__return_value_holder_"; private static final String START_SEPARATION_STRING = "//#*#-------------------------------------------------------------------------------"; @@ -57,7 +57,7 @@ java.lang.Class c = java.lang.Class.forName(repositoryName); java.lang.Class noArgArray[] = new java.lang.Class[0]; try { - java.lang.reflect.Method thePGMethod = c.getMethod(mangleExpression("__iContract__getPostList_" + getSignature()), noArgArray); + java.lang.reflect.Method thePGMethod = c.getMethod(mangleExpression(" __JContractS__getPostList_" + getSignature()), noArgArray); try { Vector posts = (Vector)thePGMethod.invoke(c, noArgArray); String arr[]; @@ -68,13 +68,13 @@ } catch (InvocationTargetException e) { - log.error("iContract: WARNING: while instrumenting postconditions in method " + getParent().getSignature() + "::" + getSignature() + " execution of\n" + mangleExpression("__iContract__getPostList_" + getSignature()) + "()\n" + "failed, throwing exception:\n" + e + " target-exception: " + e.getTargetException() + "\nTHEREFORE POSTCONDITIONS OF " + superclassName + "::" + getSignature() + " ARE IGNORED !"); + log.error("Java Contract Suite: WARNING: while instrumenting postconditions in method " + getParent().getSignature() + "::" + getSignature() + " execution of\n" + mangleExpression(" __JContractS__getPostList_" + getSignature()) + "()\n" + "failed, throwing exception:\n" + e + " target-exception: " + e.getTargetException() + "\nTHEREFORE POSTCONDITIONS OF " + superclassName + "::" + getSignature() + " ARE IGNORED !"); } catch (IllegalArgumentException e) { - log.error("iContract: WARNING: while instrumenting postconditions in method " + getParent().getSignature() + "::" + getSignature() + " execution of\n" + mangleExpression("__iContract__getPostList_" + getSignature()) + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE POSTCONDITIONS OF " + superclassName + "::" + getSignature() + " ARE IGNORED !"); + log.error("Java Contract Suite: WARNING: while instrumenting postconditions in method " + getParent().getSignature() + "::" + getSignature() + " execution of\n" + mangleExpression(" __JContractS__getPostList_" + getSignature()) + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE POSTCONDITIONS OF " + superclassName + "::" + getSignature() + " ARE IGNORED !"); } catch (IllegalAccessException e) { - log.error("iContract: WARNING: while instrumenting postconditions in method " + getParent().getSignature() + "::" + getSignature() + " execution of\n" + mangleExpression("__iContract__getPostList_" + getSignature()) + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE POSTCONDITIONS OF " + superclassName + "::" + getSignature() + " ARE IGNORED !"); + log.error("Java Contract Suite: WARNING: while instrumenting postconditions in method " + getParent().getSignature() + "::" + getSignature() + " execution of\n" + mangleExpression(" __JContractS__getPostList_" + getSignature()) + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE POSTCONDITIONS OF " + superclassName + "::" + getSignature() + " ARE IGNORED !"); } } catch (NoSuchMethodException _ex) { } @@ -114,7 +114,7 @@ java.lang.Class c = java.lang.Class.forName(repositoryName); java.lang.Class noArgArray[] = new java.lang.Class[0]; try { - java.lang.reflect.Method thePGMethod = c.getMethod(mangleExpression("__iContract__getPreList_" + getSignature()), noArgArray); + java.lang.reflect.Method thePGMethod = c.getMethod(mangleExpression(" __JContractS__getPreList_" + getSignature()), noArgArray); try { Vector pres = (Vector)thePGMethod.invoke(c, noArgArray); String arr[]; @@ -125,13 +125,13 @@ } catch (InvocationTargetException e) { - log.warn("iContract: WARNING: while instrumenting preconditions in method " + getParent().getSignature() + "::" + getSignature() + " execution of\n" + mangleExpression("__iContract__getPreList_" + getSignature()) + "()\n" + "failed, throwing exception:\n" + e + " target-exception: " + e.getTargetException() + "\nTHEREFORE PRECONDITIONS OF " + superclassName + "::" + getSignature() + " ARE IGNORED !"); + log.warn("Java Contract Suite: WARNING: while instrumenting preconditions in method " + getParent().getSignature() + "::" + getSignature() + " execution of\n" + mangleExpression(" __JContractS__getPreList_" + getSignature()) + "()\n" + "failed, throwing exception:\n" + e + " target-exception: " + e.getTargetException() + "\nTHEREFORE PRECONDITIONS OF " + superclassName + "::" + getSignature() + " ARE IGNORED !"); } catch (IllegalArgumentException e) { - log.warn("iContract: WARNING: while instrumenting preconditions in method " + getParent().getSignature() + "::" + getSignature() + " execution of\n" + mangleExpression("__iContract__getPreList_" + getSignature()) + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE PRECONDITIONS OF " + superclassName + "::" + getSignature() + " ARE IGNORED !"); + log.warn("Java Contract Suite: WARNING: while instrumenting preconditions in method " + getParent().getSignature() + "::" + getSignature() + " execution of\n" + mangleExpression(" __JContractS__getPreList_" + getSignature()) + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE PRECONDITIONS OF " + superclassName + "::" + getSignature() + " ARE IGNORED !"); } catch (IllegalAccessException e) { - log.warn("iContract: WARNING: while instrumenting preconditions in method " + getParent().getSignature() + "::" + getSignature() + " execution of\n" + mangleExpression("__iContract__getPreList_" + getSignature()) + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE PRECONDITIONS OF " + superclassName + "::" + getSignature() + " ARE IGNORED !"); + log.warn("Java Contract Suite: WARNING: while instrumenting preconditions in method " + getParent().getSignature() + "::" + getSignature() + " execution of\n" + mangleExpression(" __JContractS__getPreList_" + getSignature()) + "()\n" + "failed, throwing exception:\n" + e + "\nTHEREFORE PRECONDITIONS OF " + superclassName + "::" + getSignature() + " ARE IGNORED !"); } } catch (NoSuchMethodException _ex) { } @@ -233,7 +233,7 @@ } catch (ClassNotFoundException e) { - log.warn(getLocationDescription() + "iContract:WARNING: while instrumenting postconditions in method " + getParent().getSignature() + "::" + getSignature() + " an attempt was made to determine if " + className + " implements interface 'java.lang.Cloneable'" + " in order to decide if the 'ExprOfType-" + className + "@pre' that appears in the " + "postcondition should use 'copy' or 'reference' semantics." + " Unfortunately " + className + " could not be found " + "(exception: " + e + "). THEREFORE REFERENCE SEMANTICS WILL HAVE TO BE USED!"); + log.warn(getLocationDescription() + "Java Contract Suite: WARNING: while instrumenting postconditions in method " + getParent().getSignature() + "::" + getSignature() + " an attempt was made to determine if " + className + " implements interface 'java.lang.Cloneable'" + " in order to decide if the 'ExprOfType-" + className + "@pre' that appears in the " + "postcondition should use 'copy' or 'reference' semantics." + " Unfortunately " + className + " could not be found " + "(exception: " + e + "). THEREFORE REFERENCE SEMANTICS WILL HAVE TO BE USED!"); res = false; } } @@ -387,14 +387,14 @@ } } if (sig.length > 4) { - throw new RuntimeException("iContract:error: more than 4 arguments (" + f + ") not supported at the moment [991]. Easy to be added though."); + throw new RuntimeException("Java Contract Suite: ERROR: more than 4 arguments (" + f + ") not supported at the moment [991]. Easy to be added though."); } else { return m; } } public Vector getAllNonImplementedMethods() { - throw new RuntimeException("iContract.Method.getAllNonImplementedMethods() not expected to be called here!"); + throw new RuntimeException("Method.getAllNonImplementedMethods() not expected to be called here!"); } Vector getAllOldValues(String expr) { @@ -540,8 +540,8 @@ repositoryName = repositoryName + superclassName.substring(superclassName.lastIndexOf(".") + 1, superclassName.length()); } if (repositoryExists(repositoryName)) { - if (repositoryEntryForPostExists(repositoryName, "__iContract__getPostList_" + getSignature())) { - body = body + " super_vec = " + repositoryName + "." + mangleExpression("__iContract__getPostList_" + getSignature()) + "();\n"; + if (repositoryEntryForPostExists(repositoryName, " __JContractS__getPostList_" + getSignature())) { + body = body + " super_vec = " + repositoryName + "." + mangleExpression(" __JContractS__getPostList_" + getSignature()) + "();\n"; body = body + " for (Enumeration e = super_vec.elements(); e.hasMoreElements(); ) {\n"; body = body + " vec.addElement( e.nextElement() );\n"; body = body + " }\n"; @@ -584,7 +584,7 @@ header = header + " and it's superclass method " + superclassName + "::" + getSignature() + ".\n"; } header = header + " */\n"; - header = header + " public static final Vector " + mangleExpression("__iContract__getPostList_" + getSignature()) + "() {"; + header = header + " public static final Vector " + mangleExpression(" __JContractS__getPostList_" + getSignature()) + "() {"; String code = header + "\n Vector vec = new Vector();\n" + body + " return vec;\n" + " }\n"; return code; } @@ -635,8 +635,8 @@ repositoryName = repositoryName + superclassName.substring(superclassName.lastIndexOf(".") +... [truncated message content] |