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

annotate src/main/gov/nasa/jpf/vm/Verify.java @ 3:fdc263e5806b

added inverse matching in StringSetMatcher. Since this is not easy to do in regexes, it's at the next hight level in StringSetMatcher added a optional CG accessor interface (geChoice(i), getAllChoices(), getProcessedChoices() getUnprocessedChoices()) that can be used from listeners and peers to enumerate/analyse choice sets. Note that not all CGs have to support this as there is no requirement that CGs actually use pre-computed choice sets. The low level accessor is getChoice(i), ChoiceGeneratorBase provides generic (not very efficient) set accessor implementations. Note that ChoiceGeneratorBase.getChoice() has to be overridden in subclasses in order to support choice enumeration, the default impl is just there so that we don't break subclass compilation

author	Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date	Tue, 03 Feb 2015 08:49:33 -0800
parents	f6886b2bda4a
children	caa0924e093d

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
1 f6886b2bda4a first set of post v7 patches Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	265 /** for testing and debugging purposes */
f6886b2bda4a first set of post v7 patches Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	266 public static int breakTransition (String reason, int min, int max) {
f6886b2bda4a first set of post v7 patches Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	267 return -1;
f6886b2bda4a first set of post v7 patches Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	268 }
f6886b2bda4a first set of post v7 patches Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: 0 diff changeset	269
0 61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	270 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	271 * 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	272 * (to be used with vm.path_output)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	273 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	274 public static void printPathOutput(String msg) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	275 public static void printPathOutput(boolean cond, String msg) {}
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 public static void threadPrint (String s) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	278 System.out.print( Thread.currentThread().getName());
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	279 System.out.print(": ");
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	280 System.out.print(s);
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 threadPrintln (String s) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	284 threadPrint(s);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	285 System.out.println();
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
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	288 public static void print (String s) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	289 System.out.print(s);
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
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	292 public static void println (String s) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	293 System.out.println(s);
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
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	296 public static void print (String s, int i) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	297 System.out.print(s + " : " + i);
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
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	300 public static void print (String s, boolean b) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	301 System.out.print(s + " : " + b);
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 public static void println() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	305 System.out.println();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	306 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	307
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	308 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	309 * this is to avoid StringBuilders
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 public static void print (String... args){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	312 for (String s : args){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	313 System.out.print(s);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	314 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	315 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	316
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 * 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	319 * 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	320 * 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	321 * the application
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
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	324 //--- 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	325 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	326 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	327
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	328 //--- use these for multiple attributes
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	329 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	330 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	331
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	332 public static void setLocalAttribute (String varName, int val) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	333 public static int getLocalAttribute (String varName) { return 0; }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	334
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	335 public static void addLocalAttribute (String varName, int val) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	336 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	337
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	338 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	339 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	340
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	341 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	342 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	343
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	344 public static void setObjectAttribute (Object o, int val) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	345 public static int getObjectAttribute (Object o) { return 0; }
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 public static void addObjectAttribute (Object o, int val) {}
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	348 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	349
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 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	352 * 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	353 * 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	354 * hardwired "boolean")
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 public static boolean getBoolean () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	357 // 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	358 return ((System.currentTimeMillis() & 1) != 0);
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
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	361 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	362 * 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	363 * use first by default in a search.
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 public static boolean getBoolean (boolean falseFirst) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	366 // this is only executed when not running JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	367 return getBoolean();
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
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	370
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	371 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	372 * 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	373 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	374 public static int getInt (int min, int max) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	375 // 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	376 return getRandom().nextInt((max-min+1)) + min;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	377 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	378
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	379 public static int getIntFromList (int... values){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	380 if (values != null && values.length > 0) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	381 int i = getRandom().nextInt(values.length);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	382 return values[i];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	383 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	384 return getRandom().nextInt();
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 public static Object getObject (String key) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	389 return "?";
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	390 }
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 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	393 * 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	394 * 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	395 * ctor parameters from the normal JPF configuration mechanism
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 public static int getInt (String key){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	398 // 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	399 return getRandom().nextInt();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	400 }
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 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	403 * 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	404 * 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	405 * ctor parameters from the normal JPF configuration mechanism
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 getDouble (String key){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	408 // 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	409 return getRandom().nextDouble();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	410 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	411
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	412 public static double getDoubleFromList (double... values){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	413 if (values != null && values.length > 0) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	414 int i = getRandom().nextInt(values.length);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	415 return values[i];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	416 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	417 return getRandom().nextDouble();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	418 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	419 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	420
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	421 public static long getLongFromList (long...values){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	422 if (values != null && values.length > 0) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	423 int i = getRandom().nextInt(values.length);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	424 return values[i];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	425 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	426 return getRandom().nextLong();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	427 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	428 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	429
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	430 public static float getFloatFromList (float...values){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	431 if (values != null && values.length > 0) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	432 int i = getRandom().nextInt(values.length);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	433 return values[i];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	434 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	435 return getRandom().nextFloat();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	436 }
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
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	439
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	440 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	441 * 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	442 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	443 public static int random (int max) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	444 // this is only executed when not running JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	445 return getRandom().nextInt(max + 1);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	446 }
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 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	449 * 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	450 * 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	451 * instrumented applications w/o JPF
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 boolean randomBool () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	454 // this is only executed when not running JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	455 return getRandom().nextBoolean();
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
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	458 public static long currentTimeMillis () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	459 return System.currentTimeMillis();
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 // Backwards compatibility START
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	463 public static Object randomObject (String type) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	464 return null;
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 public static boolean isRunningInJPF() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	468 return false;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	469 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	470
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	471 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	472 * 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	473 * 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	474 * 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	475 * 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	476 * <pre><code>
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	477 * Vector v = new Vector();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	478 * v.add(obj1);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	479 * if (Verify.getBoolean()) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	480 * v.addAll(eleventyBillionObjectCollection);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	481 * v.setSize(1);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	482 * }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	483 * // compare states here
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	484 * </code></pre>
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	485 * 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	486 * 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	487 * 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	488 * 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	489 * 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	490 * 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	491 * bugs in!
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	492 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	493 public static boolean vmIsMatchingStates() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	494 return false;
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
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	497 public static void storeTrace (String fileName, String comment) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	498 // intercepted in NativePeer
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
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	501 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	502 if (cond) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	503 storeTrace(fileName, comment);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	504 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	505 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	506
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	507 public static void storeTraceAndTerminate (String fileName, String comment) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	508 storeTrace(fileName, comment);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	509 terminateSearch();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	510 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	511
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	512 public static void storeTraceAndTerminateIf (boolean cond, String fileName, String comment) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	513 if (cond) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	514 storeTrace(fileName, comment);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	515 terminateSearch();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	516 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	517 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	518
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	519 public static boolean isTraceReplay () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	520 return false; // native
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	521 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	522
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	523 public static boolean isShared (Object o){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	524 return false; // native
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	525 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	526
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	527 public static void setShared (Object o, boolean isShared) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	528 // native
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	529 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	530
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	531 public static void freezeSharedness (Object o, boolean freeze) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	532 // native
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	533 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	534
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	535 public static void terminateSearch () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	536 // native
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	537 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	538
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	539 public static void setProperties (String... p) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	540 // native
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	541 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	542
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	543 public static String getProperty (String key) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	544 // native
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	545 return null;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	546 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	547
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	548 public static <T> T createFromJSON(Class<T> clazz, String json){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	549 return null;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	550 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	551
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	552 public static void writeObjectToFile(Object object, String fileName) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	553 try {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	554 FileOutputStream fso = new FileOutputStream(fileName);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	555 ObjectOutputStream oos = new ObjectOutputStream(fso);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	556 oos.writeObject(object);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	557 oos.flush();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	558 oos.close();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	559
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	560 } catch (Exception ex) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	561 throw new RuntimeException(ex);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	562 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	563
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	564 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	565
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	566 public static <T> T readObjectFromFile(Class<T> clazz, String fileName) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	567 try
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	568 {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	569 FileInputStream fis = new FileInputStream(fileName);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	570 ObjectInputStream ois = new ObjectInputStream(fis);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	571
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	572 Object read = ois.readObject();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	573
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	574 return (T) read;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	575
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	576 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	577 catch (Exception ex) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	578 throw new RuntimeException(ex);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	579 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	580
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	581 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	582
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	583
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	584 //--- model logging support
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	585
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	586 /*
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	587 * we add these here so that we don't need to pull in any java.util.logging classes
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	588 * Note - these need to be kept in sync with our native peer
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	589 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	590 public static final int SEVERE = 1;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	591 public static final int WARNING = 2;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	592 public static final int INFO = 3;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	593 public static final int FINE = 4;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	594 public static final int FINER = 5;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	595 public static final int FINEST = 6;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	596
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	597 public static void log( String loggerId, int logLevel, String msg){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	598 System.err.println(msg);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	599 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	600
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	601 // to avoid construction of strings on the model side
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	602 public static void log( String loggerId, int logLevel, String msg, String arg){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	603 System.err.println(msg);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	604 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	605
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	606 public static void log( String loggerId, int logLevel, String format, Object... args){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	607 System.err.printf(format, args);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	608 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	609
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	610
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	611 }

Mercurial > hg > Members > kono > jpf-core

annotate src/main/gov/nasa/jpf/vm/Verify.java @ 3:fdc263e5806b