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: package de.uka.ilkd.key.rule.metaconstruct.arith;
11:
12: import java.math.BigInteger;
13:
14: import de.uka.ilkd.key.java.Services;
15: import de.uka.ilkd.key.java.expression.literal.IntLiteral;
16: import de.uka.ilkd.key.logic.Name;
17: import de.uka.ilkd.key.logic.Term;
18: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
19: import de.uka.ilkd.key.rule.inst.SVInstantiations;
20:
21: /** this class implements the interface for
22: * MetaAdderators. MetaAdderators are used to do complex term
23: * transformation when applying a taclet. Often these transformation
24: * caanot be described with the taclet scheme (or trying to do so would
25: * result in a huge number of rules)
26: */
27: public class MetaJavaLongUnsignedShiftRight extends
28: AbstractMetaOperator {
29:
30: public MetaJavaLongUnsignedShiftRight() {
31: super (new Name("#JavaLongUnsignedShiftRight"), 2);
32: }
33:
34: /**
35: * checks whether the top level structure of the given @link Term
36: * is syntactically valid, given the assumption that the top level
37: * operator of the term is the same as this Operator. The
38: * assumption that the top level operator and the term are equal
39: * is NOT checked.
40: * @return true iff the top level structure of
41: * the @link Term is valid.
42: */
43: public boolean validTopLevel(Term term) {
44: // a meta operator accepts almost everything
45: return term.op() instanceof MetaJavaLongUnsignedShiftRight
46: && term.arity() == arity();
47: }
48:
49: /** calculates the resulting term. */
50: public Term calculate(Term term, SVInstantiations svInst,
51: Services services) {
52: Term arg1 = term.sub(0);
53: Term arg2 = term.sub(1);
54: BigInteger intArg1 = null;
55: BigInteger intArg2 = null;
56:
57: intArg1 = new BigInteger(convertToDecimalString(arg1, services));
58: intArg2 = new BigInteger(convertToDecimalString(arg2, services));
59: Long longResult = new Long(intArg1.longValue() >>> intArg2
60: .longValue());
61:
62: IntLiteral lit = new IntLiteral(longResult.toString());
63: return services.getTypeConverter().convertToLogicElement(lit);
64:
65: }
66:
67: }
|