Members/kono/jpf-core: src/main/gov/nasa/jpf/vm/Verify.java annotate

author	Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date	Fri, 23 Jan 2015 10:14:01 -0800
parents
children	f6886b2bda4a

rev	line source
0 61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	1 /*
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	2 * Copyright (C) 2014, United States Government, as represented by the
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	3 * Administrator of the National Aeronautics and Space Administration.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	4 * All rights reserved.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	5 *
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	6 * The Java Pathfinder core (jpf-core) platform is licensed under the
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	7 * Apache License, Version 2.0 (the "License"); you may not use this file except
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	8 * in compliance with the License. You may obtain a copy of the License at
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	9 *
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	10 * http://www.apache.org/licenses/LICENSE-2.0.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	11 *
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	12 * Unless required by applicable law or agreed to in writing, software
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	13 * distributed under the License is distributed on an "AS IS" BASIS,
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	15 * See the License for the specific language governing permissions and
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	16 * limitations under the License.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	17 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	18 package gov.nasa.jpf.vm;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	19
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	20 import java.io.FileInputStream;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	21 import java.io.FileOutputStream;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	22 import java.io.ObjectInputStream;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	23 import java.io.ObjectOutputStream;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	24 import java.util.BitSet;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	25 import java.util.Random;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	26
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	27
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	28 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	29 * Verify is the programmatic interface of JPF that can be used from inside of
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	30 * applications. In order to enable programs to run outside of the JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	31 * environment, we provide (mostly empty) bodies for the methods that are
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	32 * otherwise intercepted by the native peer class
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	33 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	34 public class Verify {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	35 static final int MAX_COUNTERS = 10;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	36 static int[] counter; // only here so that we don't pull in all JPF classes at RT
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	37
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	38 private static Random random;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	39
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	40 /*
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	41 * only set if this was used from within a JPF context. This is mainly to
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	42 * enable encapsulation of JPF specific types so that they only get
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	43 * pulled in on demand, and we otherwise can still use the same Verify class
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	44 * for JPF-external execution. We use a class object to make sure it doesn't
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	45 * get recycled once JPF is terminated.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	46 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	47 static Class<?> peer;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	48
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	49 private static Random getRandom() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	50 if (random == null) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	51 random = new Random(42);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	52 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	53 return random;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	54 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	55
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	56 /*
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	57 * register the peer class, which is only done from within a JPF execution
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	58 * context. Be aware of that this migh actually load the real Verify class.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	59 * The sequence usually is
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	60 * JPF(Verify) -> VM(JPF_gov_nasa_jpf_vm_Verify) -> VM(Verify)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	61 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	62 public static void setPeerClass (Class<?> cls) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	63 peer = cls;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	64 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	65
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	66 // note this is NOT marked native because we might also call it from host VM code
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	67 // (beware that Verify is a different class there!). When executed by JPF,
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	68 // this is an MJI method
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	69 public static int getCounter (int id) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	70 if (peer != null) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	71 // this is executed if we are in a JPF context
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	72 return JPF_gov_nasa_jpf_vm_Verify.getCounter__I__I(null, 0, id);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	73 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	74 if (counter == null) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	75 counter = new int[id >= MAX_COUNTERS ? (id+1) : MAX_COUNTERS];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	76 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	77 if ((id < 0) \|\| (id >= counter.length)) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	78 return 0;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	79 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	80
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	81 return counter[id];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	82 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	83 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	84
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	85 public static void resetCounter (int id) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	86 if (peer != null){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	87 JPF_gov_nasa_jpf_vm_Verify.resetCounter__I__V(null, 0, id);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	88 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	89 if ((counter != null) && (id >= 0) && (id < counter.length)) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	90 counter[id] = 0;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	91 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	92 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	93 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	94
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	95 public static void setCounter (int id, int val) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	96 if (peer != null){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	97 JPF_gov_nasa_jpf_vm_Verify.setCounter__II__V(null, 0, id, val);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	98 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	99 if ((counter != null) && (id >= 0) && (id < counter.length)) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	100 counter[id] = val;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	101 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	102 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	103 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	104
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	105
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	106 public static int incrementCounter (int id) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	107 if (peer != null){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	108 return JPF_gov_nasa_jpf_vm_Verify.incrementCounter__I__I(null, 0, id);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	109 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	110 if (counter == null) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	111 counter = new int[(id >= MAX_COUNTERS) ? id+1 : MAX_COUNTERS];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	112 } else if (id >= counter.length) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	113 int[] newCounter = new int[id+1];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	114 System.arraycopy(counter, 0, newCounter, 0, counter.length);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	115 counter = newCounter;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	116 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	117
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	118 if ((id >= 0) && (id < counter.length)) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	119 return ++counter[id];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	120 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	121
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	122 return 0;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	123 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	124 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	125
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	126 public static final int NO_VALUE = -1;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	127
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	128 public static void putValue (String key, int value) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	129 throw new UnsupportedOperationException("putValue requires JPF execution");
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	130 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	131
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	132 public static int getValue (String key) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	133 throw new UnsupportedOperationException("getValue requires JPF execution");
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	134 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	135
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	136 // same mechanism and purpose as the counters, but with BitSets, which is
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	137 // more convenient if we have a lot of different events to check
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	138
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	139 static BitSet[] bitSets;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	140
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	141 private static void checkBitSetId(int id) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	142 if (bitSets == null) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	143 bitSets = new BitSet[id + 1];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	144 } else if (id >= bitSets.length) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	145 BitSet[] newBitSets = new BitSet[id + 1];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	146 System.arraycopy(bitSets, 0, newBitSets, 0, bitSets.length);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	147 bitSets = newBitSets;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	148 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	149
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	150 if (bitSets[id] == null) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	151 bitSets[id] = new BitSet();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	152 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	153 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	154
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	155
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	156 public static void setBitInBitSet(int id, int bit, boolean value) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	157 if (peer != null){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	158 // this is executed if we did run JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	159 JPF_gov_nasa_jpf_vm_Verify.setBitInBitSet__IIZ__V(null, 0, id, bit, value);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	160 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	161 // this is executed if we run this without previously executing JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	162 checkBitSetId(id);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	163 bitSets[id].set(bit, value);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	164 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	165 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	166
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	167 public static boolean getBitInBitSet(int id, int bit) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	168 if (peer != null){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	169 // this is executed if we did run JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	170 return JPF_gov_nasa_jpf_vm_Verify.getBitInBitSet__II__Z(null, 0, id, bit);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	171
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	172 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	173 // this is executed if we run this without previously executing JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	174 checkBitSetId(id);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	175 return bitSets[id].get(bit);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	176 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	177 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	178
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	179 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	180 * Adds a comment to the error trace, which will be printed and saved.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	181 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	182 public static void addComment (String s) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	183
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	184 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	185 * Backwards compatibility START
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	186 * @deprecated use "assert cond : msg"
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	187 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	188 @Deprecated
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	189 public static void assertTrue (String s, boolean cond) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	190 if (!cond) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	191 System.out.println(s);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	192 assertTrue(cond);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	193 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	194 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	195
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	196 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	197 * Checks that the condition is true.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	198 * @deprecated use 'assert' directly
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	199 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	200 @Deprecated
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	201 public static void assertTrue (boolean cond) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	202 if (!cond) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	203 throw new AssertionError("Verify.assertTrue failed");
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	204 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	205 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	206
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	207 public static void atLabel (String label) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	208
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	209 public static void atLabel (int label) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	210
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	211 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	212 * Marks the beginning of an atomic block.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	213 * THIS IS EVIL, DON'T USE IT FOR OPTIMIZATION - THAT'S WHAT POR IS FOR!
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	214 * (it's mostly here to support model classes that need to execute atomic)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	215 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	216 public static void beginAtomic () {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	217
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	218 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	219 * Marks the end of an atomic block.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	220 * EVIL - see beginAtomic()
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	221 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	222 public static void endAtomic () {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	223
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	224 public static void boring (boolean cond) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	225
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	226 public static void busyWait (long duration) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	227 // this gets only executed outside of JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	228 while (duration > 0) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	229 duration--;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	230 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	231 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	232
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	233 public static boolean isCalledFromClass (String refClsName) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	234 Throwable t = new Throwable();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	235 StackTraceElement[] st = t.getStackTrace();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	236
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	237 if (st.length < 3) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	238 // main() or run()
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	239 return false;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	240 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	241
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	242 try {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	243 Class<?> refClazz = Class.forName(refClsName);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	244 Class<?> callClazz = Class.forName(st[2].getClassName());
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	245
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	246 return (refClazz.isAssignableFrom(callClazz));
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	247
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	248 } catch (ClassNotFoundException cfnx) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	249 return false;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	250 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	251 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	252
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	253 public static void ignoreIf (boolean cond) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	254
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	255 public static void instrumentPoint (String label) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	256
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	257 public static void instrumentPointDeep (String label) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	258
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	259 public static void instrumentPointDeepRecur (String label, int depth) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	260
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	261 public static void interesting (boolean cond) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	262
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	263 public static void breakTransition (String reason) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	264
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	265 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	266 * simple debugging aids to imperatively print the current path output of the SUT
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	267 * (to be used with vm.path_output)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	268 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	269 public static void printPathOutput(String msg) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	270 public static void printPathOutput(boolean cond, String msg) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	271
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	272 public static void threadPrint (String s) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	273 System.out.print( Thread.currentThread().getName());
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	274 System.out.print(": ");
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	275 System.out.print(s);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	276 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	277
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	278 public static void threadPrintln (String s) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	279 threadPrint(s);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	280 System.out.println();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	281 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	282
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	283 public static void print (String s) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	284 System.out.print(s);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	285 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	286
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	287 public static void println (String s) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	288 System.out.println(s);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	289 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	290
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	291 public static void print (String s, int i) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	292 System.out.print(s + " : " + i);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	293 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	294
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	295 public static void print (String s, boolean b) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	296 System.out.print(s + " : " + b);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	297 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	298
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	299 public static void println() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	300 System.out.println();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	301 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	302
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	303 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	304 * this is to avoid StringBuilders
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	305 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	306 public static void print (String... args){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	307 for (String s : args){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	308 System.out.print(s);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	309 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	310 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	311
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	312 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	313 * note - these are mostly for debugging purposes (to see if attributes get
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	314 * propagated correctly, w/o having to write a listener), since attributes are
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	315 * supposed to be created at the native side, and hence can't be accessed from
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	316 * the application
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	317 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	318
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	319 //--- use these if you know there are single attributes
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	320 public static void setFieldAttribute (Object o, String fieldName, int val) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	321 public static int getFieldAttribute (Object o, String fieldName) { return 0; }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	322
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	323 //--- use these for multiple attributes
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	324 public static void addFieldAttribute (Object o, String fieldName, int val) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	325 public static int[] getFieldAttributes (Object o, String fieldName) { return new int[0]; }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	326
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	327 public static void setLocalAttribute (String varName, int val) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	328 public static int getLocalAttribute (String varName) { return 0; }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	329
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	330 public static void addLocalAttribute (String varName, int val) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	331 public static int[] getLocalAttributes (String varName) { return new int[0]; }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	332
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	333 public static void setElementAttribute (Object arr, int idx, int val){}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	334 public static int getElementAttribute (Object arr, int idx) { return 0; }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	335
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	336 public static void addElementAttribute (Object arr, int idx, int val){}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	337 public static int[] getElementAttributes (Object arr, int idx) { return new int[0]; }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	338
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	339 public static void setObjectAttribute (Object o, int val) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	340 public static int getObjectAttribute (Object o) { return 0; }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	341
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	342 public static void addObjectAttribute (Object o, int val) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	343 public static int[] getObjectAttributes (Object o) { return new int[0]; }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	344
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	345
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	346 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	347 * this is the new boolean choice generator. Since there's no real
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	348 * heuristic involved with boolean values, we skip the id (it's a
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	349 * hardwired "boolean")
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	350 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	351 public static boolean getBoolean () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	352 // just executed when not running inside JPF, native otherwise
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	353 return ((System.currentTimeMillis() & 1) != 0);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	354 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	355
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	356 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	357 * new boolean choice generator that also tells jpf which value to
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	358 * use first by default in a search.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	359 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	360 public static boolean getBoolean (boolean falseFirst) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	361 // this is only executed when not running JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	362 return getBoolean();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	363 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	364
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	365
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	366 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	367 * Returns int nondeterministically between (and including) min and max.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	368 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	369 public static int getInt (int min, int max) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	370 // this is only executed when not running JPF, native otherwise
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	371 return getRandom().nextInt((max-min+1)) + min;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	372 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	373
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	374 public static int getIntFromList (int... values){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	375 if (values != null && values.length > 0) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	376 int i = getRandom().nextInt(values.length);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	377 return values[i];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	378 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	379 return getRandom().nextInt();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	380 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	381 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	382
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	383 public static Object getObject (String key) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	384 return "?";
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	385 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	386
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	387 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	388 * this is the API for int value choice generators. 'id' is used to identify
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	389 * both the corresponding ChoiceGenerator subclass, and the application specific
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	390 * ctor parameters from the normal JPF configuration mechanism
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	391 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	392 public static int getInt (String key){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	393 // this is only executed when not running JPF, native otherwise
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	394 return getRandom().nextInt();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	395 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	396
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	397 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	398 * this is the API for double value choice generators. 'id' is used to identify
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	399 * both the corresponding ChoiceGenerator subclass, and the application specific
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	400 * ctor parameters from the normal JPF configuration mechanism
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	401 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	402 public static double getDouble (String key){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	403 // this is only executed when not running JPF, native otherwise
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	404 return getRandom().nextDouble();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	405 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	406
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	407 public static double getDoubleFromList (double... values){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	408 if (values != null && values.length > 0) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	409 int i = getRandom().nextInt(values.length);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	410 return values[i];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	411 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	412 return getRandom().nextDouble();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	413 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	414 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	415
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	416 public static long getLongFromList (long...values){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	417 if (values != null && values.length > 0) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	418 int i = getRandom().nextInt(values.length);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	419 return values[i];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	420 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	421 return getRandom().nextLong();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	422 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	423 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	424
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	425 public static float getFloatFromList (float...values){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	426 if (values != null && values.length > 0) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	427 int i = getRandom().nextInt(values.length);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	428 return values[i];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	429 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	430 return getRandom().nextFloat();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	431 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	432 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	433
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	434
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	435 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	436 * Returns a random number between 0 and max inclusive.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	437 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	438 public static int random (int max) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	439 // this is only executed when not running JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	440 return getRandom().nextInt(max + 1);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	441 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	442
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	443 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	444 * Returns a random boolean value, true or false. Note this gets
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	445 * handled by the native peer, and is just here to enable running
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	446 * instrumented applications w/o JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	447 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	448 public static boolean randomBool () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	449 // this is only executed when not running JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	450 return getRandom().nextBoolean();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	451 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	452
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	453 public static long currentTimeMillis () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	454 return System.currentTimeMillis();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	455 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	456
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	457 // Backwards compatibility START
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	458 public static Object randomObject (String type) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	459 return null;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	460 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	461
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	462 public static boolean isRunningInJPF() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	463 return false;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	464 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	465
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	466 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	467 * USE CAREFULLY - returns true if the virtual machine this code is
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	468 * running under is doing state matching. This can be used as a hint
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	469 * as to whether data structures (that are known to be correct!)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	470 * should be configured to use a canonical representation. For example,
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	471 * <pre><code>
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	472 * Vector v = new Vector();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	473 * v.add(obj1);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	474 * if (Verify.getBoolean()) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	475 * v.addAll(eleventyBillionObjectCollection);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	476 * v.setSize(1);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	477 * }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	478 * // compare states here
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	479 * </code></pre>
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	480 * To the programmer, the states are (almost certainly) the same. To
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	481 * the VM, they could be different (capacity inside the Vector). For
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	482 * the sake of speed, Vector does not store things canonically, but this
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	483 * can cause (probably mild) state explosion if matching states. If
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	484 * you know whether states are being matched, you can choose the right
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	485 * structure--as long as those structures aren't what you're looking for
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	486 * bugs in!
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	487 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	488 public static boolean vmIsMatchingStates() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	489 return false;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	490 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	491
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	492 public static void storeTrace (String fileName, String comment) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	493 // intercepted in NativePeer
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	494 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	495
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	496 public static void storeTraceIf (boolean cond, String fileName, String comment) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	497 if (cond) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	498 storeTrace(fileName, comment);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	499 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	500 }

0

61d41facf527 initial v8 import (history reset)