Enable Monitor entry exception

and comment on issues with Monitor exit exceptions.
See also cbmc#1236.

Author: peterschrammel

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
@@ -143,13 +143,16 @@ public static void monitorenter(Object object)
      */
     public static void monitorexit(Object object)
     {
-      //FIXME: we shoud remove the call to this method from the call
+      // FIXME: we shoud remove the call to this method from the call
       // stack appended to the thrown exception
+      // FIXME: Enabling thes exceptions makes
+      // jbmc-regression/synchronized-blocks/test_sync.desc
+      // run into an infinite loop during symex
       // if (object == null)
-      //   throw new NullPointerException();
+      //     throw new NullPointerException();
 
       // if (object.cproverMonitorCount == 0)
-      //   throw new IllegalMonitorStateException();
+      //    throw new IllegalMonitorStateException();
       CProver.atomicBegin();
       object.cproverMonitorCount--;
       CProver.atomicEnd();