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: package de.uka.ilkd.key.logic.ldt;
011:
012: import de.uka.ilkd.key.java.Expression;
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
015: import de.uka.ilkd.key.java.abstraction.PrimitiveType;
016: import de.uka.ilkd.key.java.abstraction.Type;
017: import de.uka.ilkd.key.java.expression.Literal;
018: import de.uka.ilkd.key.java.expression.Operator;
019: import de.uka.ilkd.key.java.expression.literal.CharLiteral;
020: import de.uka.ilkd.key.java.expression.literal.IntLiteral;
021: import de.uka.ilkd.key.java.expression.literal.LongLiteral;
022: import de.uka.ilkd.key.java.expression.operator.*;
023: import de.uka.ilkd.key.java.reference.ExecutionContext;
024: import de.uka.ilkd.key.logic.Name;
025: import de.uka.ilkd.key.logic.Namespace;
026: import de.uka.ilkd.key.logic.Term;
027: import de.uka.ilkd.key.logic.TermFactory;
028: import de.uka.ilkd.key.logic.op.Function;
029: import de.uka.ilkd.key.util.Debug;
030: import de.uka.ilkd.key.util.ExtList;
031:
032: /**
033: * This class inherits from LDT and implements all method that are
034: * necessary to handle integers, shorts and bytes.
035: * It loads the needed rule file and offers method to convert java
036: * number types to their logic counterpart
037: */
038: public abstract class AbstractIntegerLDT extends LDT {
039:
040: /**
041: * Public name constants
042: */
043: public static final String NEGATIVE_LITERAL_STRING = "neglit";
044: public static final Name NUMBERS_NAME = new Name("Z");
045: public static final Name CHAR_ID_NAME = new Name("C");
046:
047: /** the function symbols used to represent literals */
048: protected final Function numbers;
049: protected final Function charID;
050: protected final Function sharp;
051: protected final Function numberSymbol[] = new Function[10];
052:
053: /** the function symbols for the integer operations.
054: * Used as shortcuts.
055: */
056: protected final Function greaterThan;
057: protected final Function greaterOrEquals;
058: protected final Function lessThan;
059: protected final Function lessOrEquals;
060: protected final Function plus;
061: protected final Function minus;
062: protected final Function times;
063: protected final Function divide;
064: protected final Function modulo;
065: protected final Function jDivide;
066: protected final Function jModulo;
067: protected final Function negative;
068: protected final Function negativeNumber;
069: protected final Function unaryMinusJint;
070: protected final Function unaryMinusJlong;
071: protected final Function addJint;
072: protected final Function addJlong;
073: protected final Function subJint;
074: protected final Function subJlong;
075: protected final Function mulJint;
076: protected final Function mulJlong;
077: protected final Function modJint;
078: protected final Function modJlong;
079: protected final Function divJint;
080: protected final Function divJlong;
081: protected final Function shiftrightJint;
082: protected final Function shiftrightJlong;
083: protected final Function shiftleftJint;
084: protected final Function shiftleftJlong;
085: protected final Function unsignedshiftrightJint;
086: protected final Function unsignedshiftrightJlong;
087: protected final Function orJint;
088: protected final Function orJlong;
089: protected final Function andJint;
090: protected final Function andJlong;
091: protected final Function xorJint;
092: protected final Function xorJlong;
093:
094: /** the predicate symbols for being within boundaries*/
095: protected final Function inByte;
096: protected Function inShort;
097: protected Function inInt;
098: protected Function inLong;
099: protected Function inChar;
100:
101: // these functions are used to represent Java operators
102: // the taclets moving an integer expression to logic use them.
103: // At a later stage they are interpreted depending on the chosen
104: // integer semantics.
105: private Function javaUnaryMinusInt;
106: private Function javaUnaryMinusLong;
107: private Function javaBitwiseNegation;
108: private Function javaAddInt;
109: private Function javaAddLong;
110: private Function javaSubInt;
111: private Function javaSubLong;
112: private Function javaMulInt;
113: private Function javaMulLong;
114: private Function javaMod;
115: private Function javaDivInt;
116: private Function javaDivLong;
117: private Function javaShiftRightInt;
118: private Function javaShiftRightLong;
119: private Function javaShiftLeftInt;
120: private Function javaShiftLeftLong;
121: private Function javaUnsignedShiftRightInt;
122: private Function javaUnsignedShiftRightLong;
123: private Function javaBitwiseOrInt;
124: private Function javaBitwiseOrLong;
125: private Function javaBitwiseAndInt;
126: private Function javaBitwiseAndLong;
127: private Function javaBitwiseXOrInt;
128: private Function javaBitwiseXOrLong;
129: private Function javaCastByte;
130: private Function javaCastShort;
131: private Function javaCastInt;
132: private Function javaCastLong;
133: private Function javaCastChar;
134:
135: protected AbstractIntegerLDT(Name name, Namespace sorts,
136: Namespace functions, Type javaType) {
137: super (name, sorts, javaType);
138:
139: numbers = addFunction(functions, NUMBERS_NAME.toString());
140: charID = addFunction(functions, CHAR_ID_NAME.toString());
141: sharp = addFunction(functions, "#");
142: assert sharp.sort() == numbers.argSort(0);
143: for (int i = 0; i < 10; i++) {
144: numberSymbol[i] = addFunction(functions, "" + i);
145: assert numberSymbol[i].sort() == numbers.argSort(0);
146: }
147:
148: greaterThan = addFunction(functions, "gt");
149: greaterOrEquals = addFunction(functions, "geq");
150: lessThan = addFunction(functions, "lt");
151: lessOrEquals = addFunction(functions, "leq");
152: plus = addFunction(functions, "add");
153: minus = addFunction(functions, "sub");
154: times = addFunction(functions, "mul");
155: divide = addFunction(functions, "div");
156: modulo = addFunction(functions, "mod");
157: jDivide = addFunction(functions, "div");
158: jModulo = addFunction(functions, "mod");
159: negative = addFunction(functions, "neg");
160: negativeNumber = addFunction(functions, NEGATIVE_LITERAL_STRING);
161: unaryMinusJint = addFunction(functions, "unaryMinusJint");
162: unaryMinusJlong = addFunction(functions, "unaryMinusJlong");
163: addJint = addFunction(functions, "addJint");
164: addJlong = addFunction(functions, "addJlong");
165: subJint = addFunction(functions, "subJint");
166: subJlong = addFunction(functions, "subJlong");
167: mulJint = addFunction(functions, "mulJint");
168: mulJlong = addFunction(functions, "mulJlong");
169: modJint = addFunction(functions, "modJint");
170: modJlong = addFunction(functions, "modJlong");
171: divJint = addFunction(functions, "divJint");
172: divJlong = addFunction(functions, "divJlong");
173: shiftrightJint = addFunction(functions, "shiftrightJint");
174: shiftrightJlong = addFunction(functions, "shiftrightJlong");
175: shiftleftJint = addFunction(functions, "shiftleftJint");
176: shiftleftJlong = addFunction(functions, "shiftleftJlong");
177: unsignedshiftrightJint = addFunction(functions,
178: "unsignedshiftrightJint");
179: unsignedshiftrightJlong = addFunction(functions,
180: "unsignedshiftrightJlong");
181: orJint = addFunction(functions, "orJint");
182: orJlong = addFunction(functions, "orJlong");
183: andJint = addFunction(functions, "andJint");
184: andJlong = addFunction(functions, "andJlong");
185: xorJint = addFunction(functions, "xorJint");
186: xorJlong = addFunction(functions, "xorJlong");
187:
188: inByte = addFunction(functions, "inByte");
189: inShort = addFunction(functions, "inShort");
190: inInt = addFunction(functions, "inInt");
191: inLong = addFunction(functions, "inLong");
192: inChar = addFunction(functions, "inChar");
193:
194: // functions representing the Java operators directly
195: // these are ximoatised depending on the chosen integer semantics
196: javaUnaryMinusInt = addFunction(functions, "javaUnaryMinusInt");
197: javaUnaryMinusLong = addFunction(functions,
198: "javaUnaryMinusLong");
199: javaBitwiseNegation = addFunction(functions,
200: "javaBitwiseNegation");
201:
202: javaAddInt = addFunction(functions, "javaAddInt");
203: javaAddLong = addFunction(functions, "javaAddLong");
204: javaSubInt = addFunction(functions, "javaSubInt");
205: javaSubLong = addFunction(functions, "javaSubLong");
206: javaMulInt = addFunction(functions, "javaMulInt");
207: javaMulLong = addFunction(functions, "javaMulLong");
208: javaMod = addFunction(functions, "javaMod");
209: javaDivInt = addFunction(functions, "javaDivInt");
210: javaDivLong = addFunction(functions, "javaDivLong");
211: javaShiftRightInt = addFunction(functions, "javaShiftRightInt");
212: javaShiftRightLong = addFunction(functions,
213: "javaShiftRightLong");
214: javaShiftLeftInt = addFunction(functions, "javaShiftLeftInt");
215: javaShiftLeftLong = addFunction(functions, "javaShiftLeftLong");
216: javaUnsignedShiftRightInt = addFunction(functions,
217: "javaUnsignedShiftRightInt");
218: javaUnsignedShiftRightLong = addFunction(functions,
219: "javaUnsignedShiftRightLong");
220: javaBitwiseOrInt = addFunction(functions, "javaBitwiseOrInt");
221: javaBitwiseOrLong = addFunction(functions, "javaBitwiseOrLong");
222: javaBitwiseAndInt = addFunction(functions, "javaBitwiseAndInt");
223: javaBitwiseAndLong = addFunction(functions,
224: "javaBitwiseAndLong");
225: javaBitwiseXOrInt = addFunction(functions, "javaBitwiseXOrInt");
226: javaBitwiseXOrLong = addFunction(functions,
227: "javaBitwiseXOrLong");
228: javaCastByte = addFunction(functions, "javaCastByte");
229: javaCastShort = addFunction(functions, "javaCastShort");
230: javaCastInt = addFunction(functions, "javaCastInt");
231: javaCastLong = addFunction(functions, "javaCastLong");
232: javaCastChar = addFunction(functions, "javaCastChar");
233:
234: }
235:
236: /** returns the function symbol for the given operation
237: * null if no function is found for the given operator
238: * @return the function symbol for the given operation
239: */
240: public Function getFunctionFor(
241: de.uka.ilkd.key.java.expression.Operator op, Services serv,
242: ExecutionContext ec) {
243: final KeYJavaType opReturnType = op.getKeYJavaType(serv, ec);
244:
245: if (op instanceof GreaterThan) {
246: return greaterThan;
247: } else if (op instanceof GreaterOrEquals) {
248: return greaterOrEquals;
249: } else if (op instanceof LessThan) {
250: return lessThan;
251: } else if (op instanceof LessOrEquals) {
252: return lessOrEquals;
253: } else if (op instanceof Divide) {
254: return opReturnType.getJavaType() == PrimitiveType.JAVA_LONG ? getJavaDivLong()
255: : getJavaDivInt();
256: } else if (op instanceof Times) {
257: return opReturnType.getJavaType() == PrimitiveType.JAVA_LONG ? getJavaMulLong()
258: : getJavaMulInt();
259: } else if (op instanceof Plus) {
260: return opReturnType.getJavaType() == PrimitiveType.JAVA_LONG ? getJavaAddLong()
261: : getJavaAddInt();
262: } else if (op instanceof Minus) {
263: return opReturnType.getJavaType() == PrimitiveType.JAVA_LONG ? getJavaSubLong()
264: : getJavaSubInt();
265: } else if (op instanceof Modulo) {
266: return getJavaMod();
267: } else if (op instanceof ShiftLeft) {
268: return opReturnType.getJavaType() == PrimitiveType.JAVA_LONG ? getJavaShiftLeftLong()
269: : getJavaShiftLeftInt();
270: } else if (op instanceof ShiftRight) {
271: return opReturnType.getJavaType() == PrimitiveType.JAVA_LONG ? getJavaShiftRightLong()
272: : getJavaShiftRightInt();
273: } else if (op instanceof UnsignedShiftRight) {
274: return opReturnType.getJavaType() == PrimitiveType.JAVA_LONG ? getJavaUnsignedShiftRightLong()
275: : getJavaUnsignedShiftRightInt();
276: } else if (op instanceof BinaryAnd) {
277: assert opReturnType.getJavaType() != PrimitiveType.JAVA_BOOLEAN;
278: return opReturnType.getJavaType() == PrimitiveType.JAVA_LONG ? getJavaBitwiseAndLong()
279: : getJavaBitwiseAndInt();
280: } else if (op instanceof BinaryNot) {
281: assert opReturnType.getJavaType() != PrimitiveType.JAVA_BOOLEAN;
282: return getJavaBitwiseNegation();
283: } else if (op instanceof BinaryOr) {
284: assert opReturnType.getJavaType() != PrimitiveType.JAVA_BOOLEAN;
285: return opReturnType.getJavaType() == PrimitiveType.JAVA_LONG ? getJavaBitwiseOrLong()
286: : getJavaBitwiseOrInt();
287: } else if (op instanceof BinaryXOr) {
288: assert opReturnType.getJavaType() != PrimitiveType.JAVA_BOOLEAN;
289: return opReturnType.getJavaType() == PrimitiveType.JAVA_LONG ? getJavaBitwiseOrLong()
290: : getJavaBitwiseOrInt();
291: } else if (op instanceof Negative) {
292: return opReturnType.getJavaType() == PrimitiveType.JAVA_LONG ? getJavaUnaryMinusLong()
293: : getJavaUnaryMinusLong();
294: } else if (op instanceof TypeCast) {
295: if (opReturnType.getJavaType() == PrimitiveType.JAVA_CHAR) {
296: return getJavaCastChar();
297: } else if (opReturnType.getJavaType() == PrimitiveType.JAVA_BYTE) {
298: return getJavaCastByte();
299: } else if (opReturnType.getJavaType() == PrimitiveType.JAVA_SHORT) {
300: return getJavaCastShort();
301: } else if (opReturnType.getJavaType() == PrimitiveType.JAVA_INT) {
302: return getJavaCastInt();
303: } else if (opReturnType.getJavaType() == PrimitiveType.JAVA_LONG) {
304: return getJavaCastLong();
305: }
306: }
307: return null;
308: }
309:
310: /** returns true if the LDT offers an operation for the given java
311: * operator and the logic subterms
312: * @param op the de.uka.ilkd.key.java.expression.Operator to
313: * translate
314: * @param subs the logic subterms of the java operator
315: * @return true if the LDT offers an operation for the given java
316: * operator and the subterms
317: */
318: public boolean isResponsible(Operator op, Term[] subs,
319: Services services, ExecutionContext ec) {
320: if (subs.length == 1) {
321: return isResponsible(op, subs[0], services, ec);
322: } else if (subs.length == 2) {
323: return isResponsible(op, subs[0], subs[1], services, ec);
324: }
325: return false;
326: }
327:
328: /** returns true if the LDT offers an operation for the given
329: * binary java operator and the logic subterms
330: * @param op the de.uka.ilkd.key.java.expression.Operator to
331: * translate
332: * @param left the left subterm of the java operator
333: * @param right the right subterm of the java operator
334: * @return true if the LDT offers an operation for the given java
335: * operator and the subterms
336: */
337: public boolean isResponsible(Operator op, Term left, Term right,
338: Services services, ExecutionContext ec) {
339: if (left != null && left.sort().extendsTrans(targetSort())
340: && right != null
341: && right.sort().extendsTrans(targetSort())) {
342: if (getFunctionFor(op, services, ec) != null) {
343: return true;
344: }
345: }
346: return false;
347: }
348:
349: /** returns true if the LDT offers an operation for the given
350: * unary java operator and the logic subterms
351: * @param op the de.uka.ilkd.key.java.expression.Operator to
352: * translate
353: * @param sub the logic subterms of the java operator
354: * @return true if the LDT offers an operation for the given java
355: * operator and the subterm
356: */
357: public boolean isResponsible(Operator op, Term sub,
358: Services services, ExecutionContext ec) {
359: if (sub != null && sub.sort().extendsTrans(targetSort())) {
360: if (op instanceof Negative) {
361: return true;
362: }
363: }
364: return false;
365: }
366:
367: /** translates a given integer literal to its logic counterpart
368: * @param lit the Literal to be translated (has to be an
369: * IntLiteral of an LongLiteral
370: * @result the Term that represent the given integer in its logic
371: * form
372: */
373: public Term translateLiteral(Literal lit) {
374: int length = 0;
375: boolean minusFlag = false;
376: Debug.assertTrue(lit instanceof IntLiteral
377: || lit instanceof LongLiteral
378: || lit instanceof CharLiteral, "Literal '" + lit
379: + "' is not an integer literal.");
380:
381: char[] int_ch = null;
382: assert sharp != null;
383: Term result = TermFactory.DEFAULT.createFunctionTerm(sharp);
384:
385: Function identifier = numbers;
386: if (lit instanceof CharLiteral) {
387: lit = new IntLiteral(""
388: + (int) (((CharLiteral) lit).getCharValue()));
389: identifier = charID;
390: }
391:
392: String literalString = "";
393: if (lit instanceof IntLiteral) {
394: literalString = ((IntLiteral) lit).getValue();
395: } else {
396: Debug.assertTrue(lit instanceof LongLiteral);
397: literalString = ((LongLiteral) lit).getValue();
398: }
399:
400: if (literalString.charAt(0) == '-') {
401: minusFlag = true;
402: literalString = literalString.substring(1);
403: }
404: if (lit instanceof IntLiteral) {
405: if (literalString.startsWith("0x")) {
406: try {
407: int i = Integer.parseInt(
408: literalString.substring(2), 16);
409: int_ch = ("" + i).toCharArray();
410: } catch (NumberFormatException nfe) {
411: Debug.fail("Not a hexadecimal constant!");
412: }
413: } else {
414: int_ch = literalString.toCharArray();
415: }
416: length = int_ch.length;
417: } else if (lit instanceof LongLiteral) {
418: if (literalString.startsWith("0x")) {
419: try {
420: // long literals have an 'L' as last sign; we have
421: // to skip it
422: final long l = Long.parseLong(literalString
423: .substring(2, literalString.length() - 1),
424: 16);
425: int_ch = ("" + l).toCharArray();
426: } catch (NumberFormatException nfe) {
427: Debug.fail("Not a hexadecimal constant!");
428: }
429: length = int_ch.length;
430: } else {
431: // long literals have an 'L' as last sign; skip it
432: int_ch = literalString.toCharArray();
433: length = int_ch.length - 1;
434: }
435: }
436:
437: for (int i = 0; i < length; i++) {
438: result = TermFactory.DEFAULT.createFunctionTerm(
439: numberSymbol[int_ch[i] - '0'], result);
440: }
441: if (minusFlag) {
442: result = TermFactory.DEFAULT.createFunctionTerm(
443: negativeNumber, result);
444: }
445: result = TermFactory.DEFAULT.createFunctionTerm(identifier,
446: result);
447:
448: Debug
449: .out(
450: "integerldt: result of translating literal (lit, result):",
451: lit, result);
452:
453: return result;
454:
455: }
456:
457: public Function getNumberTerminator() {
458: return sharp;
459: }
460:
461: public Function getNumberSymbol() {
462: return numbers;
463: }
464:
465: public Function getCharSymbol() {
466: return charID;
467: }
468:
469: public Function getNumberLiteralFor(int number) {
470: if (number < 0 || number > 9) {
471: throw new IllegalArgumentException(
472: "Number literal symbols range from 0 to 9. Requested was:"
473: + number);
474: }
475:
476: return numberSymbol[number];
477: }
478:
479: private boolean isNumberLiteral(Function f) {
480: char c = f.name().toString().charAt(0);
481: return (c - '0' >= 0) && (c - '0' <= 9);
482: }
483:
484: public boolean hasLiteralFunction(Function f) {
485: return containsFunction(f)
486: && (f.arity() == 0 || isNumberLiteral(f));
487: }
488:
489: public Expression translateTerm(Term t, ExtList children) {
490: if (!containsFunction((Function) t.op()))
491: return null;
492: Function f = (Function) t.op();
493: if (isNumberLiteral(f) || f == numbers || f == charID) {
494: StringBuffer sb = new StringBuffer("");
495: Term it = t;
496: if (f == charID || f == numbers) {
497: it = it.sub(0);
498: f = (Function) it.op();
499: }
500: while (isNumberLiteral(f)) {
501: sb.insert(0, f.name().toString().charAt(0));
502: it = it.sub(0);
503: f = (Function) it.op();
504: }
505: // numbers must end with a sharp
506: if (f == sharp) {
507: return new IntLiteral(sb.toString());
508: }
509: }
510: throw new RuntimeException(
511: "IntegerLDT: Cannot convert term to program: " + t);
512: }
513:
514: /**
515: * returns the unary function symbol for representing a negative
516: * number literal
517: * @return the function symbol used to represent negative number literals
518: */
519: public Function getNegativeNumberSign() {
520: return negativeNumber;
521: }
522:
523: /**
524: * returns the unary function symbol for representing the negative value
525: * e.g. <code> -(var) </code>
526: * @return the function symbol used to represent the negative sign
527: */
528: public Function getNegativeSign() {
529: return negative;
530: }
531:
532: /**
533: * returns the function symbol used to represent addition of
534: * arithmetical integers
535: * @return the function symbol for integer addition
536: */
537: public Function getArithAddition() {
538: return plus;
539: }
540:
541: /**
542: * returns the function symbol used to represent substraction of
543: * arithmetical integers
544: * @return the function symbol for integer substraction
545: */
546: public Function getArithSubstraction() {
547: return minus;
548: }
549:
550: /**
551: * returns the function symbol used to represent multiplication on
552: * the arithmetical integers
553: * @return the function symbol used to represent integer multiplication
554: */
555: public Function getArithMultiplication() {
556: return times;
557: }
558:
559: /**
560: * returns the function symbol used to represent division of
561: * the arithmetical integers
562: * @return the function symbol used to represent integer division
563: */
564: public Function getArithDivision() {
565: return divide;
566: }
567:
568: /**
569: * returns the function symbol used to represent java-like division of
570: * the arithmetical integers
571: * @return the function symbol used to represent integer division
572: */
573: public Function getJDivision() {
574: return jDivide;
575: }
576:
577: /**
578: * returns the function symbol used to represent the modulo operation of
579: * the arithmetical integers
580: * @return the function symbol used to represent the integer modulo operation
581: */
582: public Function getArithModulo() {
583: return modulo;
584: }
585:
586: /**
587: * returns the function symbol used to represent the java-like modulo operation of
588: * the arithmetical integers
589: * @return the function symbol used to represent the integer modulo operation
590: */
591: public Function getJModulo() {
592: return jModulo;
593: }
594:
595: /**
596: * returns the boolean function symbol to compare two integer values
597: * <code>val1, val2</code> if <code>val1</code> is lesser or equal than
598: * <code>val2</code>
599: * @return the boolean function symbol to compare two integer values
600: */
601: public Function getLessOrEquals() {
602: return lessOrEquals;
603: }
604:
605: /**
606: * returns the boolean function symbol to compare two integer values
607: * <code>val1, val2</code> if <code>val1</code> is lesser than
608: * <code>val2</code>
609: * @return the boolean function symbol to compare two integer values
610: */
611: public Function getLessThan() {
612: return lessThan;
613: }
614:
615: /**
616: * returns the boolean function symbol to compare two integer values
617: * <code>val1, val2</code> if <code>val1</code> is greater or equals
618: * <code>val2</code>
619: * @return the boolean function symbol to compare two integer values
620: */
621: public Function getGreaterOrEquals() {
622: return greaterOrEquals;
623: }
624:
625: /**
626: * returns the boolean function symbol to compare two integer values
627: * <code>val1, val2</code> if <code>val1</code> is greater than
628: * <code>val2</code>
629: * @return the boolean function symbol to compare two integer values
630: */
631: public Function getGreaterThan() {
632: return greaterThan;
633: }
634:
635: /** returns a function mapping an arithmetic integer to its Java long representation */
636: public Function getModuloLong() {
637: return modJlong;
638: }
639:
640: /**
641: * returns the function symbol interpreted as the Java addition on
642: * int (or promotabel to int) operators, i.e. this addition performs a modulo
643: * operation wrt. to the range of type <code>int</code>. This function is independent
644: * of the chosen integer semantics.
645: *
646: * In case you want to represent the Java addition on operands promotable to <code>int</code>
647: * which shall be interpreted by the chosen integer semantics use
648: * {@link AbstractIntegerLDT#getJavaAddInt()} instead
649: *
650: * @return mathematical interpreted function realising the Java addition on operands of or promotable
651: * to type <code>int</code>
652: */
653: public Function getArithJavaIntAddition() {
654: return addJint;
655: }
656:
657: public abstract Function getInBoundsPredicate();
658:
659: /**
660: * the function representing the Java operator when one of the
661: * operators is an or can be promoted to an int
662: * @return function representing the generic Java operator function
663: */
664: public Function getJavaAddInt() {
665: return javaAddInt;
666: }
667:
668: /**
669: * the function representing the Java operator when one of the
670: * operators is of type long
671: * @return function representing the generic Java operator function
672: */
673: public Function getJavaAddLong() {
674: return javaAddLong;
675: }
676:
677: /**
678: * the function representing the Java operator when one of the
679: * operators is an or can be promoted to int
680: * @return function representing the generic Java operator function
681: */
682: public Function getJavaBitwiseAndInt() {
683: return javaBitwiseAndInt;
684: }
685:
686: /**
687: * the function representing the Java operator when one of the
688: * operators is of type long
689: * @return function representing the generic Java operator function
690: */
691: public Function getJavaBitwiseAndLong() {
692: return javaBitwiseAndLong;
693: }
694:
695: /**
696: * the function representing the Java operator <code>~</code>
697: * @return function representing the generic Java operator function
698: */
699: public Function getJavaBitwiseNegation() {
700: return javaBitwiseNegation;
701: }
702:
703: /**
704: * the function representing the Java operator <code>|</code>
705: * when one of the operands is an or can be promoted to int
706: * @return function representing the generic Java operator function
707: */
708: public Function getJavaBitwiseOrInt() {
709: return javaBitwiseOrInt;
710: }
711:
712: /**
713: * the function representing the Java operator <code>|</code>
714: * when one of the operands is of type long
715: * @return function representing the generic Java operator function
716: */
717: public Function getJavaBitwiseOrLong() {
718: return javaBitwiseOrLong;
719: }
720:
721: /**
722: * the function representing the Java operator <code>^</code>
723: * when one of the operands is an or can be promoted to int
724: * @return function representing the generic Java operator function
725: */
726: public Function getJavaBitwiseXOrInt() {
727: return javaBitwiseXOrInt;
728: }
729:
730: /**
731: * the function representing the Java operator <code>^</code>
732: * when one of the operands is exact of type long
733: * @return function representing the generic Java operator function
734: */
735: public Function getJavaBitwiseXOrLong() {
736: return javaBitwiseXOrLong;
737: }
738:
739: /**
740: * the function representing the Java operator <code>(byte)</code>
741: * @return function representing the generic Java operator function
742: */
743: public Function getJavaCastByte() {
744: return javaCastByte;
745: }
746:
747: /**
748: * the function representing the Java operator <code>(char)</code>
749: * @return function representing the generic Java operator function
750: */
751: public Function getJavaCastChar() {
752: return javaCastChar;
753: }
754:
755: /**
756: * the function representing the Java operator <code>(int)</code>
757: * @return function representing the generic Java operator function
758: */
759: public Function getJavaCastInt() {
760: return javaCastInt;
761: }
762:
763: /**
764: * the function representing the Java operator <code>(long)</code>
765: * @return function representing the generic Java operator function
766: */
767: public Function getJavaCastLong() {
768: return javaCastLong;
769: }
770:
771: /**
772: * the function representing the Java operator <code>(short)</code>
773: * @return function representing the generic Java operator function
774: */
775: public Function getJavaCastShort() {
776: return javaCastShort;
777: }
778:
779: /**
780: * the function representing the Java operator <code>/</code>
781: * when one of the operands is an or a subtype of int
782: * @return function representing the generic Java operator function
783: */
784: public Function getJavaDivInt() {
785: return javaDivInt;
786: }
787:
788: /**
789: * the function representing the Java operator <code>/</code>
790: * when one of the operands is exact of type long
791: * @return function representing the generic Java operator function
792: */
793: public Function getJavaDivLong() {
794: return javaDivLong;
795: }
796:
797: /**
798: * the function representing the Java operator <code>%</code>
799: * when one of the operands is an or a subtype of int
800: * @return function representing the generic Java operator function
801: */
802: public Function getJavaMod() {
803: return javaMod;
804: }
805:
806: /**
807: * the function representing the Java operator <code>*</code>
808: * when one of the operands is an or a subtype of int
809: * @return function representing the generic Java operator function
810: */
811: public Function getJavaMulInt() {
812: return javaMulInt;
813: }
814:
815: /**
816: * the function representing the Java operator <code>*</code>
817: * when one of the operands is exact of type long
818: * @return function representing the generic Java operator function
819: */
820: public Function getJavaMulLong() {
821: return javaMulLong;
822: }
823:
824: /**
825: * the function representing the Java operator <code><<</code>
826: * when one of the operands is an or a subtype of int
827: * @return function representing the generic Java operator function
828: */
829: public Function getJavaShiftLeftInt() {
830: return javaShiftLeftInt;
831: }
832:
833: /**
834: * the function representing the Java operator <code><<</code>
835: * when one of the operands is exact of type long
836: * @return function representing the generic Java operator function
837: */
838: public Function getJavaShiftLeftLong() {
839: return javaShiftLeftLong;
840: }
841:
842: /**
843: * the function representing the Java operator <code>>></code>
844: * when one of the operands is an or a subtype of int
845: * @return function representing the generic Java operator function
846: */
847: public Function getJavaShiftRightInt() {
848: return javaShiftRightInt;
849: }
850:
851: /**
852: * the function representing the Java operator <code>>></code>
853: * when one of the operands is exact of type long
854: * @return function representing the generic Java operator function
855: */
856: public Function getJavaShiftRightLong() {
857: return javaShiftRightLong;
858: }
859:
860: /**
861: * the function representing the Java operator <code>-</code>
862: * when one of the operands is an or a subtype of int
863: * @return function representing the generic Java operator function
864: */
865: public Function getJavaSubInt() {
866: return javaSubInt;
867: }
868:
869: /**
870: * the function representing the Java operator <code>-</code>
871: * when one of the operands is exact of type long
872: * @return function representing the generic Java operator function
873: */
874: public Function getJavaSubLong() {
875: return javaSubLong;
876: }
877:
878: /**
879: * the function representing the Java operator <code>-expr</code>
880: * when one of the operands is an or a subtype of int
881: * @return function representing the generic Java operator function
882: */
883: public Function getJavaUnaryMinusInt() {
884: return javaUnaryMinusInt;
885: }
886:
887: /**
888: * the function representing the Java operator <code>-exprLong</code>
889: * when one of the operands is exact of type long
890: * @return function representing the generic Java operator function
891: */
892: public Function getJavaUnaryMinusLong() {
893: return javaUnaryMinusLong;
894: }
895:
896: /**
897: * the function representing the Java operator <code>>>></code>
898: * when one of the operands is an or a subtype of int
899: * @return function representing the generic Java operator function
900: */
901: public Function getJavaUnsignedShiftRightInt() {
902: return javaUnsignedShiftRightInt;
903: }
904:
905: /**
906: * the function representing the Java operator <code>>>></code>
907: * when one of the operands is exact of type long
908: * @return function representing the generic Java operator function
909: */
910: public Function getJavaUnsignedShiftRightLong() {
911: return javaUnsignedShiftRightLong;
912: }
913: }
|