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: //
009: //
010:
011: package de.uka.ilkd.key.java;
012:
013: import java.io.FileReader;
014: import java.io.IOException;
015:
016: import junit.framework.TestCase;
017: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
018: import de.uka.ilkd.key.java.abstraction.PrimitiveType;
019: import de.uka.ilkd.key.java.expression.Operator;
020: import de.uka.ilkd.key.logic.JavaBlock;
021: import de.uka.ilkd.key.logic.NamespaceSet;
022: import de.uka.ilkd.key.logic.ProgramElementName;
023: import de.uka.ilkd.key.logic.op.ListOfProgramVariable;
024: import de.uka.ilkd.key.logic.op.LocationVariable;
025: import de.uka.ilkd.key.logic.op.ProgramVariable;
026: import de.uka.ilkd.key.logic.op.SLListOfProgramVariable;
027: import de.uka.ilkd.key.rule.TacletForTests;
028:
029: public class TestRecoder2KeY extends TestCase {
030:
031: public TestRecoder2KeY(String name) {
032: super (name);
033: }
034:
035: private Recoder2KeY c2k;
036:
037: // some non sense java blocks with lots of statements and expressions
038: private static String[] jblocks = new String[] {
039: "{int j=7; int i;\n i=1; double d=0.4; float f=1.445; long l=123; \n "
040: + "for (i=0, j=1; (i<42) && (i>0); i++, j--)\n"
041: + " { i=13; j=1; } "
042: + "while ((-i<7) || (i++==7--) | (--i==++7) ||(!true && false) ||"
043: + " ('a'=='d') "
044: + "|| (\"asd\"==\"as\"+\"d\") & (d==f) ^ (d/f+2>=f*d-f%d)|| (l<=~i)"
045: + " || !(this==null) || ((this!=null) ? (8<<j<8>>i) : (7&5>8>>>7L)"
046: + " || (7|5!=8^4)) && i+=j && i=j && i/=j && i%=j && i-=j && i*=j"
047: + " && i<<=j && i>>=j && i>>>=j && i&=j && i^=j && i|=j) j=7;"
048: + "}",
049:
050: "{"
051: + "int j=7; int i;\n i=1;"
052: + "do { j++; } while (i==1);"
053: + "if (j==42) j=7; else {i=7; j=43;}"
054: + ";;"
055: + "label0: j=42;"
056: + "switch (j-i) {case 7: j=2; case 42: j=3; default: j=4; }"
057: + "while (j==42) loop1:{ if (j==7) break; if (j==43) break loop1;"
058: + "if (j==42) continue; if (j==41) continue loop1;}"
059: + "if (j>42) return;"
060: + "synchronized(null) { j=7; }" + "}",
061: "{ int x = 1; {Boolean b;} }",
062: "{"
063: + "int[] a; a=new int[3]; a=new int[]{2,3,4}; int j=a[2]; j=a.length;"
064: + "}"
065:
066: };
067:
068: private static String[] jclasses = new String[] {
069: "class A1 { public A1() { }} ",
070: "package qwe.rty; import uio.pas; import dfg.hjk.*; import java.util.*;"
071: + "public abstract class A implements Z{"
072: + "static {d=3; Vector v = new Vector();}"
073: + "public static int d;"
074: + "A (int j) { d=5; }"
075: + "public A (int j, float k) {this(j); d=5; }"
076: + "private static final A[] b=new A[]{null}; "
077: + "float f; Boolean s;"
078: + "public void abc() {"
079: + "Object z=new A(4, 5) { public int d=7; };"
080: + "abc(); A a=(A)null; a=def(a); a=def(a).ghi(a).ghi(a);}"
081: + "{ int x = 1; {int i = \"\\\".length}\"; } }"
082: + "protected A def(A a) {a=ghi(a); return new A(3);}"
083: + "private synchronized A ghi(A a) { a=ghi(a); ghi(a); A a1=null; "
084: + " a1=ghi(a1); a=def(a); return null;}"
085: + "protected abstract int[] jkl(A a, int i);"
086: + "protected Object o() {if (s instanceof Class) return s.class;}"
087: + "}"
088: + "interface Z { public int d=0; }"
089: + "interface Z0 extends Z {}"
090: + "class A1 extends A { public static A a=new A(4); "
091: + "A1 (int j) {super(j);} }",
092: "public class B extends Object {"
093: + "class E { public E(Class s) {super();} }" + "}",
094: " class circ_A { static int a = circ_B.b; } "
095: + "class circ_B { static int b = circ_A.a; }",
096: " class circ2_A { static final int a = circ2_B.b; } " // This fails for an
097: + "class circ2_B { static final int b = circ2_A.a; }" // unpatched recoder library
098: };
099:
100: /** removes blanks and line feeds from a given string*/
101: private static String removeBlanks(String s) {
102: StringBuffer sb = new StringBuffer();
103: for (int i = 0; i < s.length(); i++) {
104: if (!(s.charAt(i) == (' ')) && !(s.charAt(i) == ('\n')))
105: sb.append(s.charAt(i));
106: }
107: return sb.toString();
108: }
109:
110: public void setUp() {
111: c2k = new Recoder2KeY(new Services(), new NamespaceSet());
112: }
113:
114: public void tearDown() {
115: c2k = null;
116: }
117:
118: public void testReadBlockWithContext() {
119: ProgramVariable pv = new LocationVariable(
120: new ProgramElementName("i"), new KeYJavaType(
121: PrimitiveType.JAVA_INT));
122: ListOfProgramVariable list = SLListOfProgramVariable.EMPTY_LIST
123: .prepend(pv);
124: JavaBlock block = c2k.readBlock("{ i = 2; }", c2k
125: .createContext(list));
126: ProgramVariable prgVarCmp = (ProgramVariable) ((Operator) ((StatementBlock) block
127: .program()).getStatementAt(0)).getChildAt(0);
128: assertTrue("ProgramVariables should be the same ones.",
129: prgVarCmp == pv);
130: }
131:
132: /** test compares the pretty print results from recoder and KeY modulo
133: * blanks and line feeds
134: */
135: public void testJBlocks() {
136: for (int i = 0; i < jblocks.length; i++) {
137: String keyProg = removeBlanks(c2k
138: .readBlockWithEmptyContext(jblocks[i]).toString());
139: String recoderProg = removeBlanks(c2k.recoderBlock(
140: jblocks[i], c2k.createEmptyContext()).toSource());
141: assertEquals("Block :" + i + " rec:" + recoderProg + "key:"
142: + keyProg, recoderProg, keyProg);
143: }
144: }
145:
146: private void testClass(String is) {
147: c2k = new Recoder2KeY(TacletForTests.services(),
148: new NamespaceSet());
149: CompilationUnit cu = c2k.readCompilationUnit(is);
150:
151: }
152:
153: /** test compares the pretty print results from recoder and KeY modulo
154: * blanks and line feeds
155: */
156: public void testJClasses() {
157: for (int i = 0; i < jclasses.length; i++) {
158: testClass(jclasses[i]);
159: }
160: }
161:
162: /** test compares the pretty print results from recoder and KeY modulo
163: * blanks and line feeds. Input is the Recoder2KeY.java file.
164: * Not working: RECODER does not recognize imports
165: */
166: public void xtestFileInput() {
167: char[] ch = new char[100000];
168: int n = 0;
169: try {
170: FileReader fr = new FileReader(
171: "de/uka/ilkd/key/java/Recoder2KeY.java");
172: n = fr.read(ch);
173: } catch (IOException e) {
174: System.err.println("Recoder2KeY.java not found");
175: }
176: String inputString = new String(ch, 0, n);
177: testClass(inputString);
178:
179: }
180:
181: public static void main(String[] args) {
182: Services services = new Services();
183: Recoder2KeY c2k = new Recoder2KeY(services, new NamespaceSet());
184: recoder.java.StatementBlock jb = c2k
185: .recoderBlock(
186: "{int len; int[] i = new int[] {0,1,2} ; len = i.length;}",
187: c2k.createEmptyContext());
188: System.out.println("Read: " + jb);
189: recoder.java.StatementBlock block = (recoder.java.StatementBlock) jb;
190: recoder.java.ProgramElement pe = block.getChildAt(2);
191: System.out.println("Look at " + pe);
192: // de.uka.ilkd.key.java.CopyAssignment ca = ;
193: // System.out.println("Look at "+pe);
194:
195: }
196: }
|