Implement Variable.div and fix NPE

src/main/java/staticAnalyzer/Variable.java

@@ -311,29 +311,28 @@ public Variable add( Variable v ) {
         return newLocal();
     }
 
-    public Variable div( Variable v ) { //@TODO
-        DomainValue dv;
-        if (   getDomainValue() == DomainValue.TOP
-          || v.getDomainValue() == DomainValue.TOP ) {
-            dv = DomainValue.TOP;
-        } else {
-            dv = DomainValue.GEQ0;
+    public Variable div( Variable v ) {
+        if (getDomainValue() == DomainValue.BOTTOM || v.getDomainValue() == DomainValue.BOTTOM) {
+            return new Variable(type, Kind.LOCAL, DomainValue.BOTTOM, Integer.MAX_VALUE, 0);
         }
-        Variable r = new Variable(v.type,Kind.LOCAL,dv
-                ,Integer.MAX_VALUE,0);
+
+        if (getDomainValue() == DomainValue.TOP || v.getDomainValue() == DomainValue.TOP) {
+            return new Variable(type, Kind.LOCAL, DomainValue.TOP, Integer.MAX_VALUE, 0);
+        }
+
+        Variable r = new Variable(type, Kind.LOCAL, DomainValue.GEQ0, Integer.MAX_VALUE, 0);
 
         // analyze safe and edge
-        Iterator i = safe.iterator();
-        while( i.hasNext() ) {
-            Variable s = (Variable)i.next();
-            if (v.safe.contains(s)) {
+        // For integer arithmetic: result = this / v.
+        // If this >= 0 and v >= 1, then result <= this.
+        // Propagate safe (strict upper bounds) and edge (inclusive upper bounds).
+        if (safe != null) {
+            for (Variable s : safe) {
                 r.addSafe(s);
             }
         }
-        i = edge.iterator();
-        while( i.hasNext() ) {
-            Variable s = (Variable)i.next();
-            if (v.edge.contains(s)) {
+        if (edge != null) {
+            for (Variable s : edge) {
                 r.addEdge(s);
             }
         }

src/test/java/staticAnalyzer/VariableTest.java

@@ -0,0 +1,54 @@
+package staticAnalyzer;
+
+import org.junit.jupiter.api.Test;
+import static org.junit.jupiter.api.Assertions.*;
+
+public class VariableTest {
+
+    @Test
+    public void testDivNPE() {
+        Variable v1 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.GEQ0, 1, 0);
+        Variable v2 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.GEQ0, 2, 0);
+
+        // This is expected to fail with NPE before fix
+        assertDoesNotThrow(() -> v1.div(v2), "div should not throw NPE even if safe/edge lists are null");
+    }
+
+    @Test
+    public void testDivLogic() {
+        Variable v1 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.GEQ0, 1, 0);
+        Variable v2 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.G0, 2, 0);
+
+        Variable s1 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.TOP, 3, 0);
+        Variable e1 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.TOP, 4, 0);
+
+        v1.addSafe(s1);
+        v1.addEdge(e1);
+
+        Variable res = v1.div(v2);
+
+        // Verify result is GEQ0
+        assertEquals(Variable.DomainValue.GEQ0, res.getDomainValue());
+
+        // Verify bounds propagation (v1 / v2 <= v1 < s1) => res < s1
+        assertTrue(res.isSafe(s1), "Result should be safe for s1");
+
+        // Verify bounds propagation (v1 / v2 <= v1 <= e1) => res <= e1
+        assertTrue(res.isEdge(e1), "Result should be edge for e1");
+    }
+
+    @Test
+    public void testDivBottom() {
+        Variable v1 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.BOTTOM, 1, 0);
+        Variable v2 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.GEQ0, 2, 0);
+
+        Variable res = v1.div(v2);
+        assertEquals(Variable.DomainValue.BOTTOM, res.getDomainValue());
+
+        Variable v3 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.GEQ0, 3, 0);
+        Variable v4 = new Variable("I", Variable.Kind.LOCAL, Variable.DomainValue.BOTTOM, 4, 0);
+
+        Variable res2 = v3.div(v4);
+        assertEquals(Variable.DomainValue.BOTTOM, res2.getDomainValue());
+    }
+}