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: // This file is part of KeY - Integrated Deductive Software Design
010: // Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
011: // and Chalmers University of Technology, Sweden
012: //
013: // The KeY system is protected by the GNU General Public License.
014: // See LICENSE.TXT for details.
015: //
016:
017: package de.uka.ilkd.key.parser.jml;
018:
019: import de.uka.ilkd.key.jml.WrongIntSemanticsException;
020: import de.uka.ilkd.key.logic.Name;
021: import de.uka.ilkd.key.logic.Namespace;
022: import de.uka.ilkd.key.logic.op.Function;
023:
024: public class DefaultArithOpProvider implements ArithOpProvider {
025:
026: protected Namespace functions;
027: private boolean javaSemantics;
028:
029: public DefaultArithOpProvider(Namespace functions,
030: boolean javaSemantics) {
031: this .functions = functions;
032: this .javaSemantics = javaSemantics;
033: }
034:
035: public Namespace getFunctions() {
036: return functions;
037: }
038:
039: public void setFunctions(Namespace functions) {
040: this .functions = functions;
041: }
042:
043: public Function getMin(boolean l) {
044: return getFunction(l, "long_MIN", "int_MIN", null, "minimum");
045: }
046:
047: public Function getMax(boolean l) {
048: return getFunction(l, "long_MAX", "int_MAX", null, "maximum");
049: }
050:
051: public Function getAdd(boolean l) {
052: return getFunction(l, "addJlong", "addJint", "add", "addition");
053: }
054:
055: public Function getSub(boolean l) {
056: return getFunction(l, "subJlong", "subJint", "sub",
057: "subtraction");
058: }
059:
060: public Function getMinus(boolean l) {
061: return getFunction(l, "unaryMinusJlong", "unaryMinusJint",
062: "neg", "negation");
063: }
064:
065: public Function getMul(boolean l) {
066: return getFunction(l, "mulJlong", "mulJint", "mul",
067: "multiplication");
068: }
069:
070: public Function getDiv(boolean l) {
071: return getFunction(l, "divJlong", "divJint", "jdiv", "division");
072: }
073:
074: public Function getMod(boolean l) {
075: return getFunction(l, "modJlong", "modJint", "jmod", "modulo");
076: }
077:
078: public Function getOr(boolean l) {
079: return getFunction(l, "orJlong", "orJint", "binaryOr",
080: "bitwise or");
081: }
082:
083: public Function getAnd(boolean l) {
084: return getFunction(l, "andJlong", "andJint", "binaryAnd",
085: "bitwise and");
086: }
087:
088: public Function getXor(boolean l) {
089: return getFunction(l, "xorJlong", "xorJint", "binaryXor",
090: "bitwise xor");
091: }
092:
093: public Function getNeg(boolean l) {
094: return getFunction(l, "negJlong", "negJint", "invertBits",
095: "bitwise negation");
096: }
097:
098: public Function getShiftRight(boolean l) {
099: return getFunction(l, "shiftrightJlong", "shiftrightJint",
100: "binaryShiftRight", "shift right");
101: }
102:
103: public Function getShiftLeft(boolean l) {
104: return getFunction(l, "shiftleftJlong", "shiftleftJint",
105: "binaryShiftLeft", "shift left");
106: }
107:
108: public Function getUnsignedShiftRight(boolean l) {
109: return getFunction(l, "unsignedshiftrightJlong",
110: "unsignedshiftrightJint", "binaryUnsignedShiftRight",
111: "unsigned shift right");
112: }
113:
114: public Function getCastToByte() {
115: return (Function) functions.lookup(new Name("moduloByte"));
116: }
117:
118: public Function getCastToShort() {
119: return (Function) functions.lookup(new Name("moduloShort"));
120: }
121:
122: public Function getCastToInt() {
123: return (Function) functions.lookup(new Name("moduloInt"));
124: }
125:
126: public Function getCastToLong() {
127: return (Function) functions.lookup(new Name("moduloLong"));
128: }
129:
130: private Function getFunction(boolean l, String sLong, String sInt,
131: String sDefault, String description) {
132: Function f = null;
133: if (javaSemantics) {
134: if (l) {
135: f = (Function) functions.lookup(new Name(sLong));
136: } else {
137: f = (Function) functions.lookup(new Name(sInt));
138: }
139: } else {
140: f = (Function) functions.lookup(new Name(sDefault));
141: }
142:
143: if (f == null) {
144: throw new WrongIntSemanticsException(description);
145: }
146: return f;
147: }
148:
149: }
|