Stack is added to stack set if it it is not bottom

lisa-analyzer · Feb 20, 2024 · fe37814 · fe37814
1 parent 548f42f
commit fe37814
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 8 deletions.
diff --git a/src/main/java/it/unipr/analysis/AbstractStackSet.java b/src/main/java/it/unipr/analysis/AbstractStackSet.java
@@ -22,7 +22,8 @@ public AbstractStackSet(Set<AbstractStack> elements, boolean isTop) {
 	}
 
 	public void add(AbstractStack other) {
-		this.elements.add(other);
+		if (!other.isBottom())
+			this.elements.add(other);
 	}
 
 	public AbstractStackSet top() {
@@ -32,12 +33,12 @@ public AbstractStackSet top() {
 	public AbstractStackSet bottom() {
 		return BOTTOM;
 	}
-	
+
 	@Override
 	public boolean isTop() {
 		return !isBottom() && this.elements().isEmpty() && this.isTop == true;
 	}
-	
+
 	@Override
 	public boolean isBottom() {
 		return this.elements == null;
@@ -58,20 +59,20 @@ else if (isBottom())
 			result.add(stack.clone());
 		return result;
 	}
-	
+
 	@Override
 	public AbstractStackSet lubAux(AbstractStackSet other) throws SemanticException {
 		AbstractStackSet lubAux = super.lubAux(other);
 		if (lubAux.size() > 10)
 			return TOP;
 		return lubAux;
 	}
-	
+
 	@Override
 	public int hashCode() {
 		return super.hashCode();
 	}
-	
+
 	@Override
 	public boolean equals(Object obj) {
 		if (this == obj)

diff --git a/src/main/java/it/unipr/analysis/EVMAbstractState.java b/src/main/java/it/unipr/analysis/EVMAbstractState.java
@@ -954,9 +954,9 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
 					for (AbstractStack stack : stacks) {
 						AbstractStack resultStack = stack.clone();
 						KIntegerSet new_mu_i = null;
-
+						
 						KIntegerSet offset = resultStack.pop();
-
+						
 						if (mu_i.equals(KIntegerSet.ZERO)) {
 							// This is an error. We cannot read from memory if
 							// there is no active words saved