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.ProgramElement;
14: import de.uka.ilkd.key.java.Services;
15: import de.uka.ilkd.key.java.declaration.ArrayOfModifier;
16: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
17: import de.uka.ilkd.key.java.declaration.VariableSpecification;
18: import de.uka.ilkd.key.java.reference.TypeRef;
19: import de.uka.ilkd.key.java.reference.TypeReference;
20: import de.uka.ilkd.key.logic.Name;
21: import de.uka.ilkd.key.logic.op.ProgramSV;
22: import de.uka.ilkd.key.logic.op.SchemaVariable;
23: import de.uka.ilkd.key.rule.inst.SVInstantiations;
24:
25: public class ArrayPostDecl extends ProgramMetaConstruct {
26:
27: public ArrayPostDecl(SchemaVariable sv) {
28: super (new Name("array-post-declaration"), (ProgramSV) sv);
29: }
30:
31: /**
32: * Replaces a local variable declaration <code> #t #v[]; </code> with
33: * <code>#t[] #v;</code>
34: * @param services the Services with all necessary information
35: * about the java programs
36: * @param svInst the instantiations of the schema variables
37: * @return the transformed program
38: */
39: public ProgramElement symbolicExecution(ProgramElement pe,
40: Services services, SVInstantiations svInst) {
41:
42: final LocalVariableDeclaration declaration = (LocalVariableDeclaration) pe;
43: final ArrayOfModifier modifiers = declaration.getModifiers();
44: final TypeReference originalTypeReference = declaration
45: .getTypeReference();
46: /* Debug.assertTrue
47: (declaration.getVariables().size() == 1,
48: "ArrayPostDecl metaconsstruct can only treat single variable declarations");*/
49: final VariableSpecification var = declaration.getVariables()
50: .getVariableSpecification(0);
51:
52: final TypeReference newTypeReference = new TypeRef(
53: originalTypeReference.getProgramElementName(),
54: originalTypeReference.getDimensions()
55: + var.getDimensions(), originalTypeReference
56: .getReferencePrefix(), var.getProgramVariable()
57: .getKeYJavaType());
58:
59: final VariableSpecification newVar = new VariableSpecification(
60: var.getProgramVariable(), 0, var.getInitializer(), var
61: .getType());
62:
63: return new LocalVariableDeclaration(modifiers,
64: newTypeReference, newVar);
65:
66: }
67:
68: }
|