@@ -40,7 +40,7 @@ public class AbstractStack implements ValueDomain<AbstractStack>, BaseLattice<Ab
4040 private final StackElement [] stack ;
4141
4242 /**
43- * The size of this stack (i.e., the number of elements)
43+ * The size of this stack (i.e., the number of elements).
4444 */
4545 private int size ;
4646
@@ -267,35 +267,17 @@ public StackElement[] getStack() {
267267
268268 @ Override
269269 public AbstractStack lubAux (AbstractStack other ) throws SemanticException {
270- StackElement [] result = new StackElement [STACK_LIMIT ];
271-
272- for (int i = 0 ; i < STACK_LIMIT ; i ++) {
273- result [i ] = this .stack [i ].lub (other .stack [i ]);
274- }
275-
276- return new AbstractStack (result );
270+ throw new RuntimeException ("lub on abstract stack should be never called" );
277271 }
278272
279273 @ Override
280274 public AbstractStack wideningAux (AbstractStack other ) throws SemanticException {
281- StackElement [] result = new StackElement [STACK_LIMIT ];
282-
283- for (int i = 0 ; i < STACK_LIMIT ; i ++) {
284- result [i ] = this .stack [i ].widening (other .stack [i ]);
285- }
286-
287- return new AbstractStack (result );
275+ throw new RuntimeException ("widening on abstract stack should be never called" );
288276 }
289277
290278 @ Override
291279 public AbstractStack glbAux (AbstractStack other ) throws SemanticException {
292- StackElement [] result = new StackElement [STACK_LIMIT ];
293-
294- for (int i = 0 ; i < STACK_LIMIT ; i ++) {
295- result [i ] = this .stack [i ].glb (other .stack [i ]);
296- }
297-
298- return new AbstractStack (result );
280+ throw new RuntimeException ("glb on abstract stack should be never called" );
299281 }
300282
301283 @ Override
0 commit comments