01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.rule.metaconstruct;
12:
13: import de.uka.ilkd.key.java.*;
14: import de.uka.ilkd.key.java.declaration.*;
15: import de.uka.ilkd.key.java.reference.TypeReference;
16: import de.uka.ilkd.key.logic.Name;
17: import de.uka.ilkd.key.logic.op.ProgramSV;
18: import de.uka.ilkd.key.logic.op.SchemaVariable;
19: import de.uka.ilkd.key.rule.inst.SVInstantiations;
20:
21: public class MultipleVarDecl extends ProgramMetaConstruct {
22:
23: public MultipleVarDecl(SchemaVariable sv) {
24: super (new Name("multiple-var-decl"), (ProgramSV) sv);
25: }
26:
27: /**
28: * Replaces a declaration of multiple variables by two variable
29: * declarations where the first one declares a single variable
30: * and the second one the remaining variables.
31: * @param services the Services with all necessary information
32: * about the java programs
33: * @param svInst the instantiations esp. of the inner and outer label
34: * @return the transformed program
35: */
36: public ProgramElement symbolicExecution(ProgramElement pe,
37: Services services, SVInstantiations svInst) {
38: VariableDeclaration vardecl = (VariableDeclaration) pe;
39: ArrayOfModifier modifiers = vardecl.getModifiers();
40: TypeReference tref = vardecl.getTypeReference();
41: ArrayOfVariableSpecification variables = vardecl.getVariables();
42: VariableSpecification headVar = variables
43: .getVariableSpecification(0);
44: VariableSpecification[] tailVars = new VariableSpecification[variables
45: .size() - 1];
46:
47: for (int i = 0; i < variables.size() - 1; i++)
48: tailVars[i] = variables.getVariableSpecification(i + 1);
49:
50: if (pe instanceof LocalVariableDeclaration) {
51: LocalVariableDeclaration newVarDecl = new LocalVariableDeclaration(
52: modifiers, tref, headVar);
53: LocalVariableDeclaration newVarDeclList = new LocalVariableDeclaration(
54: modifiers, tref, tailVars);
55: return new StatementBlock(new ArrayOfStatement(
56: new Statement[] { newVarDecl, newVarDeclList }));
57: }
58: throw new RuntimeException(
59: "Meta-construct MultipleVarDecl could "
60: + "not handle program element " + pe);
61: }
62:
63: }
|