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: //
012: /**
013: * tests the symbolic execution of the program meta constructs
014: */package de.uka.ilkd.key.rule.metaconstruct;
015:
016: import junit.framework.TestCase;
017: import de.uka.ilkd.key.java.Expression;
018: import de.uka.ilkd.key.java.ProgramElement;
019: import de.uka.ilkd.key.java.Services;
020: import de.uka.ilkd.key.java.StatementBlock;
021: import de.uka.ilkd.key.java.expression.Assignment;
022: import de.uka.ilkd.key.java.reference.TypeRef;
023: import de.uka.ilkd.key.java.statement.Break;
024: import de.uka.ilkd.key.java.statement.LabeledStatement;
025: import de.uka.ilkd.key.java.statement.LoopStatement;
026: import de.uka.ilkd.key.java.visitor.JavaASTCollector;
027: import de.uka.ilkd.key.logic.ProgramElementName;
028: import de.uka.ilkd.key.logic.op.SchemaVariableFactory;
029: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
030: import de.uka.ilkd.key.rule.TacletForTests;
031: import de.uka.ilkd.key.rule.inst.SVInstantiations;
032:
033: public class TestProgramMetaConstructs extends TestCase {
034:
035: public TestProgramMetaConstructs(String name) {
036: super (name);
037: de.uka.ilkd.key.util.Debug.ENABLE_DEBUG = false;
038: }
039:
040: public void setUp() {
041: }
042:
043: public void testDoBreak() {
044: LabeledStatement labeledBlock = (LabeledStatement) ((StatementBlock) TacletForTests
045: .parsePrg
046: //("{l1:l2:{l3:{l4:break l3; int i = 0;} int j=1;}}")).getChildAt(0);
047: ("{l4:break l3; int i = 0; int j=1;}")).getChildAt(0);
048: DoBreak rmLabel = new DoBreak(labeledBlock);
049:
050: ProgramElement result = rmLabel.symbolicExecution(rmLabel
051: .body(), new Services(),
052: SVInstantiations.EMPTY_SVINSTANTIATIONS);
053: assertTrue(result instanceof Break);
054: }
055:
056: /** tests AST walkers */
057: public void xtestASTWalker() {
058: ProgramElement block = TacletForTests
059: .parsePrg("{int a=5; test1:test2:while (true) "
060: + "{test3: {int j=3;}}}");
061: JavaASTCollector coll = new JavaASTCollector(block,
062: de.uka.ilkd.key.java.statement.LabeledStatement.class);
063: coll.start();
064: assertTrue(coll.getNodes().size() == 3);
065:
066: ProgramElement block2 = TacletForTests
067: .parsePrg("{while(true) {if (true) break; else continue;}}");
068: WhileLoopTransformation trans = new WhileLoopTransformation(
069: block2, new ProgramElementName("l1"),
070: new ProgramElementName("l2"));
071: trans.start();
072: System.out.println("Result:" + trans);
073: }
074:
075: public void testTypeOf() { //this is no really sufficient test
076: Services services = new Services();
077: //but I can't access programs here
078: StatementBlock block = (StatementBlock) TacletForTests
079: .parsePrg(" { int i; int j; i=j; }");
080: Expression expr = (Expression) ((Assignment) block
081: .getStatementAt(2)).getChildAt(1);
082: ProgramMetaConstruct typeof = new TypeOf(expr);
083: assertTrue(((TypeRef) typeof.symbolicExecution(expr, services,
084: SVInstantiations.EMPTY_SVINSTANTIATIONS)).getName()
085: .toString().equals("int"));
086: }
087:
088: public void testBugId183() {
089: StatementBlock bl = (StatementBlock) TacletForTests
090: .parsePrg("{ while ( true ) {} }");
091: LoopStatement l = (LoopStatement) bl.getChildAt(0);
092: UnwindLoop wlt = new UnwindLoop(SchemaVariableFactory
093: .createProgramSV(new ProgramElementName("inner"),
094: ProgramSVSort.LABEL, false),
095: SchemaVariableFactory.createProgramSV(
096: new ProgramElementName("outer"),
097: ProgramSVSort.LABEL, false), l);
098:
099: SVInstantiations inst = SVInstantiations.EMPTY_SVINSTANTIATIONS;
100: try {
101: wlt.symbolicExecution(l, new Services(), inst);
102: } catch (java.util.NoSuchElementException e) {
103: assertTrue(
104: " Problem with empty while-blocks. See Bug #183 ",
105: false);
106: }
107:
108: }
109:
110: }
|