From: Quoc-Sang Phan <dark2bright@gmail.com>
Date: Tue, 23 Jan 2018 20:47:37 +0000 (-0800)
Subject: fix bug: check division by zero
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=65a8b24090dc95a8b89747c42bfeaced86bea3a9

fix bug: check division by zero
---

diff --git a/src/main/gov/nasa/jpf/jvm/bytecode/DDIV.java b/src/main/gov/nasa/jpf/jvm/bytecode/DDIV.java
index 4c20b68..c14099b 100644
--- a/src/main/gov/nasa/jpf/jvm/bytecode/DDIV.java
+++ b/src/main/gov/nasa/jpf/jvm/bytecode/DDIV.java
@@ -35,6 +35,11 @@ public class DDIV extends Instruction implements JVMInstruction {
     double v1 = frame.popDouble();
     double v2 = frame.popDouble();
     
+    if (v1 == 0) {
+        return ti.createAndThrowException("java.lang.ArithmeticException",
+                                          "division by zero");
+    }
+
     double r = v2 / v1;
     
     frame.pushDouble(r);