Fixing a null pointer dereference in the cvc3 compatibility layer. (#1089)

diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker.java b/src/bindings/compat/java/src/cvc3/ValidityChecker.java
index 1b38a4c9526e45d380da57e3800a9272283db5a9..9289a8ae7675c0fef9c1dc5c8fc24cd697850162 100644 (file)
--- a/src/bindings/compat/java/src/cvc3/ValidityChecker.java
+++ b/src/bindings/compat/java/src/cvc3/ValidityChecker.java
@@ -160,23 +160,23 @@ public class ValidityChecker extends Embedded {
     private static native Object
        jniCreateOp2(Object ValidityChecker, String name, Object Type, Object ExprDef) throws Cvc3Exception;
     private static native Object
-       jniEqOp() throws Cvc3Exception;
+       jniEqOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-       jniLtOp() throws Cvc3Exception;
+       jniLtOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-       jniLeOp() throws Cvc3Exception;
+       jniLeOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-       jniGtOp() throws Cvc3Exception;
+       jniGtOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-       jniGeOp() throws Cvc3Exception;
+       jniGeOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-       jniPlusOp() throws Cvc3Exception;
+       jniPlusOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-       jniMinusOp() throws Cvc3Exception;
+       jniMinusOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-       jniMultOp() throws Cvc3Exception;
+       jniMultOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-       jniDivideOp() throws Cvc3Exception;
+       jniDivideOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
        jniFunExpr1(Object ValidityChecker, Object Op, Object Expr) throws Cvc3Exception;
     private static native Object
@@ -919,47 +919,47 @@ public class ValidityChecker extends Embedded {
 
     // '='
     public OpMut eqOp() throws Cvc3Exception {
-       return new OpMut(jniEqOp(), embeddedManager());
+       return new OpMut(jniEqOp(embedded()), embeddedManager());
     }
 
     // '<'
     public OpMut ltOp() throws Cvc3Exception {
-       return new OpMut(jniLtOp(), embeddedManager());
+       return new OpMut(jniLtOp(embedded()), embeddedManager());
     }
 
     // '<='
     public OpMut leOp() throws Cvc3Exception {
-       return new OpMut(jniLeOp(), embeddedManager());
+       return new OpMut(jniLeOp(embedded()), embeddedManager());
     }
 
     // '>'
     public OpMut gtOp() throws Cvc3Exception {
-       return new OpMut(jniGtOp(), embeddedManager());
+       return new OpMut(jniGtOp(embedded()), embeddedManager());
     }
 
     // '>='
     public OpMut geOp() throws Cvc3Exception {
-       return new OpMut(jniGeOp(), embeddedManager());
+       return new OpMut(jniGeOp(embedded()), embeddedManager());
     }
 
     // '+'
     public OpMut plusOp() throws Cvc3Exception {
-       return new OpMut(jniPlusOp(), embeddedManager());
+       return new OpMut(jniPlusOp(embedded()), embeddedManager());
     }
 
     // '-'
     public OpMut minusOp() throws Cvc3Exception {
-       return new OpMut(jniMinusOp(), embeddedManager());
+       return new OpMut(jniMinusOp(embedded()), embeddedManager());
     }
 
     // '*'
     public OpMut multOp() throws Cvc3Exception {
-       return new OpMut(jniMultOp(), embeddedManager());
+       return new OpMut(jniMultOp(embedded()), embeddedManager());
     }
 
     // '/' for rationals
     public OpMut divideOp() throws Cvc3Exception {
-       return new OpMut(jniDivideOp(), embeddedManager());
+       return new OpMut(jniDivideOp(embedded()), embeddedManager());
     }
 
     public ExprMut funExpr(Op op, Expr expr1) throws Cvc3Exception {

diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
index cfda940d83f9ab4ac493e8a6a4a2d4e61414d4c3..6c6a9f8cba3b348854372b668932d7f775e6192a 100644 (file)
--- a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
+++ b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
@@ -300,40 +300,40 @@ jobject m ValidityChecker vc n string name c Type type c Expr expr
 return embed_copy(env, vc->createOp(name, *type, *expr));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniEqOp
-jobject
-return embed_copy<Op>(env, Op(EQ));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), EQ));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniLtOp
-jobject
-return embed_copy<Op>(env, Op(LT));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), LT));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniLeOp
-jobject
-return embed_copy<Op>(env, Op(LE));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), LE));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniGtOp
-jobject
-return embed_copy<Op>(env, Op(GT));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), GT));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniGeOp
-jobject
-return embed_copy<Op>(env, Op(GE));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), GE));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniPlusOp
-jobject
-return embed_copy<Op>(env, Op(PLUS));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), PLUS));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniMinusOp
-jobject
-return embed_copy<Op>(env, Op(MINUS));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), MINUS));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniMultOp
-jobject
-return embed_copy<Op>(env, Op(MULT));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), MULT));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniDivideOp
-jobject
-return embed_copy<Op>(env, Op(DIVIDE));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), DIVIDE));
 
 
 DEFINITION: Java_cvc3_ValidityChecker_jniFunExpr1

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 169b49faa0ae5c549a13e04475d6f70363f7eab2..df7257d3fa5e5774c1360f2a8ca7d4aa320f7bde 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -252,8 +252,8 @@ Expr::Expr(const Expr& e) : CVC4::Expr(e) {
 Expr::Expr(const CVC4::Expr& e) : CVC4::Expr(e) {
 }
 
-Expr::Expr(const CVC4::Kind k) : CVC4::Expr() {
-  *this = getEM()->operatorOf(k);
+Expr::Expr(ExprManager* em, const CVC4::Kind k) : CVC4::Expr() {
+  *this = em->operatorOf(k);
 }
 
 Expr Expr::eqExpr(const Expr& right) const {

diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index 25e3ae32f753b42b37cc974ee7e4ee7addc58d6d..daac466d56e847d4c97e01e304845270fc52d797 100644 (file)
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -321,7 +321,7 @@ public:
   Expr();
   Expr(const Expr& e);
   Expr(const CVC4::Expr& e);
-  Expr(CVC4::Kind k);
+  Expr(ExprManager* em, CVC4::Kind k);
 
   // Compound expression constructors
   Expr eqExpr(const Expr& right) const;