001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: package de.uka.ilkd.key.java;
009:
010: import java.io.File;
011:
012: import junit.framework.TestCase;
013: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
014: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
015: import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
016: import de.uka.ilkd.key.proof.ProofAggregate;
017: import de.uka.ilkd.key.util.HelperClassForTests;
018:
019: /**
020: * This class tests several methods of the JavaInfo class
021: */
022: public class TestJavaInfo extends TestCase {
023:
024: public static final String testfile = System
025: .getProperty("key.home")
026: + File.separator
027: + "examples"
028: + File.separator
029: + "_testcase"
030: + File.separator
031: + "javainfo"
032: + File.separator + "testJavaInfo.key";
033:
034: private static Services services;
035: private static JavaInfo javaInfo;
036:
037: private static int down = 0;
038: private static int testcases = 0;
039:
040: public TestJavaInfo() {
041: testcases++;
042: }
043:
044: public void setUp() {
045: if (down != 0)
046: return;
047: HelperClassForTests helper = new HelperClassForTests();
048: final ProofAggregate agg = helper.parse(new File(testfile));
049: services = agg.getFirstProof().getServices();
050: javaInfo = services.getJavaInfo();
051: }
052:
053: public void tearDown() {
054: down++;
055: if (testcases > down)
056: return;
057: services = null;
058: javaInfo = null;
059: }
060:
061: public void testRetrieveArrayTypeByJLSName() {
062: assertTrue("Did not find [I",
063: javaInfo.getKeYJavaType("[I") != null);
064:
065: assertTrue("Did not find [java.lang.Object", javaInfo
066: .getKeYJavaType("[Ljava.lang.Object") != null);
067: }
068:
069: public void testRetrieveArrayTypeByAlternativeName() {
070: assertTrue("Did not find int[]", javaInfo
071: .getKeYJavaType("int[]") != null);
072:
073: assertTrue("Did not find java.lang.Object[]", javaInfo
074: .getKeYJavaType("java.lang.Object[]") != null);
075: }
076:
077: public void testGetAllSubtypes() {
078: assertTrue("No subtypes of java.lang.Object?", javaInfo
079: .getAllSubtypes(services.getJavaInfo()
080: .getJavaLangObject()) != null);
081: // attention this test is not for fun, there are some methods deoending on
082: // this property
083: assertTrue(
084: "The method getAllSubtypes must not contain the type itself",
085: !javaInfo.getAllSubtypes(
086: services.getJavaInfo().getJavaLangObject())
087: .contains(javaInfo.getJavaLangObject()));
088: }
089:
090: public void testGetAllSupertypes() {
091: KeYJavaType rte = javaInfo
092: .getKeYJavaType("java.lang.RuntimeException");
093: assertTrue("Did not find class java.lang.RuntimeException",
094: rte != null);
095: final ListOfKeYJavaType allSupertypes = javaInfo
096: .getAllSupertypes(rte);
097:
098: assertTrue("No supertypes of java.lang.RuntimeException?",
099: allSupertypes != null);
100:
101: assertTrue(
102: "The method getAllSupertypes must contain the type itself",
103: allSupertypes.contains(rte));
104: }
105:
106: public void testFindArrayLength() {
107: KeYJavaType intarray = javaInfo.getKeYJavaType("int[]");
108: assertTrue("Could not find length attribute for arrays: ",
109: javaInfo.getAttribute("length", intarray) != null);
110:
111: }
112:
113: private static final String[] implictFieldsClassOnly = new String[] {
114: ImplicitFieldAdder.IMPLICIT_CLASS_ERRONEOUS,
115: ImplicitFieldAdder.IMPLICIT_CLASS_INIT_IN_PROGRESS,
116: ImplicitFieldAdder.IMPLICIT_CLASS_INITIALIZED,
117: ImplicitFieldAdder.IMPLICIT_CLASS_PREPARED };
118:
119: private static final String[] generalImplicitFields = new String[] {
120: ImplicitFieldAdder.IMPLICIT_CREATED,
121: ImplicitFieldAdder.IMPLICIT_NEXT_TO_CREATE,
122: ImplicitFieldAdder.IMPLICIT_INITIALIZED,
123: ImplicitFieldAdder.IMPLICIT_TRANSIENT };
124:
125: public void testFindImplicitArrayAttributes() {
126: KeYJavaType intarray = javaInfo.getKeYJavaType("int[]");
127: KeYJavaType objarray = javaInfo
128: .getKeYJavaType("java.lang.Object[]");
129:
130: assertTrue("Missing array types", intarray != null
131: && objarray != null);
132:
133: assertTrue("Could not find "
134: + ImplicitFieldAdder.IMPLICT_ARRAY_TRA_INITIALIZED
135: + "attribute for arrays.", javaInfo.getAttribute(
136: ImplicitFieldAdder.IMPLICT_ARRAY_TRA_INITIALIZED,
137: intarray) != null);
138: assertTrue("Could not find "
139: + ImplicitFieldAdder.IMPLICT_ARRAY_TRA_INITIALIZED
140: + "attribute for arrays.", javaInfo.getAttribute(
141: ImplicitFieldAdder.IMPLICT_ARRAY_TRA_INITIALIZED,
142: objarray) != null);
143:
144: for (int i = 0; i < generalImplicitFields.length; i++) {
145: assertTrue("Could not find " + generalImplicitFields[i]
146: + "attribute for arrays.", javaInfo
147: .lookupVisibleAttribute(generalImplicitFields[i],
148: intarray) != null);
149: assertTrue("Could not find " + generalImplicitFields[i]
150: + "attribute for arrays.", javaInfo
151: .lookupVisibleAttribute(generalImplicitFields[i],
152: objarray) != null);
153: }
154: }
155:
156: public void testFindImplicitAttributesForClassTypesOnly() {
157: KeYJavaType obj = javaInfo.getKeYJavaType("java.lang.Object");
158: for (int i = 0; i < generalImplicitFields.length; i++) {
159: assertTrue("Could not find " + generalImplicitFields[i]
160: + "attribute for arrays.", javaInfo
161: .lookupVisibleAttribute(generalImplicitFields[i],
162: obj) != null);
163: }
164: for (int i = 0; i < implictFieldsClassOnly.length; i++) {
165: assertTrue("Could not find " + implictFieldsClassOnly[i]
166: + "attribute for arrays.", javaInfo
167: .lookupVisibleAttribute(implictFieldsClassOnly[i],
168: obj) != null);
169: }
170: }
171:
172: /**
173: * Important getAttribute methods of javaInfo must return only local declared
174: * attributes
175: *
176: */
177: public void testFindAttributesLocallyDeclaredOnly() {
178: KeYJavaType obj = javaInfo.getKeYJavaType("java.lang.Object");
179:
180: KeYJavaType rte = javaInfo
181: .getKeYJavaType("java.lang.RuntimeException");
182:
183: assertTrue(
184: "Did not find locally declared attribute "
185: + ImplicitFieldAdder.IMPLICIT_CREATED,
186: javaInfo.getAttribute(
187: ImplicitFieldAdder.IMPLICIT_CREATED, obj) != null);
188:
189: assertTrue(
190: "Attribute "
191: + ImplicitFieldAdder.IMPLICIT_CREATED
192: + " is locally declared in class java.lang.Object and should not be "
193: + "returned by this method for type java.lang.RuntimeException",
194: javaInfo.getAttribute(
195: ImplicitFieldAdder.IMPLICIT_CREATED, rte) == null);
196:
197: }
198:
199: /**
200: * tests if the common subtypes of two sorts are correctly determined
201: */
202: public void testGetCommonSubtypes() {
203:
204: final KeYJavaType ae = javaInfo
205: .getKeYJavaType("java.lang.ArithmeticException");
206: final KeYJavaType npe = javaInfo
207: .getKeYJavaType("java.lang.NullPointerException");
208:
209: assertTrue(javaInfo.getCommonSubtypes(ae, npe).size() == 0);
210:
211: final KeYJavaType obj = javaInfo
212: .getKeYJavaType("java.lang.Object");
213: final KeYJavaType rte = javaInfo
214: .getKeYJavaType("java.lang.RuntimeException");
215:
216: long start = System.currentTimeMillis();
217:
218: final ListOfKeYJavaType commons = javaInfo.getCommonSubtypes(
219: obj, rte);
220: assertTrue(commons.equals(javaInfo.getAllSubtypes(rte).prepend(
221: rte)));
222:
223: long end = System.currentTimeMillis();
224: final long duration = end - start;
225:
226: // test caching
227: long durationCache = 0;
228: for (int i = 0; i < 1000; i++) {
229: start = System.currentTimeMillis();
230: final ListOfKeYJavaType commonsCache = javaInfo
231: .getCommonSubtypes(obj, rte);
232: end = System.currentTimeMillis();
233: assertTrue("Cache inconsistence", commonsCache
234: .equals(commons));
235: durationCache += end - start;
236: }
237: assertTrue("Performance problem with caching common subsorts",
238: durationCache / 1000 < duration || duration == 0
239: && durationCache / 1000 == 0);
240:
241: }
242:
243: /**
244: * test getPrimtiveKeYJavaType
245: */
246: public void testGetPrimitiveKJT() {
247: final String[] primitiveTypeNames = new String[] { "long",
248: "int", "short", "byte", "char", "boolean" };
249:
250: for (int i = 0; i < primitiveTypeNames.length; i++) {
251: assertNotNull(
252: "Type" + primitiveTypeNames[i] + " not found",
253: javaInfo
254: .getPrimitiveKeYJavaType(primitiveTypeNames[i]));
255: }
256:
257: assertNull("Ooops, non primitive type found", javaInfo
258: .getPrimitiveKeYJavaType("java.lang.Object"));
259: assertNull("Ooops, non existing type found", javaInfo
260: .getPrimitiveKeYJavaType("myOwnType"));
261: }
262:
263: }
|