2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
18 package gov.nasa.jpf.vm;
20 import gov.nasa.jpf.JPFException;
23 * a FieldLockInfo that assumes lock protection after n accesses with
26 public abstract class ThresholdFieldLockInfo extends FieldLockInfo implements Cloneable {
27 protected int remainingChecks;
29 protected ThresholdFieldLockInfo(int remainingChecks) {
30 this.remainingChecks = remainingChecks;
34 public boolean isProtected() {
35 // otherwise this would have turned into a EmptyFieldLockInfo
36 return (remainingChecks == 0);
39 protected void checkFailedLockAssumption(ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
40 if (remainingChecks == 0) {
41 // with no locks remaining this would have been demoted to an
42 // EmptyFieldLockInfo by now
43 lockAssumptionFailed(ti, ei, fi);
48 * this implements a path-local FieldLockInfo that are never mutated
49 * this has to be overridden for search global FieldLockInfos
51 protected FieldLockInfo getInstance (int nRemaining){
53 ThresholdFieldLockInfo fli = (ThresholdFieldLockInfo)clone();
54 fli.remainingChecks = nRemaining;
57 } catch (CloneNotSupportedException cnsx){
58 throw new JPFException("clone of ThresholdFieldLockInfo failed: " + this);