From a2dd5b86164efca5bc13c2c31c0ff013a059a328 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 11 Nov 2018 23:09:51 +0000 Subject: [PATCH 1/2] Enable Monitor entry exception and comment on issues with Monitor exit exceptions. See also cbmc#1236. --- src/main/java/java/lang/Object.java | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/main/java/java/lang/Object.java b/src/main/java/java/lang/Object.java index bbab359..024bf9e 100644 --- a/src/main/java/java/lang/Object.java +++ b/src/main/java/java/lang/Object.java @@ -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 @@ -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(); From 436b272c00c5098494334527ca1e306a48b8ec58 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 11 Nov 2018 23:10:24 +0000 Subject: [PATCH 2/2] Fix typo --- src/main/java/java/lang/Object.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/java/java/lang/Object.java b/src/main/java/java/lang/Object.java index 024bf9e..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 @@ -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)