File tree Expand file tree Collapse file tree 1 file changed +8
-8
lines changed
Expand file tree Collapse file tree 1 file changed +8
-8
lines changed Original file line number Diff line number Diff line change @@ -35,11 +35,11 @@ public class Object {
3535 // used by monitorenter, monitorexit, wait, and notify
3636 // Not present in the original Object class
3737 public int monitorCount ;
38-
38+
3939 public Object () {
4040 monitorCount = 0 ;
4141 }
42-
42+
4343 public final Class <?> getClass () {
4444 /*
4545 * MODELS LIBRARY {
@@ -122,8 +122,8 @@ public static void monitorenter(Object object)
122122 {
123123 //FIXME: we shoud remove the call to this method from the call
124124 // stack appended to the thrown exception
125- if (object == null )
126- throw new NullPointerException ();
125+ // if (object == null)
126+ // throw new NullPointerException();
127127
128128 CProver .atomicBegin ();
129129 // this assume blocks this execution path in JBMC and simulates
@@ -145,11 +145,11 @@ public static void monitorexit(Object object)
145145 {
146146 //FIXME: we shoud remove the call to this method from the call
147147 // stack appended to the thrown exception
148- if (object == null )
149- throw new NullPointerException ();
148+ // if (object == null)
149+ // throw new NullPointerException();
150150
151- if (object .monitorCount == 0 )
152- throw new IllegalMonitorStateException ();
151+ // if (object.monitorCount == 0)
152+ // throw new IllegalMonitorStateException();
153153 CProver .atomicBegin ();
154154 object .monitorCount --;
155155 CProver .atomicEnd ();
You can’t perform that action at this time.
0 commit comments