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: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // 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:
018: package de.uka.ilkd.key.proof.decproc;
019:
020: /** This class is responsible for the translation of type boundary <tt>String</tt>s into their
021: * actual values.
022: *
023: * @author akuwertz
024: * @version 1.0, 03/31/2006
025: */
026:
027: public class TypeBoundTranslation {
028:
029: /** The array of <tt>String</tt> representations of the type boundary values */
030: private static final String[][] typeBounds = new String[][] {
031: // Int bounds
032: { "-2147483648", //MIN
033: "2147483647", //MAX
034: "2147483648", //HALFRANGE
035: "4294967296" //RANGE
036: },
037:
038: // Char bounds
039: { "0", //MIN
040: "65535", //MAX
041: null, // NullPointerException for char_HALFRANGE
042: "65535" //RANGE
043: },
044:
045: // Long bounds
046: { "-9223372036854775808", //MIN
047: "9223372036854775807", //MAX
048: "9223372036854775808", //HALFRANGE
049: "18446744073709551616" //RANGE
050: },
051:
052: // Byte bounds
053: { "-128", //MIN
054: "127", //MAX
055: "128", //HALFRANGE
056: "256" //RANGE
057: },
058:
059: // Short bounds
060: { "-32768", //MIN
061: "32767", //MAX
062: "32768", //HALFRANGE
063: "65536" //RANGE
064: } };
065:
066: /** String constants for wrong boundary specifiers */
067: private static final String noTypeBoundString = "The given string constant does not represent a valid type boudary!";
068:
069: /** Make the constructor private */
070: private TypeBoundTranslation() {
071: super ();
072: }
073:
074: /* Public method implementation */
075:
076: /** Returns a <tt>String</tt> representation of the value of a type boundary specified by
077: * the argument <tt>String</tt> <tt>typeBound</tt>
078: *
079: * @param typeBound the type boundary to be translated into a value
080: * @throws IllegalArgumentException if <tt>typeBound</tt> represent no valid type boundary
081: */
082: public static String getTypeBoundValue(String typeBound) {
083:
084: int indexOne, indexTwo;
085:
086: // Parse type constraint
087: String[] parts = typeBound.split("_");
088: String partOne = parts[0];
089: String partTwo = parts[1];
090:
091: // Compare data type
092: if (partOne.equals("int"))
093: indexOne = 0;
094: else if (partOne.equals("char"))
095: indexOne = 1;
096: else if (partOne.equals("long"))
097: indexOne = 2;
098: else if (partOne.equals("byte"))
099: indexOne = 3;
100: else if (partOne.equals("short"))
101: indexOne = 4;
102: else
103: throw new IllegalArgumentException(noTypeBoundString);
104:
105: // compare constraint
106: if (partTwo.equals("MIN"))
107: indexTwo = 0;
108: else if (partTwo.equals("MAX"))
109: indexTwo = 1;
110: else if (partTwo.equals("HALFRANGE"))
111: indexTwo = 2;
112: else if (partTwo.equals("RANGE"))
113: indexTwo = 3;
114: else
115: throw new IllegalArgumentException(noTypeBoundString);
116:
117: return typeBounds[indexOne][indexTwo];
118: }
119: }
|