Menu
▾
▴
jcontracts-svn
|
From: <js...@us...> - 2006-11-23 17:21:38
|
Revision: 16
http://svn.sourceforge.net/jcontracts/?rev=16&view=rev
Author: jstuyts
Date: 2006-11-23 09:21:27 -0800 (Thu, 23 Nov 2006)
Log Message:
-----------
Corrected path of main class.
Modified Paths:
--------------
trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java
trunk/source/java/net/sf/jcontracts/icontract/MergeOption.java
Modified: trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java 2006-11-23 17:14:28 UTC (rev 15)
+++ trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java 2006-11-23 17:21:27 UTC (rev 16)
@@ -16,7 +16,7 @@
protected void activateOnTargets(Vector targets) {
System.out.println("NAME: iContract, Version " + VERSION);
System.out.println("AUTHOR: Copyright (C), 1997,98,99 Reto Kramer <in...@re...>");
- System.out.println("SYNOPSIS: java iContract.Tool {option} {file}");
+ 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\".");
System.out.println(" Instruments java source code files with checks to enforce:");
System.out.println(" - method pre- and post-conditions");
Modified: trunk/source/java/net/sf/jcontracts/icontract/MergeOption.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/MergeOption.java 2006-11-23 17:14:28 UTC (rev 15)
+++ trunk/source/java/net/sf/jcontracts/icontract/MergeOption.java 2006-11-23 17:21:27 UTC (rev 16)
@@ -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. \"iContract.Tool<SPACE>pre\" enables pre)");
+ 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)");
}
String pattern = patternline.substring(0, patternline.indexOf(' '));
if (match(item, pattern)) {
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <js...@us...> - 2006-11-23 17:23:36
|
Revision: 17
http://svn.sourceforge.net/jcontracts/?rev=17&view=rev
Author: jstuyts
Date: 2006-11-23 09:23:27 -0800 (Thu, 23 Nov 2006)
Log Message:
-----------
Corrected names of system properties.
Modified Paths:
--------------
trunk/source/java/net/sf/jcontracts/icontract/Class.java
trunk/source/java/net/sf/jcontracts/icontract/Method.java
trunk/source/java/net/sf/jcontracts/icontract/Tool.java
Modified: trunk/source/java/net/sf/jcontracts/icontract/Class.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/Class.java 2006-11-23 17:21:27 UTC (rev 16)
+++ trunk/source/java/net/sf/jcontracts/icontract/Class.java 2006-11-23 17:23:27 UTC (rev 17)
@@ -618,9 +618,9 @@
String inst_var_decl = "// Keeps track of calling chain to avoid recursive invariant checks.\n";
inst_var_decl = inst_var_decl + "// Avoids inv checks in public methods that are called from private ones.\n";
inst_var_decl = inst_var_decl + "// Stores bookkeeping information -- key: thread, value: call level\n";
- boolean do_not_enforce_precompilation_of_source = Boolean.getBoolean("icontract.internal.do_not_enforce_precompilation_of_source");
+ 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:icontract.internal.do_not_enforce_precompilation_of_source=true");
+ System.err.println("iContract:SWITCH:jcontracts.internal.do_not_enforce_precompilation_of_source=true");
}
boolean icl_already_defined = false;
if (!do_not_enforce_precompilation_of_source) {
@@ -632,7 +632,7 @@
}
}
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 -Dicontract.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("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!");
}
if (!icl_already_defined) {
inst_var_decl = inst_var_decl + "protected transient java.util.Hashtable __icl_ = new java.util.Hashtable(1);\n";
Modified: trunk/source/java/net/sf/jcontracts/icontract/Method.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/Method.java 2006-11-23 17:21:27 UTC (rev 16)
+++ trunk/source/java/net/sf/jcontracts/icontract/Method.java 2006-11-23 17:23:27 UTC (rev 17)
@@ -855,10 +855,10 @@
log.debug("getOldVarSaveCode:type_of_val=" + type_of_val);
String tmp_val = getMangledValue(val);
log.debug("getOldVarSaveCode:tmp_val =" + tmp_val);
- boolean do_clone_for_oldvalues = Boolean.getBoolean("icontract.internal.do_clone_for_oldvalues");
+ boolean do_clone_for_oldvalues = Boolean.getBoolean("jcontracts.internal.do_clone_for_oldvalues");
if (do_clone_for_oldvalues) {
- System.err.println("iContract:SWITCH:icontract.internal.do_clone_for_oldvalues=true");
- System.err.println("Classes that implement java.lang.Cloneable, Arrays and Strings will be cloned if they appear in postcondition old-value references (e.g. @post xxx@pre). THIS IS NOT DEFAULT BEHAVIOUR PAST 0.2b6, remove -Dicontract.internal.do_clone_for_oldvalues to disable.");
+ System.err.println("iContract:SWITCH:jcontracts.internal.do_clone_for_oldvalues=true");
+ System.err.println("Classes that implement java.lang.Cloneable, Arrays and Strings will be cloned if they appear in postcondition old-value references (e.g. @post xxx@pre). THIS IS NOT DEFAULT BEHAVIOUR PAST 0.2b6, remove -Djcontracts.internal.do_clone_for_oldvalues to disable.");
if (type_of_val.equals("int") || type_of_val.equals("float") || type_of_val.equals("boolean") || type_of_val.equals("byte") || type_of_val.equals("double") || type_of_val.equals("long") || type_of_val.equals("short") || type_of_val.equals("char")) {
code = code + "// can not call methods on " + type_of_val + " (therefore no clone).\n";
code = code + type_of_val + " " + tmp_val + " = " + base_val + "; // save " + val + " (in " + (String)post_source.elementAt(i) + ")\n";
Modified: trunk/source/java/net/sf/jcontracts/icontract/Tool.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/Tool.java 2006-11-23 17:21:27 UTC (rev 16)
+++ trunk/source/java/net/sf/jcontracts/icontract/Tool.java 2006-11-23 17:23:27 UTC (rev 17)
@@ -118,7 +118,7 @@
if (!unresolved.isEmpty()) {
log.error("\n");
log.error("could not resolve the following type names:\n" + unresolved);
- boolean do_not_enforce_precompilation_of_source = Boolean.getBoolean("icontract.internal.do_not_enforce_precompilation_of_source");
+ boolean do_not_enforce_precompilation_of_source = Boolean.getBoolean("jcontracts.internal.do_not_enforce_precompilation_of_source");
if (!do_not_enforce_precompilation_of_source) {
throw new RuntimeException("could not resolve the following type names:\n" + unresolved);
}
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
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] |
|
From: <js...@us...> - 2006-11-24 09:50:56
|
Revision: 20
http://svn.sourceforge.net/jcontracts/?rev=20&view=rev
Author: jstuyts
Date: 2006-11-24 01:50:54 -0800 (Fri, 24 Nov 2006)
Log Message:
-----------
Removed URLs that no longer work.
Modified Paths:
--------------
trunk/source/java/net/sf/jcontracts/icontract/Darwin.java
trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java
trunk/source/java/net/sf/jcontracts/icontract/Tool.java
Modified: trunk/source/java/net/sf/jcontracts/icontract/Darwin.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/Darwin.java 2006-11-24 07:56:11 UTC (rev 19)
+++ trunk/source/java/net/sf/jcontracts/icontract/Darwin.java 2006-11-24 09:50:54 UTC (rev 20)
@@ -63,7 +63,7 @@
}
log.info("iDarwin, Version 0.1a");
- log.info("Copyright (C) 1997,98,99 Reto Kramer <in...@re...>");
+ log.info("Copyright (C) 1997,98,99 Reto Kramer");
log.info("options:" + options);
log.info("all files:" + targets);
if (targets.isEmpty()) {
Modified: trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java 2006-11-24 07:56:11 UTC (rev 19)
+++ trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java 2006-11-24 09:50:54 UTC (rev 20)
@@ -47,7 +47,7 @@
protected void activateOnTargets(Vector targets) {
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("AUTHOR: Copyright (C), 1997,98,99 Reto Kramer");
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\".");
System.out.println(" Instruments java source code files with checks to enforce:");
@@ -148,10 +148,10 @@
System.out.println(" source file (removes all lines starting with \"/*|*/\").");
System.out.println(" Also creates a clean file <inputfile>.clean");
System.out.println("");
- //System.out.println(" PROBLEMS:");
- //System.out.println(" Please send problem reports and requests for new features as");
- //System.out.println(" an e-mail to <ICO...@RE...>.");
- //System.out.println(" Submitters will receive a reply with a problem tracking-number.");
+ System.out.println(" PROBLEMS:");
+ System.out.println(" Please enter problem reports and requests for new features in");
+ System.out.println(" the issue tracker, which can be found at:");
+ System.out.println(" https://sourceforge.net/tracker/?group_id=175492&atid=889550");
System.exit(0);
}
}
Modified: trunk/source/java/net/sf/jcontracts/icontract/Tool.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/Tool.java 2006-11-24 07:56:11 UTC (rev 19)
+++ trunk/source/java/net/sf/jcontracts/icontract/Tool.java 2006-11-24 09:50:54 UTC (rev 20)
@@ -71,7 +71,7 @@
}
log.info("Java Contract Suite, Version " + HelpOption.VERSION);
- log.info("Copyright (C) 1997-2000 Reto Kramer <in...@re...>");
+ log.info("Copyright (C) 1997-2000 Reto Kramer");
log.info("options:" + options);
log.info("all files:" + targets);
if (targets.isEmpty()) {
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <js...@us...> - 2006-11-24 10:13:21
|
Revision: 21
http://svn.sourceforge.net/jcontracts/?rev=21&view=rev
Author: jstuyts
Date: 2006-11-24 02:13:20 -0800 (Fri, 24 Nov 2006)
Log Message:
-----------
Updated copyright statements.
Modified Paths:
--------------
trunk/source/java/net/sf/jcontracts/icontract/Darwin.java
trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java
trunk/source/java/net/sf/jcontracts/icontract/Tool.java
Modified: trunk/source/java/net/sf/jcontracts/icontract/Darwin.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/Darwin.java 2006-11-24 09:50:54 UTC (rev 20)
+++ trunk/source/java/net/sf/jcontracts/icontract/Darwin.java 2006-11-24 10:13:20 UTC (rev 21)
@@ -63,7 +63,8 @@
}
log.info("iDarwin, Version 0.1a");
- log.info("Copyright (C) 1997,98,99 Reto Kramer");
+ log.info("Copyright (C) 1997-1999 Reto Kramer");
+ log.info("Copyright (C) 2006 John Swapceinski, Johan\xA0Stuyts");
log.info("options:" + options);
log.info("all files:" + targets);
if (targets.isEmpty()) {
Modified: trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java 2006-11-24 09:50:54 UTC (rev 20)
+++ trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java 2006-11-24 10:13:20 UTC (rev 21)
@@ -47,7 +47,8 @@
protected void activateOnTargets(Vector targets) {
System.out.println("NAME: Java Contract Suite, Version " + VERSION);
- System.out.println("AUTHOR: Copyright (C), 1997,98,99 Reto Kramer");
+ System.out.println("AUTHOR: Copyright (C) 1997-1999 Reto Kramer");
+ System.out.println(" Copyright (C) 2006 John Swapceinski, Johan Stuyts");
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\".");
System.out.println(" Instruments java source code files with checks to enforce:");
Modified: trunk/source/java/net/sf/jcontracts/icontract/Tool.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/Tool.java 2006-11-24 09:50:54 UTC (rev 20)
+++ trunk/source/java/net/sf/jcontracts/icontract/Tool.java 2006-11-24 10:13:20 UTC (rev 21)
@@ -72,6 +72,7 @@
log.info("Java Contract Suite, Version " + HelpOption.VERSION);
log.info("Copyright (C) 1997-2000 Reto Kramer");
+ log.info("Copyright (C) 2006 John Swapceinski, Johan Stuyts");
log.info("options:" + options);
log.info("all files:" + targets);
if (targets.isEmpty()) {
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <js...@us...> - 2006-11-27 20:14:52
|
Revision: 34
http://svn.sourceforge.net/jcontracts/?rev=34&view=rev
Author: jstuyts
Date: 2006-11-27 12:14:50 -0800 (Mon, 27 Nov 2006)
Log Message:
-----------
Formatted code.
Modified Paths:
--------------
trunk/source/java/net/sf/jcontracts/icontract/AllFilesUpToDateException.java
trunk/source/java/net/sf/jcontracts/icontract/AllOption.java
trunk/source/java/net/sf/jcontracts/icontract/ArgMetaclassFactory.java
trunk/source/java/net/sf/jcontracts/icontract/AssertionExpression.java
trunk/source/java/net/sf/jcontracts/icontract/Class.java
trunk/source/java/net/sf/jcontracts/icontract/CleanOption.java
trunk/source/java/net/sf/jcontracts/icontract/CompilerOption.java
trunk/source/java/net/sf/jcontracts/icontract/Constants.java
trunk/source/java/net/sf/jcontracts/icontract/Darwin.java
trunk/source/java/net/sf/jcontracts/icontract/DefaultExceptionOption.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/IContracted.java
trunk/source/java/net/sf/jcontracts/icontract/Interface.java
trunk/source/java/net/sf/jcontracts/icontract/Internal0Option.java
trunk/source/java/net/sf/jcontracts/icontract/InvCheck.java
trunk/source/java/net/sf/jcontracts/icontract/InvCheckCallOption.java
trunk/source/java/net/sf/jcontracts/icontract/MergeOption.java
trunk/source/java/net/sf/jcontracts/icontract/MetaclassFactory.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/OneOneOption.java
trunk/source/java/net/sf/jcontracts/icontract/Option.java
trunk/source/java/net/sf/jcontracts/icontract/OutputOption.java
trunk/source/java/net/sf/jcontracts/icontract/ParameterOption.java
trunk/source/java/net/sf/jcontracts/icontract/PrePostCheck.java
trunk/source/java/net/sf/jcontracts/icontract/ProcessingOption.java
trunk/source/java/net/sf/jcontracts/icontract/QuietOption.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/SystemInTarget.java
trunk/source/java/net/sf/jcontracts/icontract/Target.java
trunk/source/java/net/sf/jcontracts/icontract/Tool.java
trunk/source/java/net/sf/jcontracts/icontract/UnableToDetermineTypeException.java
trunk/source/java/net/sf/jcontracts/icontract/Variable.java
trunk/source/java/net/sf/jcontracts/icontract/VerboseOption.java
trunk/source/java/net/sf/jcontracts/icontract/WrapExceptionOption.java
trunk/source/java/net/sf/jcontracts/icontract/XOption.java
Modified: trunk/source/java/net/sf/jcontracts/icontract/AllFilesUpToDateException.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/AllFilesUpToDateException.java 2006-11-27 16:56:26 UTC (rev 33)
+++ trunk/source/java/net/sf/jcontracts/icontract/AllFilesUpToDateException.java 2006-11-27 20:14:50 UTC (rev 34)
@@ -1,11 +1,14 @@
package net.sf.jcontracts.icontract;
-
-public class AllFilesUpToDateException extends RuntimeException {
-
- public AllFilesUpToDateException() {
- }
-
- public AllFilesUpToDateException(String s) {
- super(s);
- }
-}
+
+public class AllFilesUpToDateException extends RuntimeException
+{
+
+ public AllFilesUpToDateException()
+ {
+ }
+
+ public AllFilesUpToDateException(String s)
+ {
+ super(s);
+ }
+}
Modified: trunk/source/java/net/sf/jcontracts/icontract/AllOption.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/AllOption.java 2006-11-27 16:56:26 UTC (rev 33)
+++ trunk/source/java/net/sf/jcontracts/icontract/AllOption.java 2006-11-27 20:14:50 UTC (rev 34)
@@ -1,12 +1,14 @@
package net.sf.jcontracts.icontract;
import java.util.Vector;
-
-public class AllOption extends ParameterOption {
-
- public static final String NAME = "a";
-
- public AllOption(String name, Vector arguments) {
- super(name, arguments);
- }
-}
+
+public class AllOption extends ParameterOption
+{
+
+ public static final String NAME = "a";
+
+ public AllOption(String name, Vector arguments)
+ {
+ super(name, arguments);
+ }
+}
Modified: trunk/source/java/net/sf/jcontracts/icontract/ArgMetaclassFactory.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/ArgMetaclassFactory.java 2006-11-27 16:56:26 UTC (rev 33)
+++ trunk/source/java/net/sf/jcontracts/icontract/ArgMetaclassFactory.java 2006-11-27 20:14:50 UTC (rev 34)
@@ -5,80 +5,107 @@
import net.sf.jcontracts.argparser.OptionMetaclass;
import net.sf.jcontracts.argparser.ParserMetaclassFactory;
import net.sf.jcontracts.argparser.TargetMetaclass;
-
-public class ArgMetaclassFactory
- implements ParserMetaclassFactory {
-
- public OptionMetaclass newOption(String name, Vector parameters) {
- OptionMetaclass o = null;
- try {
- if (name.compareTo("h") == 0) {
- o = new HelpOption(name, parameters);
- } else
- if (name.compareTo("v") == 0) {
- o = new VerboseOption(name, parameters);
- } else
- if (name.compareTo("c") == 0) {
- o = new CompilerOption(name, parameters);
- } else
- if (name.compareTo("b") == 0) {
- o = new SourceCompilerOption(name, parameters);
- } else
- if (name.compareTo("n") == 0) {
- o = new NoRepositoryCompilationOption(name, parameters);
- } else
- if (name.compareTo("o") == 0) {
- o = new OutputOption(name, parameters);
- } else
- if (name.compareTo("y") == 0) {
- o = new OneOneOption(name, parameters);
- } else
- if (name.compareTo("k") == 0) {
- o = new RepositoryOutputOption(name, parameters);
- } else
- if (name.compareTo("d") == 0) {
- o = new DefaultExceptionOption(name, parameters);
- } else
- if (name.compareTo("r") == 0) {
- o = new CleanOption(name, parameters);
- } else
- if (name.compareTo("m") == 0) {
- o = new MergeOption(name, parameters);
- } else
- if (name.compareTo("i") == 0) {
- o = new InvCheckCallOption(name, parameters);
- } else
- if (name.compareTo("w") == 0) {
- o = new WrapExceptionOption(name, parameters);
- } else
- if (name.compareTo("q") == 0) {
- o = new QuietOption(name, parameters);
- } else
- if (name.compareTo("a") == 0) {
- o = new AllOption(name, parameters);
- } else
- if (name.compareTo("x") == 0) {
- o = new XOption(name, parameters);
- } else
- if (name.compareTo("Z") == 0) {
- o = new Internal0Option(name, parameters);
- } else
- if (name.compareTo("j") == 0) {
- o = new NoInitialCompilationOption(name, parameters);
- } else {
- throw new RuntimeException("Java Contract Suite: error: unknown option -" + name);
- }
- }
- catch (NoClassDefFoundError _ex) {
- throw new RuntimeException("Attempt to perform in-process call to sun.tools.javac.Main failed because the class could not be found! In Java-2, make sure that the JDK's tools.jar (contain sun.tools.javac.*) is on your classpath!", _ex);
- }
- return o;
- }
-
- public TargetMetaclass newTarget(String name) {
- return new FileTarget(name);
- }
-
- public ArgMetaclassFactory() {
- }
-}
+
+public class ArgMetaclassFactory implements ParserMetaclassFactory
+{
+
+ public OptionMetaclass newOption(String name, Vector parameters)
+ {
+ OptionMetaclass o = null;
+ try
+ {
+ if (name.compareTo("h") == 0)
+ {
+ o = new HelpOption(name, parameters);
+ }
+ else if (name.compareTo("v") == 0)
+ {
+ o = new VerboseOption(name, parameters);
+ }
+ else if (name.compareTo("c") == 0)
+ {
+ o = new CompilerOption(name, parameters);
+ }
+ else if (name.compareTo("b") == 0)
+ {
+ o = new SourceCompilerOption(name, parameters);
+ }
+ else if (name.compareTo("n") == 0)
+ {
+ o = new NoRepositoryCompilationOption(name, parameters);
+ }
+ else if (name.compareTo("o") == 0)
+ {
+ o = new OutputOption(name, parameters);
+ }
+ else if (name.compareTo("y") == 0)
+ {
+ o = new OneOneOption(name, parameters);
+ }
+ else if (name.compareTo("k") == 0)
+ {
+ o = new RepositoryOutputOption(name, parameters);
+ }
+ else if (name.compareTo("d") == 0)
+ {
+ o = new DefaultExceptionOption(name, parameters);
+ }
+ else if (name.compareTo("r") == 0)
+ {
+ o = new CleanOption(name, parameters);
+ }
+ else if (name.compareTo("m") == 0)
+ {
+ o = new MergeOption(name, parameters);
+ }
+ else if (name.compareTo("i") == 0)
+ {
+ o = new InvCheckCallOption(name, parameters);
+ }
+ else if (name.compareTo("w") == 0)
+ {
+ o = new WrapExceptionOption(name, parameters);
+ }
+ else if (name.compareTo("q") == 0)
+ {
+ o = new QuietOption(name, parameters);
+ }
+ else if (name.compareTo("a") == 0)
+ {
+ o = new AllOption(name, parameters);
+ }
+ else if (name.compareTo("x") == 0)
+ {
+ o = new XOption(name, parameters);
+ }
+ else if (name.compareTo("Z") == 0)
+ {
+ o = new Internal0Option(name, parameters);
+ }
+ else if (name.compareTo("j") == 0)
+ {
+ o = new NoInitialCompilationOption(name, parameters);
+ }
+ else
+ {
+ throw new RuntimeException("Java Contract Suite: error: unknown option -" + name);
+ }
+ }
+ catch (NoClassDefFoundError _ex)
+ {
+ throw new RuntimeException(
+ "Attempt to perform in-process call to sun.tools.javac.Main failed because the class could not be found! In Java-2, make sure that the JDK's tools.jar (contain sun.tools.javac.*) is on your classpath!",
+ _ex);
+ }
+ return o;
+ }
+
+ public TargetMetaclass newTarget(String name)
+ {
+ return new FileTarget(name);
+ }
+
+ public ArgMetaclassFactory()
+ {
+ }
+}
Modified: trunk/source/java/net/sf/jcontracts/icontract/AssertionExpression.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/AssertionExpression.java 2006-11-27 16:56:26 UTC (rev 33)
+++ trunk/source/java/net/sf/jcontracts/icontract/AssertionExpression.java 2006-11-27 20:14:50 UTC (rev 34)
@@ -8,865 +8,1149 @@
import org.apache.log4j.Logger;
-class AssertionExpression {
- private static final Logger log = Logger.getLogger(AssertionExpression.class);
- private String expression_;
- private IContracted subject_;
+class AssertionExpression
+{
+ private static final Logger log = Logger.getLogger(AssertionExpression.class);
- AssertionExpression(String expr, IContracted subject) {
- expression_ = expr.trim();
- subject_ = subject;
- }
+ private String expression_;
- void addBoundVariablesTo(Hashtable vartab) {
- String elementType = getElementType();
- String elementVar = getElementVar();
- vartab.put(elementVar, elementType);
- String quantifiedExpression = getQuantifiedExpression();
- AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
- if (subassert.includesQuantifier()) {
- subassert.addBoundVariablesTo(vartab);
- }
- }
+ private IContracted subject_;
- boolean containsImplies(String expr) {
- return expr.indexOf("implies") != -1;
- }
+ AssertionExpression(String expr, IContracted subject)
+ {
+ expression_ = expr.trim();
+ subject_ = subject;
+ }
- String getCheckCode() {
- String code = "";
- String resultVar = "__result_" + getMangledValue(getElementVar());
- code = code + getPartialCheckCode();
- String prefix = getUpToQuantifier();
- code = code + "if (!" + prefix + resultVar + ")\n";
- return code;
- }
+ void addBoundVariablesTo(Hashtable vartab)
+ {
+ String elementType = getElementType();
+ String elementVar = getElementVar();
+ vartab.put(elementVar, elementType);
+ String quantifiedExpression = getQuantifiedExpression();
+ AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
+ if (subassert.includesQuantifier())
+ {
+ subassert.addBoundVariablesTo(vartab);
+ }
+ }
- private String getElementType() {
- int f = expression_.indexOf("forall ");
- if (f == -1) {
- f = expression_.indexOf("exists ");
- }
- int start = expression_.indexOf(" ", f);
- int end = expression_.indexOf(" ", start + 1);
- return expression_.substring(start, end).trim();
- }
+ boolean containsImplies(String expr)
+ {
+ return expr.indexOf("implies") != -1;
+ }
- private String getElementVar() {
- int dummy = 0;
- int start = 0;
- int end = 0;
- String res = "";
- try {
- int f = expression_.indexOf("forall ");
- if (f == -1) {
+ String getCheckCode()
+ {
+ String code = "";
+ String resultVar = "__result_" + getMangledValue(getElementVar());
+ code = code + getPartialCheckCode();
+ String prefix = getUpToQuantifier();
+ code = code + "if (!" + prefix + resultVar + ")\n";
+ return code;
+ }
+
+ private String getElementType()
+ {
+ int f = expression_.indexOf("forall ");
+ if (f == -1)
+ {
f = expression_.indexOf("exists ");
- }
- dummy = expression_.indexOf(" ", f);
- start = expression_.indexOf(" ", dummy + 1);
- end = expression_.indexOf(" ", start + 1);
- res = expression_.substring(start, end).trim();
- }
- catch (StringIndexOutOfBoundsException _ex) {
- throw new RuntimeException("can not determine the variable name in expression " + expression_);
- }
- return res;
- }
+ }
+ int start = expression_.indexOf(" ", f);
+ int end = expression_.indexOf(" ", start + 1);
+ return expression_.substring(start, end).trim();
+ }
- private String getExistsCheckCode() {
- String code = "";
- String quantificationDomain = getQuantificationDomain();
- if (isRangeDomain(quantificationDomain)) {
- code = getExistsCheckCode_OverRange();
- } else
- if (isArrayDomain()) {
- code = getExistsCheckCode_OverArray();
- } else
- if (isIteratorDomain()) {
- code = getExistsCheckCode_OverIterator(false);
- } else
- if (isEnumerationDomain()) {
- code = getExistsCheckCode_OverEnumeration(false);
- } else {
- String d = getQuantificationDomain().trim();
- String type_of_domain = "";
- try {
- type_of_domain = subject_.getTypeOfValue(d).trim();
- if (type_of_domain.indexOf("[") != -1) {
- code = getExistsCheckCode_OverArray();
- } else
- if (type_of_domain.equals("java.util.Enumeration")) {
- code = getExistsCheckCode_OverEnumeration(false);
- } else
- if (type_of_domain.equals("java.util.Iterator")) {
- code = getExistsCheckCode_OverIterator(false);
- } else
- if (isImplementationOf("java.util.Iterator", type_of_domain)) {
- code = getExistsCheckCode_OverIterator(false);
- } else
- if (isImplementationOf("java.util.Enumeration", type_of_domain)) {
- code = getExistsCheckCode_OverEnumeration(false);
- } else
- if (hasImplementationOfMethod("elements", "java.util.Enumeration", type_of_domain)) {
- code = getExistsCheckCode_OverEnumeration(true);
- } else
- if (hasImplementationOfMethod("iterator", "java.util.Iterator", type_of_domain)) {
- code = getExistsCheckCode_OverIterator(true);
- } else {
- String dd = getQuantificationDomain().trim();
- log.warn("The type of " + dd + " in " + ((CodeMetaclass)subject_).getSignature() + " is " + type_of_domain + "\n" + "Complete assertion: " + subject_ + "\nQuantifier domains must be: Array, Range (e.g. a .. b [by c]), Enumeration, Iterator or implementation thereof or\nimplementors of 'Enumeration elements()' or 'Iterator iterator()' (e.g. the Java 2 Collections, JDK 1.1 Vector, etc.)\n" + "As a best effort will use java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
- code = getExistsCheckCode_OverEnumeration(false);
+ private String getElementVar()
+ {
+ int dummy = 0;
+ int start = 0;
+ int end = 0;
+ String res = "";
+ try
+ {
+ int f = expression_.indexOf("forall ");
+ if (f == -1)
+ {
+ f = expression_.indexOf("exists ");
}
- }
- catch (UnableToDetermineTypeException e) {
- String dd = getQuantificationDomain().trim();
- log.warn("Could not determine type of " + dd + " in " + ((CodeMetaclass)subject_).getSignature() + "\n" + "Complete assertion: " + subject_ + "\n" + "Using java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
- log.warn(e.getMessage());
+ dummy = expression_.indexOf(" ", f);
+ start = expression_.indexOf(" ", dummy + 1);
+ end = expression_.indexOf(" ", start + 1);
+ res = expression_.substring(start, end).trim();
+ }
+ catch (StringIndexOutOfBoundsException _ex)
+ {
+ throw new RuntimeException("can not determine the variable name in expression " + expression_);
+ }
+ return res;
+ }
+
+ private String getExistsCheckCode()
+ {
+ String code = "";
+ String quantificationDomain = getQuantificationDomain();
+ if (isRangeDomain(quantificationDomain))
+ {
+ code = getExistsCheckCode_OverRange();
+ }
+ else if (isArrayDomain())
+ {
+ code = getExistsCheckCode_OverArray();
+ }
+ else if (isIteratorDomain())
+ {
+ code = getExistsCheckCode_OverIterator(false);
+ }
+ else if (isEnumerationDomain())
+ {
code = getExistsCheckCode_OverEnumeration(false);
- }
- }
- return code;
- }
+ }
+ else
+ {
+ String d = getQuantificationDomain().trim();
+ String type_of_domain = "";
+ try
+ {
+ type_of_domain = subject_.getTypeOfValue(d).trim();
+ if (type_of_domain.indexOf("[") != -1)
+ {
+ code = getExistsCheckCode_OverArray();
+ }
+ else if (type_of_domain.equals("java.util.Enumeration"))
+ {
+ code = getExistsCheckCode_OverEnumeration(false);
+ }
+ else if (type_of_domain.equals("java.util.Iterator"))
+ {
+ code = getExistsCheckCode_OverIterator(false);
+ }
+ else if (isImplementationOf("java.util.Iterator", type_of_domain))
+ {
+ code = getExistsCheckCode_OverIterator(false);
+ }
+ else if (isImplementationOf("java.util.Enumeration", type_of_domain))
+ {
+ code = getExistsCheckCode_OverEnumeration(false);
+ }
+ else if (hasImplementationOfMethod("elements", "java.util.Enumeration", type_of_domain))
+ {
+ code = getExistsCheckCode_OverEnumeration(true);
+ }
+ else if (hasImplementationOfMethod("iterator", "java.util.Iterator", type_of_domain))
+ {
+ code = getExistsCheckCode_OverIterator(true);
+ }
+ else
+ {
+ String dd = getQuantificationDomain().trim();
+ log
+ .warn("The type of "
+ + dd
+ + " in "
+ + ((CodeMetaclass) subject_).getSignature()
+ + " is "
+ + type_of_domain
+ + "\n"
+ + "Complete assertion: "
+ + subject_
+ + "\nQuantifier domains must be: Array, Range (e.g. a .. b [by c]), Enumeration, Iterator or implementation thereof or\nimplementors of 'Enumeration elements()' or 'Iterator iterator()' (e.g. the Java 2 Collections, JDK 1.1 Vector, etc.)\n"
+ + "As a best effort will use java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
+ code = getExistsCheckCode_OverEnumeration(false);
+ }
+ }
+ catch (UnableToDetermineTypeException e)
+ {
+ String dd = getQuantificationDomain().trim();
+ log
+ .warn("Could not determine type of "
+ + dd
+ + " in "
+ + ((CodeMetaclass) subject_).getSignature()
+ + "\n"
+ + "Complete assertion: "
+ + subject_
+ + "\n"
+ + "Using java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
+ log.warn(e.getMessage());
+ code = getExistsCheckCode_OverEnumeration(false);
+ }
+ }
+ return code;
+ }
- private String getExistsCheckCode_OverArray() {
- String code = "";
- String elementType = getElementType();
- String elementVar = getElementVar();
- String indexVar = "__index_" + getMangledValue(getElementVar());
- String resultVar = "__result_" + getMangledValue(getElementVar());
- String quantificationDomain = getQuantificationDomain();
- String quantifiedExpression = getQuantifiedExpression();
- code = code + "boolean " + resultVar + "=false;\n";
- code = code + "for ( int " + indexVar + "= 0; (" + indexVar + " < " + quantificationDomain + ".length) && !" + resultVar + "; " + indexVar + "++){\n";
- code = code + " " + elementType + " " + elementVar + "= " + quantificationDomain + "[" + indexVar + "];\n";
- AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
- if (subassert.includesQuantifier()) {
- code = code + subassert.getPartialCheckCode();
- String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
- code = code + resultVar + "=" + subresultVar + ";\n";
- } else
- if (containsImplies(quantifiedExpression)) {
- code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression) + " )) // implication condition\n";
- code = code + " { } // amount to dc\n";
- code = code + "else {\n";
- code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
- code = code + "}\n";
- } else {
- code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
- }
- code = code + "} // loop\n";
- return code;
- }
+ private String getExistsCheckCode_OverArray()
+ {
+ String code = "";
+ String elementType = getElementType();
+ String elementVar = getElementVar();
+ String indexVar = "__index_" + getMangledValue(getElementVar());
+ String resultVar = "__result_" + getMangledValue(getElementVar());
+ String quantificationDomain = getQuantificationDomain();
+ String quantifiedExpression = getQuantifiedExpression();
+ code = code + "boolean " + resultVar + "=false;\n";
+ code = code + "for ( int " + indexVar + "= 0; (" + indexVar + " < " + quantificationDomain + ".length) && !"
+ + resultVar + "; " + indexVar + "++){\n";
+ code = code + " " + elementType + " " + elementVar + "= " + quantificationDomain + "[" + indexVar + "];\n";
+ AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
+ if (subassert.includesQuantifier())
+ {
+ code = code + subassert.getPartialCheckCode();
+ String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
+ code = code + resultVar + "=" + subresultVar + ";\n";
+ }
+ else if (containsImplies(quantifiedExpression))
+ {
+ code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression)
+ + " )) // implication condition\n";
+ code = code + " { } // amount to dc\n";
+ code = code + "else {\n";
+ code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
+ code = code + "}\n";
+ }
+ else
+ {
+ code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
+ }
+ code = code + "} // loop\n";
+ return code;
+ }
- private String getExistsCheckCode_OverEnumeration(boolean enumerationImpl) {
- String code = "";
- String elementType = getElementType();
- String castElementType = elementType;
- if (elementType.equals("int")) {
- castElementType = "Integer";
- }
- if (elementType.equals("float")) {
- castElementType = "Float";
- }
- if (elementType.equals("boolean")) {
- castElementType = "Boolean";
- }
- if (elementType.equals("byte")) {
- castElementType = "Byte";
- }
- if (elementType.equals("double")) {
- castElementType = "Double";
- }
- if (elementType.equals("long")) {
- castElementType = "Long";
- }
- if (elementType.equals("short")) {
- castElementType = "Short";
- }
- if (elementType.equals("char")) {
- castElementType = "Character";
- }
- String enumVar = "__" + getMangledValue(getElementVar()) + "_enum";
- String elementVar = getElementVar();
- String resultVar = "__result_" + getMangledValue(getElementVar());
- String quantificationDomain = getQuantificationDomain();
- String quantifiedExpression = getQuantifiedExpression();
- code = code + "boolean " + resultVar + "=false;\n";
- String postfix = "";
- if (enumerationImpl) {
- postfix = ".elements()";
- }
- code = code + "for (java.util.Enumeration " + enumVar + "=" + quantificationDomain + postfix + ";\n";
- code = code + " " + enumVar + ".hasMoreElements() && !" + resultVar + "; ){\n";
- code = code + " " + castElementType + " " + elementVar + "=(";
- code = code + castElementType + ")(" + enumVar + ".nextElement());\n";
- AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
- if (subassert.includesQuantifier()) {
- code = code + subassert.getPartialCheckCode();
- String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
- code = code + resultVar + "=" + subresultVar + ";\n";
- } else
- if (containsImplies(quantifiedExpression)) {
- code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression) + " )) // implication condition\n";
- code = code + " { } // amount to dc\n";
- code = code + "else {\n";
- code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
- code = code + "}\n";
- } else {
- code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
- }
- code = code + "} // loop\n";
- return code;
- }
+ private String getExistsCheckCode_OverEnumeration(boolean enumerationImpl)
+ {
+ String code = "";
+ String elementType = getElementType();
+ String castElementType = elementType;
+ if (elementType.equals("int"))
+ {
+ castElementType = "Integer";
+ }
+ if (elementType.equals("float"))
+ {
+ castElementType = "Float";
+ }
+ if (elementType.equals("boolean"))
+ {
+ castElementType = "Boolean";
+ }
+ if (elementType.equals("byte"))
+ {
+ castElementType = "Byte";
+ }
+ if (elementType.equals("double"))
+ {
+ castElementType = "Double";
+ }
+ if (elementType.equals("long"))
+ {
+ castElementType = "Long";
+ }
+ if (elementType.equals("short"))
+ {
+ castElementType = "Short";
+ }
+ if (elementType.equals("char"))
+ {
+ castElementType = "Character";
+ }
+ String enumVar = "__" + getMangledValue(getElementVar()) + "_enum";
+ String elementVar = getElementVar();
+ String resultVar = "__result_" + getMangledValue(getElementVar());
+ String quantificationDomain = getQuantificationDomain();
+ String quantifiedExpression = getQuantifiedExpression();
+ code = code + "boolean " + resultVar + "=false;\n";
+ String postfix = "";
+ if (enumerationImpl)
+ {
+ postfix = ".elements()";
+ }
+ code = code + "for (java.util.Enumeration " + enumVar + "=" + quantificationDomain + postfix + ";\n";
+ code = code + " " + enumVar + ".hasMoreElements() && !" + resultVar + "; ){\n";
+ code = code + " " + castElementType + " " + elementVar + "=(";
+ code = code + castElementType + ")(" + enumVar + ".nextElement());\n";
+ AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
+ if (subassert.includesQuantifier())
+ {
+ code = code + subassert.getPartialCheckCode();
+ String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
+ code = code + resultVar + "=" + subresultVar + ";\n";
+ }
+ else if (containsImplies(quantifiedExpression))
+ {
+ code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression)
+ + " )) // implication condition\n";
+ code = code + " { } // amount to dc\n";
+ code = code + "else {\n";
+ code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
+ code = code + "}\n";
+ }
+ else
+ {
+ code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
+ }
+ code = code + "} // loop\n";
+ return code;
+ }
- private String getExistsCheckCode_OverIterator(boolean iteratorImpl) {
- String code = "";
- String elementType = getElementType();
- String castElementType = elementType;
- if (elementType.equals("int")) {
- castElementType = "Integer";
- }
- if (elementType.equals("float")) {
- castElementType = "Float";
- }
- if (elementType.equals("boolean")) {
- castElementType = "Boolean";
- }
- if (elementType.equals("byte")) {
- castElementType = "Byte";
- }
- if (elementType.equals("double")) {
- castElementType = "Double";
- }
- if (elementType.equals("long")) {
- castElementType = "Long";
- }
- if (elementType.equals("short")) {
- castElementType = "Short";
- }
- if (elementType.equals("char")) {
- castElementType = "Character";
- }
- String enumVar = "__" + getMangledValue(getElementVar()) + "_iterator";
- String elementVar = getElementVar();
- String resultVar = "__result_" + getMangledValue(getElementVar());
- String quantificationDomain = getQuantificationDomain();
- String quantifiedExpression = getQuantifiedExpression();
- code = code + "boolean " + resultVar + "=false;\n";
- String postfix = "";
- if (iteratorImpl) {
- postfix = ".iterator()";
- }
- code = code + "for (java.util.Iterator " + enumVar + "=" + quantificationDomain + postfix + ";\n";
- code = code + " " + enumVar + ".hasNext() && !" + resultVar + "; ){\n";
- code = code + " " + castElementType + " " + elementVar + "=(";
- code = code + castElementType + ")(" + enumVar + ".next());\n";
- AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
- if (subassert.includesQuantifier()) {
- code = code + subassert.getPartialCheckCode();
- String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
- code = code + resultVar + "=" + subresultVar + ";\n";
- } else
- if (containsImplies(quantifiedExpression)) {
- code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression) + " )) // implication condition\n";
- code = code + " { } // amount to dc\n";
- code = code + "else {\n";
- code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
- code = code + "}\n";
- } else {
- code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
- }
- code = code + "} // loop\n";
- return code;
- }
+ private String getExistsCheckCode_OverIterator(boolean iteratorImpl)
+ {
+ String code = "";
+ String elementType = getElementType();
+ String castElementType = elementType;
+ if (elementType.equals("int"))
+ {
+ castElementType = "Integer";
+ }
+ if (elementType.equals("float"))
+ {
+ castElementType = "Float";
+ }
+ if (elementType.equals("boolean"))
+ {
+ castElementType = "Boolean";
+ }
+ if (elementType.equals("byte"))
+ {
+ castElementType = "Byte";
+ }
+ if (elementType.equals("double"))
+ {
+ castElementType = "Double";
+ }
+ if (elementType.equals("long"))
+ {
+ castElementType = "Long";
+ }
+ if (elementType.equals("short"))
+ {
+ castElementType = "Short";
+ }
+ if (elementType.equals("char"))
+ {
+ castElementType = "Character";
+ }
+ String enumVar = "__" + getMangledValue(getElementVar()) + "_iterator";
+ String elementVar = getElementVar();
+ String resultVar = "__result_" + getMangledValue(getElementVar());
+ String quantificationDomain = getQuantificationDomain();
+ String quantifiedExpression = getQuantifiedExpression();
+ code = code + "boolean " + resultVar + "=false;\n";
+ String postfix = "";
+ if (iteratorImpl)
+ {
+ postfix = ".iterator()";
+ }
+ code = code + "for (java.util.Iterator " + enumVar + "=" + quantificationDomain + postfix + ";\n";
+ code = code + " " + enumVar + ".hasNext() && !" + resultVar + "; ){\n";
+ code = code + " " + castElementType + " " + elementVar + "=(";
+ code = code + castElementType + ")(" + enumVar + ".next());\n";
+ AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
+ if (subassert.includesQuantifier())
+ {
+ code = code + subassert.getPartialCheckCode();
+ String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
+ code = code + resultVar + "=" + subresultVar + ";\n";
+ }
+ else if (containsImplies(quantifiedExpression))
+ {
+ code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression)
+ + " )) // implication condition\n";
+ code = code + " { } // amount to dc\n";
+ code = code + "else {\n";
+ code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
+ code = code + "}\n";
+ }
+ else
+ {
+ code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
+ }
+ code = code + "} // loop\n";
+ return code;
+ }
- private String getExistsCheckCode_OverRange() {
- String code = "";
- String elementType = getElementType();
- String _tmp = "__" + getMangledValue(getElementVar()) + "_counter";
- String elementVar = getElementVar();
- String resultVar = "__result_" + getMangledValue(getElementVar());
- String quantificationDomain = getQuantificationDomain();
- String rangeStart = getRangeStart(quantificationDomain);
- String rangeEnd = getRangeEnd(quantificationDomain);
- String step = getRangeStep(quantificationDomain);
- String quantifiedExpression = getQuantifiedExpression();
- code = code + "boolean " + resultVar + "=false;\n";
- code = code + "for (" + elementType + " " + elementVar + "=" + rangeStart + "; ";
- String compare = "";
- if (step.startsWith("-")) {
- compare = " >= ";
- } else {
- compare = " <= ";
- }
- code = code + "(" + elementVar + compare + rangeEnd + ") && !" + resultVar + "; " + elementVar + "=" + elementVar + "+(" + elementType + ")" + step + " ){\n";
- AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
- if (subassert.includesQuantifier()) {
- code = code + subassert.getPartialCheckCode();
- String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
- code = code + resultVar + "=" + subresultVar + ";\n";
- } else
- if (containsImplies(quantifiedExpression)) {
- code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression) + " )) // implication condition\n";
- code = code + " { } // amount to dc\n";
- code = code + "else {\n";
- code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
- code = code + "}\n";
- } else {
- code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
- }
- code = code + "} // loop\n";
- return code;
- }
+ private String getExistsCheckCode_OverRange()
+ {
+ String code = "";
+ String elementType = getElementType();
+ String _tmp = "__" + getMangledValue(getElementVar()) + "_counter";
+ String elementVar = getElementVar();
+ String resultVar = "__result_" + getMangledValue(getElementVar());
+ String quantificationDomain = getQuantificationDomain();
+ String rangeStart = getRangeStart(quantificationDomain);
+ String rangeEnd = getRangeEnd(quantificationDomain);
+ String step = getRangeStep(quantificationDomain);
+ String quantifiedExpression = getQuantifiedExpression();
+ code = code + "boolean " + resultVar + "=false;\n";
+ code = code + "for (" + elementType + " " + elementVar + "=" + rangeStart + "; ";
+ String compare = "";
+ if (step.startsWith("-"))
+ {
+ compare = " >= ";
+ }
+ else
+ {
+ compare = " <= ";
+ }
+ code = code + "(" + elementVar + compare + rangeEnd + ") && !" + resultVar + "; " + elementVar + "="
+ + elementVar + "+(" + elementType + ")" + step + " ){\n";
+ AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
+ if (subassert.includesQuantifier())
+ {
+ code = code + subassert.getPartialCheckCode();
+ String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
+ code = code + resultVar + "=" + subresultVar + ";\n";
+ }
+ else if (containsImplies(quantifiedExpression))
+ {
+ code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression)
+ + " )) // implication condition\n";
+ code = code + " { } // amount to dc\n";
+ code = code + "else {\n";
+ code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
+ code = code + "}\n";
+ }
+ else
+ {
+ code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
+ }
+ code = code + "} // loop\n";
+ return code;
+ }
- private String getForallCheckCode() {
- String code = "";
- String quantificationDomain = getQuantificationDomain();
- if (isRangeDomain(quantificationDomain)) {
- code = getForallCheckCode_OverRange();
- } else
- if (isArrayDomain()) {
- code = getForallCheckCode_OverArray();
- } else
- if (isIteratorDomain()) {
- code = getForallCheckCode_OverIterator(false);
- } else
- if (isEnumerationDomain()) {
- code = getForallCheckCode_OverEnumeration(false);
- } else {
- String d = getQuantificationDomain().trim();
- String type_of_domain = "";
- try {
- type_of_domain = subject_.getTypeOfValue(d).trim();
- if (type_of_domain.indexOf("[") != -1) {
- code = getForallCheckCode_OverArray();
- } else
- if (type_of_domain.equals("java.util.Enumeration")) {
- code = getForallCheckCode_OverEnumeration(false);
- } else
- if (type_of_domain.equals("java.util.Iterator")) {
- code = getForallCheckCode_OverIterator(false);
- } else
- if (isImplementationOf("java.util.Iterator", type_of_domain)) {
- code = getForallCheckCode_OverIterator(false);
- } else
- if (isImplementationOf("java.util.Enumeration", type_of_domain)) {
- code = getForallCheckCode_OverEnumeration(false);
- } else
- if (hasImplementationOfMethod("elements", "java.util.Enumeration", type_of_domain)) {
- code = getForallCheckCode_OverEnumeration(true);
- } else
- if (hasImplementationOfMethod("iterator", "java.util.Iterator", type_of_domain)) {
- code = getForallCheckCode_OverIterator(true);
- } else {
- String dd = getQuantificationDomain().trim();
- log.warn("The type of " + dd + " in " + ((CodeMetaclass)subject_).getSignature() + " is " + type_of_domain + "\n" + "Complete assertion: " + subject_ + "\nQuantifier domains must be: Array, Range (e.g. a .. b [by c]), Enumeration, Iterator or implementation thereof or\nimplementors of 'Enumeration elements()' or 'Iterator iterator()' (e.g. the Java 2 Collections, JDK 1.1 Vector, etc.)\n" + "As a best effort will use java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
- code = getForallCheckCode_OverEnumeration(false);
+ private String getForallCheckCode()
+ {
+ String code = "";
+ String quantificationDomain = getQuantificationDomain();
+ if (isRangeDomain(quantificationDomain))
+ {
+ code = getForallCheckCode_OverRange();
+ }
+ else if (isArrayDomain())
+ {
+ code = getForallCheckCode_OverArray();
+ }
+ else if (isIteratorDomain())
+ {
+ code = getForallCheckCode_OverIterator(false);
+ }
+ else if (isEnumerationDomain())
+ {
+ code = getForallCheckCode_OverEnumeration(false);
+ }
+ else
+ {
+ String d = getQuantificationDomain().trim();
+ String type_of_domain = "";
+ try
+ {
+ type_of_domain = subject_.getTypeOfValue(d).trim();
+ if (type_of_domain.indexOf("[") != -1)
+ {
+ code = getForallCheckCode_OverArray();
+ }
+ else if (type_of_domain.equals("java.util.Enumeration"))
+ {
+ code = getForallCheckCode_OverEnumeration(false);
+ }
+ else if (type_of_domain.equals("java.util.Iterator"))
+ {
+ code = getForallCheckCode_OverIterator(false);
+ }
+ else if (isImplementationOf("java.util.Iterator", type_of_domain))
+ {
+ code = getForallCheckCode_OverIterator(false);
+ }
+ else if (isImplementationOf("java.util.Enumeration", type_of_domain))
+ {
+ code = getForallCheckCode_OverEnumeration(false);
+ }
+ else if (hasImplementationOfMethod("elements", "java.util.Enumeration", type_of_domain))
+ {
+ code = getForallCheckCode_OverEnumeration(true);
+ }
+ else if (hasImplementationOfMethod("iterator", "java.util.Iterator", type_of_domain))
+ {
+ code = getForallCheckCode_OverIterator(true);
+ }
+ else
+ {
+ String dd = getQuantificationDomain().trim();
+ log
+ .warn("The type of "
+ + dd
+ + " in "
+ + ((CodeMetaclass) subject_).getSignature()
+ + " is "
+ + type_of_domain
+ + "\n"
+ + "Complete assertion: "
+ + subject_
+ + "\nQuantifier domains must be: Array, Range (e.g. a .. b [by c]), Enumeration, Iterator or implementation thereof or\nimplementors of 'Enumeration elements()' or 'Iterator iterator()' (e.g. the Java 2 Collections, JDK 1.1 Vector, etc.)\n"
+ + "As a best effort will use java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
+ code = getForallCheckCode_OverEnumeration(false);
+ }
}
- }
- catch (UnableToDetermineTypeException e) {
- String dd = getQuantificationDomain().trim();
- log.warn("Could not determine type of " + dd + " in " + ((CodeMetaclass)subject_).getSignature() + "\n" + "Complete assertion: " + subject_ + "\n" + "Using java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
- log.warn(e.getMessage());
- code = getForallCheckCode_OverEnumeration(false);
- }
- }
- return code;
- }
+ catch (UnableToDetermineTypeException e)
+ {
+ String dd = getQuantificationDomain().trim();
+ log
+ .warn("Could not determine type of "
+ + dd
+ + " in "
+ + ((CodeMetaclass) subject_).getSignature()
+ + "\n"
+ + "Complete assertion: "
+ + subject_
+ + "\n"
+ + "Using java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
+ log.warn(e.getMessage());
+ code = getForallCheckCode_OverEnumeration(false);
+ }
+ }
+ return code;
+ }
- private String getForallCheckCode_OverArray() {
- String code = "";
- String elementType = getElementType();
- String elementVar = getElementVar();
- String indexVar = "__index_" + getMangledValue(getElementVar());
- String resultVar = "__result_" + getMangledValue(getElementVar());
- String quantificationDomain = getQuantificationDomain();
- String quantifiedExpression = getQuantifiedExpression();
- code = code + "boolean " + resultVar + "=true;\n";
- code = code + "for ( int " + indexVar + "= 0; " + indexVar + " < " + quantificationDomain + ".length; " + indexVar + "++){\n";
- code = code + " " + elementType + " " + elementVar + "= " + quantificationDomain + "[" + indexVar + "];\n";
- AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
- if (subassert.includesQuantifier()) {
- code = code + subassert.getPartialCheckCode();
- String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
- code = code + resultVar + "=" + resultVar + " && " + subresultVar + ";\n";
- } else
- if (containsImplies(quantifiedExpression)) {
- code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression) + " )) // implication condition\n";
- code = code + " { } // implication evaluates to true, does not affect return\n";
- code = code + "else {\n";
- code = code + " " + resultVar + "=" + resultVar + " && (" + getImplication(quantifiedExpression) + " ); // the implication \n";
- code = code + "}\n";
- } else {
- code = code + " " + resultVar + "=" + resultVar + " && (" + quantifiedExpression + ");\n";
- }
- code = code + "}\n";
- return code;
- }
+ private String getForallCheckCode_OverArray()
+ {
+ String code = "";
+ String elementType = getElementType();
+ String elementVar = getElementVar();
+ String indexVar = "__index_" + getMangledValue(getElementVar());
+ String resultVar = "__result_" + getMangledValue(getElementVar());
+ String quantificationDomain = getQuantificationDomain();
+ String quantifiedExpression = getQuantifiedExpression();
+ code = code + "boolean " + resultVar + "=true;\n";
+ code = code + "for ( int " + indexVar + "= 0; " + indexVar + " < " + quantificationDomain + ".length; "
+ + indexVar + "++){\n";
+ code = code + " " + elementType + " " + elementVar + "= " + quantificationDomain + "[" + indexVar + "];\n";
+ AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
+ if (subassert.includesQuantifier())
+ {
+ code = code + subassert.getPartialCheckCode();
+ String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
+ code = code + resultVar + "=" + resultVar + " && " + subresultVar + ";\n";
+ }
+ else if (containsImplies(quantifiedExpression))
+ {
+ code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression)
+ + " )) // implication condition\n";
+ code = code + " { } // implication evaluates to true, does not affect return\n";
+ code = code + "else {\n";
+ code = code + " " + resultVar + "=" + resultVar + " && (" + getImplication(quantifiedExpression)
+ + " ); // the implication \n";
+ code = code + "}\n";
+ }
+ else
+ {
+ code = code + " " + resultVar + "=" + resultVar + " && (" + quantifiedExpression + ");\n";
+ }
+ code = code + "}\n";
+ return code;
+ }
- private String getForallCheckCode_OverEnumeration(boolean enumerationImpl) {
- String code = "";
- String elementType = getElementType();
- String castElementType = elementType;
- if (elementType.equals("int")) {
- castElementType = "Integer";
- }
- if (elementType.equals("float")) {
- castElementType = "Float";
- }
- if (elementType.equals("boolean")) {
- castElementType = "Boolean";
- }
- if (elementType.equals("byte")) {
- castElementType = "Byte";
- }
- if (elementType.equals("double")) {
- castElementType = "Double";
- }
- if (elementType.equals("long")) {
- castElementType = "Long";
- }
- if (elementType.equals("short")) {
- castElementType = "Short";
- }
- if (elementType.equals("char")) {
- castElementType = "Character";
- }
- String enumVar = "__" + getMangledValue(getElementVar()) + "_enum";
- String elementVar = getElementVar();
- String resultVar = "__result_" + getMangledValue(getElementVar());
- String quantificationDomain = getQuantificationDomain();
- String quantifiedExpression = getQuantifiedExpression();
- code = code + "boolean " + resultVar + "=true;\n";
- String postfix = "";
- if (enumerationImpl) {
- postfix = ".elements()";
- }
- code = code + "for (java.util.Enumeration " + enumVar + "=" + quantificationDomain + postfix + ";\n";
- code = code + " " + enumVar + ".hasMoreElements() && " + resultVar + "; ){\n";
- code = code + " " + castElementType + " " + elementVar + "=(";
- code = code + castElementType + ")(" + enumVar + ".nextElement());\n";
- AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
- if (subassert.includesQuantifier()) {
- code = code + subassert.getPartialCheckCode();
- String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
- code = code + resultVar + "=" + resultVar + " && " + subresultVar + ";\n";
- } else
- if (containsImplies(quantifiedExpression)) {
- code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression) + " )) // implication condition\n";
- code = code + " { } // implication evaluates to true, does not affect return\n";
- code = code + "else {\n";
- code = code + " " + resultVar + "=" + resultVar + " && (" + getImplication(quantifiedExpression) + " ); // the implication \n";
- code = code + "}\n";
- } else {
- code = code + " " + resultVar + "=" + resultVar + " && (" + quantifiedExpression + ");\n";
- }
- code = code + "}\n";
- return code;
- }
+ private String getForallCheckCode_OverEnumeration(boolean enumerationImpl)
+ {
+ String code = "";
+ String elementType = getElementType();
+ String castElementType = elementType;
+ if (elementType.equals("int"))
+ {
+ castElementType = "Integer";
+ }
+ if (elementType.equals("float"))
+ {
+ castElementType = "Float";
+ }
+ if (elementType.equals("boolean"))
+ {
+ castElementType = "Boolean";
+ }
+ if (elementType.equals("byte"))
+ {
+ castElementType = "Byte";
+ }
+ if (elementType.equals("double"))
+ {
+ castElementType = "Double";
+ }
+ if (elementType.equals("long"))
+ {
+ castElementType = "Long";
+ }
+ if (elementType.equals("short"))
+ {
+ castElementType = "Short";
+ }
+ if (elementType.equals("char"))
+ {
+ castElementType = "Character";
+ }
+ String enumVar = "__" + getMangledValue(getElementVar()) + "_enum";
+ String elementVar = getElementVar();
+ String resultVar = "__result_" + getMangledValue(getElementVar());
+ String quantificationDomain = getQuantificationDomain();
+ String quantifiedExpression = getQuantifiedExpression();
+ code = code + "boolean " + resultVar + "=true;\n";
+ String postfix = "";
+ if (enumerationImpl)
+ {
+ postfix = ".elements()";
+ }
+ code = code + "for (java.util.Enumeration " + enumVar + "=" + quantificationDomain + postfix + ";\n";
+ code = code + " " + enumVar + ".hasMoreElements() && " + resultVar + "; ){\n";
+ code = code + " " + castElementType + " " + elementVar + "=(";
+ code = code + castElementType + ")(" + enumVar + ".nextElement());\n";
+ AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
+ if (subassert.includesQuantifier())
+ {
+ code = code + subassert.getPartialCheckCode();
+ String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
+ code = code + resultVar + "=" + resultVar + " && " + subresultVar + ";\n";
+ }
+ else if (containsImplies(quantifiedExpression))
+ {
+ code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression)
+ + " )) // implication condition\n";
+ code = code + " { } // implication evaluates to true, does not affect return\n";
+ code = code + "else {\n";
+ code = code + " " + resultVar + "=" + resultVar + " && (" + getImplication(quantifiedExpression)
+ + " ); // the implication \n";
+ code = code + "}\n";
+ }
+ else
+ {
+ code = code + " " + resultVar + "=" + resultVar + " && (" + quantifiedExpression + ");\n";
+ }
+ code = code + "}\n";
+ return code;
+ }
- private String getForallCheckCode_OverIterator(boolean iteratorImpl) {
- String code = "";
- String elementType = getElementType();
- String castElementType = elementType;
- if (elementType.equals("int")) {
- castElementType = "Integer";
- }
- if (elementType.equals("float")) {
- castElementType = "Float";
- }
- if (elementType.equals("boolean")) {
- castElementType = "Boolean";
- }
- if (elementType.equals("byte")) {
- castElementType = "Byte";
- }
- if (elementType.equals("double")) {
- castElementType = "Double";
- }
- if (elementType.equals("long")) {
- castElementType = "Long";
- }
- if (elementType.equals("short")) {
- castElementType = "Short";
- }
- if (elementType.equals("char")) {
- castEleme...
[truncated message content] |
×
Want the latest updates on software, tech news, and AI?
Get latest updates about software, tech news, and AI from SourceForge directly in your inbox once a month.
Thanks for helping keep SourceForge clean.
X