File tree 1 file changed +8
-8
lines changed
1 file changed +8
-8
lines changed Original file line number Diff line number Diff line change @@ -35,11 +35,11 @@ public class Object {
35
35
// used by monitorenter, monitorexit, wait, and notify
36
36
// Not present in the original Object class
37
37
public int monitorCount ;
38
-
38
+
39
39
public Object () {
40
40
monitorCount = 0 ;
41
41
}
42
-
42
+
43
43
public final Class <?> getClass () {
44
44
/*
45
45
* MODELS LIBRARY {
@@ -122,8 +122,8 @@ public static void monitorenter(Object object)
122
122
{
123
123
//FIXME: we shoud remove the call to this method from the call
124
124
// stack appended to the thrown exception
125
- if (object == null )
126
- throw new NullPointerException ();
125
+ // if (object == null)
126
+ // throw new NullPointerException();
127
127
128
128
CProver .atomicBegin ();
129
129
// this assume blocks this execution path in JBMC and simulates
@@ -145,11 +145,11 @@ public static void monitorexit(Object object)
145
145
{
146
146
//FIXME: we shoud remove the call to this method from the call
147
147
// stack appended to the thrown exception
148
- if (object == null )
149
- throw new NullPointerException ();
148
+ // if (object == null)
149
+ // throw new NullPointerException();
150
150
151
- if (object .monitorCount == 0 )
152
- throw new IllegalMonitorStateException ();
151
+ // if (object.monitorCount == 0)
152
+ // throw new IllegalMonitorStateException();
153
153
CProver .atomicBegin ();
154
154
object .monitorCount --;
155
155
CProver .atomicEnd ();
You can’t perform that action at this time.
0 commit comments