288712: anno style verifyerror

6 files changed, 221 insertions, 0 deletions

diff --git a/tests/bugs166/pr288712/Main.java b/tests/bugs166/pr288712/Main.java
new file mode 100644
index 000000000..5dcfb388f
--- /dev/null
+++ b/tests/bugs166/pr288712/Main.java
@@ -0,0 +1,11 @@
+import figures.Line;
+import figures.Point;
+
+public class Main {
+	public static void main(String[] args) {
+		Point p1 = new Point(10, 100);
+		Point p2 = new Point(20, 200);
+		Line l1 = new Line(p1, p2);
+	}
+
+}
diff --git a/tests/bugs166/pr288712/answers/Answer2h.java b/tests/bugs166/pr288712/answers/Answer2h.java
new file mode 100644
index 000000000..dda4766e2
--- /dev/null
+++ b/tests/bugs166/pr288712/answers/Answer2h.java
@@ -0,0 +1,41 @@
+package answers;
+
+import org.aspectj.lang.ProceedingJoinPoint;
+import org.aspectj.lang.annotation.*;
+import figures.*;
+import java.awt.Rectangle;
+
+@Aspect
+public class Answer2h {
+	@Pointcut("call(public void figures.FigureElement+.move" +
+			"()) && target(fe)")
+	void movingFigureElement(Point fe) {}
+
+	@Around("movingFigureElement(fe)")
+	public void checkIfBoundsMovedSame(ProceedingJoinPoint thisJoinPoint,
+			Point fe) throws Throwable {		
+/*
+	@Pointcut("call(public void figures.FigureElement+.move" +
+			"(int, int)) && target(fe) && args(dx, dy)")
+	void movingFigureElement(FigureElement fe, int dx, int dy) {}
+
+	@Around("movingFigureElement(fe, dx, dy)")
+	public void checkIfBoundsMovedSame(ProceedingJoinPoint thisJoinPoint,
+			FigureElement fe, int dx, int dy) throws Throwable {		
+*/
+		Rectangle rectangleBefore = new Rectangle(fe.getBounds());
+		//thisJoinPoint.proceed(new Object[]{fe, dx, dy});		
+		thisJoinPoint.proceed(new Object[]{fe});		
+//		rectangleBefore.translate(dx, dy);
+		if(!rectangleBefore.equals(fe.getBounds()))
+			throw new IllegalStateException("move() invariant violation");
+
+		
+		// IF THE THREE LINES BELOW ARE UN-COMMENTED, THE EXCEPTION
+		// ISN'T THROWN!?
+		// Note: The three lines can be located anywhere inside the advice. 
+//		for(Object o: thisJoinPoint.getArgs()) {
+//			System.out.print(o+" ");
+//		}
+	}
+}
diff --git a/tests/bugs166/pr288712/figures/FigureElement.java b/tests/bugs166/pr288712/figures/FigureElement.java
new file mode 100644
index 000000000..334fc91b6
--- /dev/null
+++ b/tests/bugs166/pr288712/figures/FigureElement.java
@@ -0,0 +1,21 @@
+// Copyright (c) 2002 Palo Alto Research Center, Incorporated.
+// All Rights Reserved.
+
+
+package figures;
+
+import java.awt.*;
+import java.awt.geom.*;
+
+public interface FigureElement {
+    public static final int MIN_VALUE = 0;
+    public static final int MAX_VALUE = 500;
+
+    public abstract void move(int dx, int dy);
+
+    public abstract Rectangle getBounds();
+
+    public abstract boolean contains(Point2D p);
+
+    public abstract void paint(Graphics2D g2);
+}
diff --git a/tests/bugs166/pr288712/figures/Line.java b/tests/bugs166/pr288712/figures/Line.java
new file mode 100644
index 000000000..801684979
--- /dev/null
+++ b/tests/bugs166/pr288712/figures/Line.java
@@ -0,0 +1,58 @@
+// Copyright (c) 2002 Palo Alto Research Center, Incorporated.
+// All Rights Reserved.
+
+
+package figures;
+
+import java.awt.*;
+import java.awt.geom.*;
+
+public class Line extends ShapeFigureElement {
+    private Point _p1;
+    private Point _p2;
+
+    public Line(Point p1, Point p2) {
+        _p1 = p1;
+        _p2 = p2;
+    }
+
+    public Point getP1() { return _p1; }
+    public Point getP2() { return _p2; }
+
+    public void move(int dx, int dy) {
+        _p1.move(dx, dy);
+    }
+    public void move() {
+        _p1.move();
+//        _p2.move(dx, dy);
+    }
+
+    public String toString() {
+        return "Line(" + _p1 + ", " + _p2 + ")";
+    }
+
+    /**
+     * Used to determine if this line {@link contains(Point2D)} a point.
+     */
+    final static int THRESHHOLD = 5;
+
+    /**
+     * Returns <code>true</code> if the point segment distance is less than
+     * {@link THRESHHOLD}.
+     */
+    public boolean contains(Point2D p) {
+        return getLine2D().ptLineDist(p) < THRESHHOLD;
+    }
+
+    private Line2D getLine2D() {
+	return new Line2D.Float((float)getP1().getX(),
+                                (float)getP1().getY(),
+                                (float)getP2().getX(),
+                                (float)getP2().getY());
+    }
+
+    public Shape getShape() {
+        return getLine2D();
+    }
+}
+
diff --git a/tests/bugs166/pr288712/figures/Point.java b/tests/bugs166/pr288712/figures/Point.java
new file mode 100644
index 000000000..ce020c88a
--- /dev/null
+++ b/tests/bugs166/pr288712/figures/Point.java
@@ -0,0 +1,52 @@
+// Copyright (c) 2002 Palo Alto Research Center, Incorporated.
+// All Rights Reserved.
+
+
+package figures;
+
+import java.awt.*;
+import java.awt.geom.*;
+
+public class Point extends ShapeFigureElement {
+    private int _x;
+    private int _y;
+
+    public Point(int x, int y) {
+        _x = x;
+        _y = y;
+    }
+
+    public int getX() { return _x; }
+
+    public int getY() { return _y; }
+
+    public void setX(int x) { _x = x; }
+
+    public void setY(int y) { _y = y; }
+
+    public void move() {}
+    public void move(int dx, int dy) {
+    	_x += dx; 
+    	_y += dy;
+    	//setX(getX() + dx);
+    	//setY(getY() + dy);
+    }
+
+    public String toString() {
+        return "Point(" + _x + ", " + _y + ")";
+    }
+
+    /** The height of displayed {@link Point}s. */
+    private final static int HEIGHT = 10;
+
+    /** The width of displayed {@link Point}s. -- same as {@link HEIGHT}. */
+    private final static int WIDTH  = Point.HEIGHT;
+
+    public Shape getShape() {
+	return new Ellipse2D.Float((float)getX()-Point.WIDTH/2,
+                                   (float)getY()-Point.HEIGHT/2,
+                                   (float)Point.HEIGHT,
+                                   (float)Point.WIDTH);
+    }
+}
+
diff --git a/tests/bugs166/pr288712/figures/ShapeFigureElement.java b/tests/bugs166/pr288712/figures/ShapeFigureElement.java
new file mode 100644
index 000000000..295e39fac
--- /dev/null
+++ b/tests/bugs166/pr288712/figures/ShapeFigureElement.java
@@ -0,0 +1,38 @@
+// Copyright (c) 2002 Palo Alto Research Center, Incorporated.
+// All Rights Reserved.
+
+
+package figures;
+
+import java.awt.*;
+import java.awt.geom.*;
+
+public abstract class ShapeFigureElement implements FigureElement {
+    public abstract void move(int dx, int dy);
+
+    public abstract Shape getShape();
+
+    public Rectangle getBounds() {
+        return getShape().getBounds();
+    }
+
+    public boolean contains(Point2D p) {
+        return getShape().contains(p);
+    }
+
+    public Color getLineColor() {
+        return Color.black;
+    }
+
+    public Color getFillColor() {
+        return Color.red;
+    }
+
+    public final void paint(Graphics2D g2) {
+        Shape shape = getShape();
+        g2.setPaint(getFillColor());
+        g2.fill(shape);
+        g2.setPaint(getLineColor());
+        g2.draw(shape);
+    }
+}