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: package gov.nasa.jpf.jvm;
020:
021: import gov.nasa.jpf.Config;
022: import gov.nasa.jpf.Error;
023: import gov.nasa.jpf.ErrorList;
024: import gov.nasa.jpf.JPF;
025:
026: import java.io.PrintStream;
027:
028: import junit.framework.TestCase;
029:
030: /**
031: * base class for JPF unit tests. TestJPF mostly includes JPF invocations
032: * that check for occurrence or absence of certain execution results
033: */
034: public abstract class TestJPF extends TestCase {
035: static PrintStream out = System.out;
036:
037: protected TestJPF(String name) {
038: super (name);
039: }
040:
041: protected void runJPFDeadlock(String[] args) {
042: report(args);
043:
044: try {
045: Config conf = JPF.createConfig(args);
046:
047: if (conf.getTargetArg() != null) {
048: JPF jpf = new JPF(conf);
049: jpf.run();
050:
051: ErrorList errors = jpf.getSearchErrors();
052:
053: if (errors != null) {
054: for (int i = 0; i < errors.size(); i++) {
055: Error e = (Error) errors.get(i);
056:
057: if ("Deadlock".equals(e.getMessage())) {
058: System.out.println("found Deadlock");
059:
060: return; // success, we got the sucker
061: }
062: }
063: }
064: }
065: } catch (Throwable x) {
066: x.printStackTrace();
067: fail("JPF internal exception executing: " + args[0] + "."
068: + args[1] + " : " + x);
069: }
070:
071: fail("JPF failed to detect deadlock");
072: }
073:
074: /**
075: * run JPF and case the test to fail if NO AssertionsError is encountered
076: */
077: protected void runJPFassertionError(String[] args) {
078: runJPFException(args, "java.lang.AssertionError");
079: }
080:
081: /**
082: * It runs JPF and cause the test to fail if an AssertionError is encountered
083: */
084: protected void runJPFnoAssertionError(String[] args) {
085: runJPFnoException(args);
086: }
087:
088: protected void runJPFnoException(String[] args) {
089: ExceptionInfo xi = null;
090:
091: report(args);
092:
093: try {
094: // run JPF on our target test func
095: gov.nasa.jpf.JPF.main(args);
096:
097: xi = JVM.getVM().getPendingException();
098: if (xi == null) {
099: return; // success
100: }
101: } catch (Throwable t) {
102: // we get as much as one little hickup and we declare it failed
103: fail("JPF internal exception executing: " + args[0] + "."
104: + args[1] + " : " + t);
105: }
106:
107: fail("JPF caught exception executing: " + args[0] + "."
108: + args[1] + " : " + xi.getExceptionClassname());
109: }
110:
111: protected void runJPFException(String[] args, String xClassName) {
112: ExceptionInfo xi = null;
113:
114: report(args);
115:
116: try {
117: // run JPF on our target test func
118: gov.nasa.jpf.JPF.main(args);
119:
120: xi = JVM.getVM().getPendingException();
121: if (xi == null) {
122: fail("JPF failed to catch exception executing: "
123: + args[0] + "." + args[1] + " , expected: "
124: + xClassName);
125: } else if (!xClassName.equals(xi.getExceptionClassname())) {
126: fail("JPF caught wrong exception: "
127: + xi.getExceptionClassname() + ", expected: "
128: + xClassName);
129: }
130: } catch (Throwable x) {
131: fail("JPF internal exception executing: " + args[0] + "."
132: + args[1] + " : " + x);
133: }
134: }
135:
136: void report(String[] args) {
137: out.print(" running jpf with args:");
138:
139: for (int i = 0; i < args.length; i++) {
140: out.print(' ');
141: out.print(args[i]);
142: }
143:
144: out.println();
145: }
146: }
|