@@ -27,7 +27,7 @@ public class AbstractStack implements ValueDomain<AbstractStack>, BaseLattice<Ab
2727 * The top abstract element of this domain.
2828 */
2929 private static final AbstractStack TOP = new AbstractStack (
30- createFilledArray (STACK_LIMIT , StackElement .TOP ), STACK_LIMIT );
30+ createFilledArray (STACK_LIMIT , StackElement .TOP ));
3131
3232 /**
3333 * The bottom abstract element of this domain.
@@ -39,11 +39,6 @@ public class AbstractStack implements ValueDomain<AbstractStack>, BaseLattice<Ab
3939 */
4040 private final StackElement [] stack ;
4141
42- /**
43- * The size of this stack (i.e., the number of elements).
44- */
45- private int size ;
46-
4742 /**
4843 * Helper method to create and fill an array with a specific element.
4944 */
@@ -57,7 +52,7 @@ private static StackElement[] createFilledArray(int size, StackElement element)
5752 * Builds an initial symbolic stack.
5853 */
5954 public AbstractStack () {
60- this (createFilledArray (STACK_LIMIT , StackElement .BOTTOM ), 0 );
55+ this (createFilledArray (STACK_LIMIT , StackElement .BOTTOM ));
6156 }
6257
6358 /**
@@ -67,22 +62,6 @@ public AbstractStack() {
6762 */
6863 public AbstractStack (StackElement [] stack ) {
6964 this .stack = stack ;
70- if (stack != null ) {
71- int bottomCounter = 0 ;
72- for (StackElement item : stack ) {
73- if (item .isBottom ()) {
74- bottomCounter ++;
75- }
76- }
77- this .size = STACK_LIMIT - bottomCounter ;
78- } else {
79- this .size = 0 ;
80- }
81- }
82-
83- AbstractStack (StackElement [] stack , int size ) {
84- this .stack = stack ;
85- this .size = size ;
8665 }
8766
8867 @ Override
@@ -174,10 +153,6 @@ public boolean isBottom() {
174153 return stack == null ;
175154 }
176155
177- public boolean isEmpty () {
178- return size == 0 ;
179- }
180-
181156 @ Override
182157 public int hashCode () {
183158 return Objects .hash (Arrays .hashCode (stack ));
@@ -214,7 +189,7 @@ public StackElement getTop() {
214189 public AbstractStack clone () {
215190 if (isBottom () || isTop ())
216191 return this ;
217- return new AbstractStack (Arrays . copyOf ( stack , STACK_LIMIT ), this . size );
192+ return new AbstractStack (stack . clone () );
218193 }
219194
220195 /**
@@ -226,7 +201,6 @@ public void push(StackElement target) {
226201 // Shift all elements one position to the left
227202 System .arraycopy (stack , 1 , stack , 0 , STACK_LIMIT - 1 );
228203 stack [STACK_LIMIT - 1 ] = target ;
229- this .size ++;
230204 }
231205
232206 /**
@@ -238,31 +212,12 @@ public StackElement pop() {
238212 StackElement result = stack [STACK_LIMIT - 1 ];
239213 // Shift all elements one position to the right
240214 System .arraycopy (stack , 0 , stack , 1 , STACK_LIMIT - 1 );
241- if (!stack [1 ].isTop ()) {
215+ if (!stack [1 ].isTop ())
242216 stack [0 ] = StackElement .BOTTOM ;
243- this .size --;
244- } else {
217+ else
245218 stack [0 ] = StackElement .TOP ;
246- }
247- return result ;
248- }
249-
250- /**
251- * Returns the number of items in the stack (non-bottom).
252- *
253- * @return the number of items in the stack.
254- */
255- public int size () {
256- return this .size ;
257- }
258219
259- /**
260- * Yields the stack.
261- *
262- * @return the stack as an array
263- */
264- public StackElement [] getStack () {
265- return stack ;
220+ return result ;
266221 }
267222
268223 @ Override
@@ -282,9 +237,6 @@ public AbstractStack glbAux(AbstractStack other) throws SemanticException {
282237
283238 @ Override
284239 public boolean lessOrEqualAux (AbstractStack other ) throws SemanticException {
285- if (size () > other .size ())
286- return false ;
287-
288240 // Starting from the top of the stack and moving downward
289241 for (int i = STACK_LIMIT - 1 ; i >= 0 ; i --) {
290242 if (!this .stack [i ].lessOrEqual (other .stack [i ])) {
@@ -363,8 +315,7 @@ public AbstractStack dupX(int x) {
363315 if (hasBottomUntil (x ))
364316 return bottom ();
365317
366- AbstractStack clonedStack = clone ();
367- StackElement [] stackArray = clonedStack .getStack ();
318+ StackElement [] stackArray = this .stack .clone ();
368319
369320 int topIndex = STACK_LIMIT - 1 ;
370321 int targetIndex = topIndex - x + 1 ;
@@ -376,7 +327,7 @@ public AbstractStack dupX(int x) {
376327
377328 resultArray [topIndex ] = elementToDuplicate ;
378329
379- return new AbstractStack (resultArray , size () + 1 );
330+ return new AbstractStack (resultArray );
380331 }
381332
382333 /**
@@ -394,12 +345,12 @@ public AbstractStack swapX(int x) {
394345 int topIndex = STACK_LIMIT - 1 ;
395346 int swapIndex = topIndex - x ;
396347
397- StackElement [] newStack = Arrays . copyOf ( stack , STACK_LIMIT );
348+ StackElement [] newStack = this . stack . clone ( );
398349
399350 StackElement temp = newStack [topIndex ];
400351 newStack [topIndex ] = newStack [swapIndex ];
401352 newStack [swapIndex ] = temp ;
402353
403- return new AbstractStack (newStack , size () );
354+ return new AbstractStack (newStack );
404355 }
405356}
0 commit comments