diff --git a/src/main/java/java/lang/Object.java b/src/main/java/java/lang/Object.java index bbab359..a9e3b2e 100644 --- a/src/main/java/java/lang/Object.java +++ b/src/main/java/java/lang/Object.java @@ -110,7 +110,7 @@ public final void wait() throws InterruptedException { protected void finalize() throws Throwable { } /** - * This method is not present in the original Objecct class. + * This method is not present in the original Object class. * It will be called by JBMC when the monitor in this instance * is being acquired as a result of either the execution of a * monitorenter bytecode instruction or the call to a synchronized @@ -122,8 +122,8 @@ public static void monitorenter(Object object) { //FIXME: we shoud remove the call to this method from the call // stack appended to the thrown exception - // if (object == null) - // throw new NullPointerException(); + if (object == null) + throw new NullPointerException(); CProver.atomicBegin(); // this assume blocks this execution path in JBMC and simulates @@ -134,7 +134,7 @@ public static void monitorenter(Object object) } /** - * This method is not present in the original Objecct class. + * This method is not present in the original Object class. * It will be called by JBMC when the monitor in this instance * is being released as a result of either the execution of a * monitorexit bytecode instruction or the return (normal or exceptional) @@ -145,6 +145,9 @@ public static void monitorexit(Object object) { //FIXME: we shoud remove the call to this method from the call // stack appended to the thrown exception + // FIXME: Enabling these exceptions makes + // jbmc-regression/synchronized-blocks/test_sync.desc + // run into an infinite loop during symex // if (object == null) // throw new NullPointerException();