---

Point.java

package edu.ksu.cis.bandera.abstraction.lib.real;

/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * Bandera, a Java(TM) analysis and transformation toolkit           *
 * Copyright (C) 1998-2001 SAnToS Laboratories (santos@cis.ksu.edu)  *

 * All rights reserved.                                              *
 *                                                                   *
 * This work was done as a project in the SAnToS Laboratory,         *
 * Department of Computing and Information Sciences, Kansas State    *
 * University, USA (http://www.cis.ksu.edu/santos).                  *
 * It is understood that any modification not identified as such is  *
 * not covered by the preceding statement.                           *
 *                                                                   *
 * This work is free software; you can redistribute it and/or        *
 * modify it under the terms of the GNU Library General Public       *
 * License as published by the Free Software Foundation; either      *
 * version 2 of the License, or (at your option) any later version.  *
 *                                                                   *
 * This work is distributed in the hope that it will be useful,      *
 * but WITHOUT ANY WARRANTY; without even the implied warranty of    *
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *
 * Library General Public License for more details.                  *
 *                                                                   *
 * You should have received a copy of the GNU Library General Public *
 * License along with this toolkit; if not, write to the             *
 * Free Software Foundation, Inc., 59 Temple Place - Suite 330,      *
 * Boston, MA  02111-1307, USA.                                      *
 *                                                                   *
 * Java is a trademark of Sun Microsystems, Inc.                     *
 *                                                                   *
 * To submit a bug report, send a comment, or get the latest news on *
 * this project and other SAnToS projects, please visit the web-site *
 *                http://www.cis.ksu.edu/santos                      *
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
// This file was generated by Bandera (http://www.cis.ksu.edu/santos/bandera).
import edu.ksu.cis.bandera.abstraction.*;
public class Point extends RealAbstraction {
  private static final Point v = new Point();
  public static final int POINT = 0;
  private Point() {
  }  
  public static int abs(double n) {
    if (n == n) return POINT;
    throw new RuntimeException("Point cannot abstract value '" + n + "'");
  }  
  public static int add(int left$, int right$) {
    if (left$ == left$) return POINT;
    throw new RuntimeException("Point.add(" + left$ + ", " + right$ + ") is undefined");
  }  
  private static int addNoChoose(int left, int right) {
    int result = 0;
    switch (left) {
      case 0:
        switch (right) {
          case 0:
            result = 1;
            break;
        }
        break;
    }
    if (result == 0) throw new RuntimeException("Point.addNoChoose(" + left + ", " + right + ") is undefined");
    return result;
  }  
  public static int addSet(int leftTokens, int rightTokens) {
    int result = -1;
    for (int left = 0; (1 << left) <= leftTokens; left++) {
      if ((leftTokens & (1 << left)) == 0) continue;
      for (int right = 0; (1 << right) <= rightTokens; right++) {
        if ((rightTokens & (1 << right)) != 0) {
          if (result == -1) result = addNoChoose(left, right);
          else result = Abstraction.meetArith(result, addNoChoose(left, right));
        }
      }
    }
    return result;
  }  
  public static int div(int left$, int right$) {
    if (left$ == left$) return POINT;
    throw new RuntimeException("Point.div(" + left$ + ", " + right$ + ") is undefined");
  }  
  private static int divNoChoose(int left, int right) {
    int result = 0;
    switch (left) {
      case 0:
        switch (right) {
          case 0:
            result = 1;
            break;
        }
        break;
    }
    if (result == 0) throw new RuntimeException("Point.divNoChoose(" + left + ", " + right + ") is undefined");
    return result;
  }  
  public static int divSet(int leftTokens, int rightTokens) {
    int result = -1;
    for (int left = 0; (1 << left) <= leftTokens; left++) {
      if ((leftTokens & (1 << left)) == 0) continue;
      for (int right = 0; (1 << right) <= rightTokens; right++) {
        if ((rightTokens & (1 << right)) != 0) {
          if (result == -1) result = divNoChoose(left, right);
          else result = Abstraction.meetArith(result, divNoChoose(left, right));
        }
      }
    }
    return result;
  }  
  public static boolean eq(int left$, int right$) {
    if (left$ == left$) return Abstraction.choose();
    throw new RuntimeException("Point.eq(" + left$ + ", " + right$ + ") is undefined");
  }  
  private static byte eqNoChoose(int left, int right) {
    byte result = -1;
    switch (left) {
      case 0:
        switch (right) {
          case 0:
            result = 2;
            break;
        }
        break;
    }
    if (result == -1) throw new RuntimeException("Point.eqNoChoose(" + left + ", " + right + ") is undefined");
    return result;
  }  
  public static byte eqSet(int leftTokens, int rightTokens) {
    byte result = -1;
    for (int left = 0; (1 << left) <= leftTokens; left++) {
      if ((leftTokens & (1 << left)) == 0) continue;
      for (int right = 0; (1 << right) <= rightTokens; right++) {
        if ((rightTokens & (1 << right)) != 0) {
          if (result == -1) result = eqNoChoose(left, right);
          else result = Abstraction.meetTest(result, eqNoChoose(left, right));
        }
      }
    }
    return result;
  }  
  public static boolean ge(int left$, int right$) {
    if (left$ == left$) return Abstraction.choose();
    throw new RuntimeException("Point.ge(" + left$ + ", " + right$ + ") is undefined");
  }  
  private static byte geNoChoose(int left, int right) {
    byte result = -1;
    switch (left) {
      case 0:
        switch (right) {
          case 0:
            result = 2;
            break;
        }
        break;
    }
    if (result == -1) throw new RuntimeException("Point.geNoChoose(" + left + ", " + right + ") is undefined");
    return result;
  }  
  public static byte geSet(int leftTokens, int rightTokens) {
    byte result = -1;
    for (int left = 0; (1 << left) <= leftTokens; left++) {
      if ((leftTokens & (1 << left)) == 0) continue;
      for (int right = 0; (1 << right) <= rightTokens; right++) {
        if ((rightTokens & (1 << right)) != 0) {
          if (result == -1) result = geNoChoose(left, right);
          else result = Abstraction.meetTest(result, geNoChoose(left, right));
        }
      }
    }
    return result;
  }  
  public static String getBASLRepresentation() {
    return
      "abstraction Point extends real \n"
      + "  begin\n"
      + "    TOKENS = {POINT};\n"
      + "    DEFAULT = POINT;\n"
      + "    ONE2ONE = {};\n"
      + "    abstract (n)\n"
      + "      begin\n"
      + "        _ -> POINT;\n"
      + "      end\n"
      + "    operator + add \n"
      + "      begin\n"
      + "        _ -> POINT;\n"
      + "      end\n"
      + "    operator - sub \n"
      + "      begin\n"
      + "        _ -> POINT;\n"
      + "      end\n"
      + "    operator * mul \n"
      + "      begin\n"
      + "        _ -> POINT;\n"
      + "      end\n"
      + "    operator / div \n"
      + "      begin\n"
      + "        _ -> POINT;\n"
      + "      end\n"
      + "    test == eq \n"
      + "      begin\n"
      + "        _ -> T;\n"
      + "      end\n"
      + "    test != neq \n"
      + "      begin\n"
      + "        _ -> T;\n"
      + "      end\n"
      + "    test < lt \n"
      + "      begin\n"
      + "        _ -> T;\n"
      + "      end\n"
      + "    test <= le \n"
      + "      begin\n"
      + "        _ -> T;\n"
      + "      end\n"
      + "    test > gt \n"
      + "      begin\n"
      + "        _ -> T;\n"
      + "      end\n"
      + "    test >= ge \n"
      + "      begin\n"
      + "        _ -> T;\n"
      + "      end\n"
      + "  end\n"
    ;
  }  
  public static String getName() {
    return "Point";
  }  
  public static int getNumOfTokens() {
    return 1;
  }  
  public static String getToken(int value) {
    switch(value) {
      case POINT: return "Point.POINT";
    }
    return "Point.???";
  }  
  public static boolean gt(int left$, int right$) {
    if (left$ == left$) return Abstraction.choose();
    throw new RuntimeException("Point.gt(" + left$ + ", " + right$ + ") is undefined");
  }  
  private static byte gtNoChoose(int left, int right) {
    byte result = -1;
    switch (left) {
      case 0:
        switch (right) {
          case 0:
            result = 2;
            break;
        }
        break;
    }
    if (result == -1) throw new RuntimeException("Point.gtNoChoose(" + left + ", " + right + ") is undefined");
    return result;
  }  
  public static byte gtSet(int leftTokens, int rightTokens) {
    byte result = -1;
    for (int left = 0; (1 << left) <= leftTokens; left++) {
      if ((leftTokens & (1 << left)) == 0) continue;
      for (int right = 0; (1 << right) <= rightTokens; right++) {
        if ((rightTokens & (1 << right)) != 0) {
          if (result == -1) result = gtNoChoose(left, right);
          else result = Abstraction.meetTest(result, gtNoChoose(left, right));
        }
      }
    }
    return result;
  }  
  public static boolean isOne2One(int value) {
    return false;
  }  
  public static boolean le(int left$, int right$) {
    if (left$ == left$) return Abstraction.choose();
    throw new RuntimeException("Point.le(" + left$ + ", " + right$ + ") is undefined");
  }  
  private static byte leNoChoose(int left, int right) {
    byte result = -1;
    switch (left) {
      case 0:
        switch (right) {
          case 0:
            result = 2;
            break;
        }
        break;
    }
    if (result == -1) throw new RuntimeException("Point.leNoChoose(" + left + ", " + right + ") is undefined");
    return result;
  }  
  public static byte leSet(int leftTokens, int rightTokens) {
    byte result = -1;
    for (int left = 0; (1 << left) <= leftTokens; left++) {
      if ((leftTokens & (1 << left)) == 0) continue;
      for (int right = 0; (1 << right) <= rightTokens; right++) {
        if ((rightTokens & (1 << right)) != 0) {
          if (result == -1) result = leNoChoose(left, right);
          else result = Abstraction.meetTest(result, leNoChoose(left, right));
        }
      }
    }
    return result;
  }  
  public static boolean lt(int left$, int right$) {
    if (left$ == left$) return Abstraction.choose();
    throw new RuntimeException("Point.lt(" + left$ + ", " + right$ + ") is undefined");
  }  
  private static byte ltNoChoose(int left, int right) {
    byte result = -1;
    switch (left) {
      case 0:
        switch (right) {
          case 0:
            result = 2;
            break;
        }
        break;
    }
    if (result == -1) throw new RuntimeException("Point.ltNoChoose(" + left + ", " + right + ") is undefined");
    return result;
  }  
  public static byte ltSet(int leftTokens, int rightTokens) {
    byte result = -1;
    for (int left = 0; (1 << left) <= leftTokens; left++) {
      if ((leftTokens & (1 << left)) == 0) continue;
      for (int right = 0; (1 << right) <= rightTokens; right++) {
        if ((rightTokens & (1 << right)) != 0) {
          if (result == -1) result = ltNoChoose(left, right);
          else result = Abstraction.meetTest(result, ltNoChoose(left, right));
        }
      }
    }
    return result;
  }  
  public static int mul(int left$, int right$) {
    if (left$ == left$) return POINT;
    throw new RuntimeException("Point.mul(" + left$ + ", " + right$ + ") is undefined");
  }  
  private static int mulNoChoose(int left, int right) {
    int result = 0;
    switch (left) {
      case 0:
        switch (right) {
          case 0:
            result = 1;
            break;
        }
        break;
    }
    if (result == 0) throw new RuntimeException("Point.mulNoChoose(" + left + ", " + right + ") is undefined");
    return result;
  }  
  public static int mulSet(int leftTokens, int rightTokens) {
    int result = -1;
    for (int left = 0; (1 << left) <= leftTokens; left++) {
      if ((leftTokens & (1 << left)) == 0) continue;
      for (int right = 0; (1 << right) <= rightTokens; right++) {
        if ((rightTokens & (1 << right)) != 0) {
          if (result == -1) result = mulNoChoose(left, right);
          else result = Abstraction.meetArith(result, mulNoChoose(left, right));
        }
      }
    }
    return result;
  }  
  public static boolean ne(int left$, int right$) {
    if (left$ == left$) return Abstraction.choose();
    throw new RuntimeException("Point.ne(" + left$ + ", " + right$ + ") is undefined");
  }  
  private static byte neNoChoose(int left, int right) {
    byte result = -1;
    switch (left) {
      case 0:
        switch (right) {
          case 0:
            result = 2;
            break;
        }
        break;
    }
    if (result == -1) throw new RuntimeException("Point.neNoChoose(" + left + ", " + right + ") is undefined");
    return result;
  }  
  public static byte neSet(int leftTokens, int rightTokens) {
    byte result = -1;
    for (int left = 0; (1 << left) <= leftTokens; left++) {
      if ((leftTokens & (1 << left)) == 0) continue;
      for (int right = 0; (1 << right) <= rightTokens; right++) {
        if ((rightTokens & (1 << right)) != 0) {
          if (result == -1) result = neNoChoose(left, right);
          else result = Abstraction.meetTest(result, neNoChoose(left, right));
        }
      }
    }
    return result;
  }  
  public static int sub(int left$, int right$) {
    if (left$ == left$) return POINT;
    throw new RuntimeException("Point.sub(" + left$ + ", " + right$ + ") is undefined");
  }  
  private static int subNoChoose(int left, int right) {
    int result = 0;
    switch (left) {
      case 0:
        switch (right) {
          case 0:
            result = 1;
            break;
        }
        break;
    }
    if (result == 0) throw new RuntimeException("Point.subNoChoose(" + left + ", " + right + ") is undefined");
    return result;
  }  
  public static int subSet(int leftTokens, int rightTokens) {
    int result = -1;
    for (int left = 0; (1 << left) <= leftTokens; left++) {
      if ((leftTokens & (1 << left)) == 0) continue;
      for (int right = 0; (1 << right) <= rightTokens; right++) {
        if ((rightTokens & (1 << right)) != 0) {
          if (result == -1) result = subNoChoose(left, right);
          else result = Abstraction.meetArith(result, subNoChoose(left, right));
        }
      }
    }
    return result;
  }  
  public String toString() {
    return getName();
  }  
  public static Point v() {
    return v;
  }  
}

---