001: //
002: //Copyright (C) 2005 United States Government as represented by the
003: //Administrator of the National Aeronautics and Space Administration
004: //(NASA). All Rights Reserved.
005: //
006: //This software is distributed under the NASA Open Source Agreement
007: //(NOSA), version 1.3. The NOSA has been approved by the Open Source
008: //Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: //directory tree for the complete NOSA document.
010: //
011: //THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: //KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: //LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: //SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: //A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: //THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: //DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019:
020: /*
021: * Created on Sep 8, 2005
022: *
023: * TODO To change the template for this generated file go to
024: * Window - Preferences - Java - Code Style - Code Templates
025: */
026: package gov.nasa.jpf.jvm.choice;
027:
028: import gov.nasa.jpf.Config;
029: import gov.nasa.jpf.jvm.IntChoiceGenerator;
030: import gov.nasa.jpf.jvm.JVM;
031: import gov.nasa.jpf.jvm.StaticElementInfo;
032: import gov.nasa.jpf.jvm.ClassInfo;
033:
034: /**
035: * @author jpenix
036: *
037: * choose from a set of static variables (auch as an enumeration)
038: * specified in a configuration as
039: * bob.class = IntChoiceFromStaticVarSet
040: * bob.values = {MyClass.ONE, MyClass.TWO, MyOtherClass.OTHER}
041: * where "bob" is the choice id.
042: *
043: * choices can then made using: getInt("bob");
044: */
045: /**
046: * @author jpenix
047: *
048: * TODO To change the template for this generated type comment go to
049: * Window - Preferences - Java - Code Style - Code Templates
050: */
051: public class IntChoiceFromStaticVarSet extends IntChoiceGenerator {
052:
053: String[] values;
054: int count = -1;
055:
056: /**
057: * @param conf - JPF configuration object
058: * @param id - String identifier for the choice instance. this should be unique.
059: */
060: public IntChoiceFromStaticVarSet(Config conf, String id) {
061: super (id);
062: values = conf.getStringArray(id + ".values");
063: }
064:
065: /* (non-Javadoc)
066: * @see gov.nasa.jpf.jvm.IntChoiceGenerator#getNextChoice()
067: */
068: public int getNextChoice(JVM vm) {
069:
070: //split out class name and variable name
071: String[] varId = values[count].split("[.]+");
072:
073: ClassInfo ci = ClassInfo.getClassInfo(varId[0]);
074: StaticElementInfo ei = vm.getKernelState().sa.get(ci.getName());
075: int ret = ei.getIntField(varId[1], null);
076:
077: // print "Choice: bob = MyClass.ONE(1)"
078: vm.println("Choice: " + id + " = " + values[count] + "(" + ret
079: + ")");
080: return ret;
081: }
082:
083: /* (non-Javadoc)
084: * @see gov.nasa.jpf.jvm.ChoiceGenerator#hasMoreChoices()
085: */
086: public boolean hasMoreChoices(JVM vm) {
087: if (count < values.length - 1)
088: return true;
089: else
090: return false;
091: }
092:
093: /* (non-Javadoc)
094: * @see gov.nasa.jpf.jvm.ChoiceGenerator#advance(gov.nasa.jpf.jvm.JVM)
095: */
096: public void advance(JVM vm) {
097: count++;
098: }
099:
100: }
|