From 65a8b24090dc95a8b89747c42bfeaced86bea3a9 Mon Sep 17 00:00:00 2001
From: Quoc-Sang Phan <dark2bright@gmail.com>
Date: Tue, 23 Jan 2018 12:47:37 -0800
Subject: [PATCH] fix bug: check division by zero

---
 src/main/gov/nasa/jpf/jvm/bytecode/DDIV.java | 5 +++++
 1 file changed, 5 insertions(+)

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);
-- 
2.34.1