Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/util/test/TestMultiProcessJPF.java @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial v8 import (history reset)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 10:14:01 -0800
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:61d41facf527
1 /*
2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
4 * All rights reserved.
5 *
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
9 *
10 * http://www.apache.org/licenses/LICENSE-2.0.
11 *
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
17 */
18
19 package gov.nasa.jpf.util.test;
20
21 import gov.nasa.jpf.Config;
22 import gov.nasa.jpf.Property;
23 import gov.nasa.jpf.util.TypeRef;
24 import gov.nasa.jpf.vm.NotDeadlockedProperty;
25
26 /**
27 * @author Nastaran Shafiei <nastaran.shafiei@gmail.com>
28 *
29 * This is a root class for testing multi-processes code. This forces
30 * JPF to use MultiProcessVM and DistributedSchedulerFactory
31 */
32 public abstract class TestMultiProcessJPF extends TestJPF {
33 int numOfPrc;
34
35 @Override
36 protected void setTestTargetKeys(Config conf, StackTraceElement testMethod) {
37 conf.put("target.entry", "runTestMethod([Ljava/lang/String;)V");
38 conf.put("target.replicate", Integer.toString(numOfPrc));
39 conf.put("target", testMethod.getClassName());
40 conf.put("target.test_method", testMethod.getMethodName());
41 conf.put("vm.class", "gov.nasa.jpf.vm.MultiProcessVM");
42 conf.put("vm.scheduler_factory.class", "gov.nasa.jpf.vm.DistributedSchedulerFactory");
43 }
44
45 protected native int getProcessId();
46
47 protected boolean mpVerifyAssertionErrorDetails (int prcNum, String details, String... args){
48 if (runDirectly) {
49 return true;
50 } else {
51 numOfPrc = prcNum;
52 unhandledException( getCaller(), "java.lang.AssertionError", details, args);
53 return false;
54 }
55 }
56
57 protected boolean mpVerifyAssertionError (int prcNum, String... args){
58 if (runDirectly) {
59 return true;
60 } else {
61 numOfPrc = prcNum;
62 unhandledException( getCaller(), "java.lang.AssertionError", null, args);
63 return false;
64 }
65 }
66
67 protected boolean mpVerifyNoPropertyViolation (int prcNum, String...args){
68 if (runDirectly) {
69 return true;
70 } else {
71 numOfPrc = prcNum;
72 noPropertyViolation(getCaller(), args);
73 return false;
74 }
75 }
76
77 protected boolean mpVerifyUnhandledExceptionDetails (int prcNum, String xClassName, String details, String... args){
78 if (runDirectly) {
79 return true;
80 } else {
81 numOfPrc = prcNum;
82 unhandledException( getCaller(), xClassName, details, args);
83 return false;
84 }
85 }
86
87 protected boolean mpVerifyUnhandledException (int prcNum, String xClassName, String... args){
88 if (runDirectly) {
89 return true;
90 } else {
91 numOfPrc = prcNum;
92 unhandledException( getCaller(), xClassName, null, args);
93 return false;
94 }
95 }
96
97 protected boolean mpVerifyJPFException (int prcNum, TypeRef xClsSpec, String... args){
98 if (runDirectly) {
99 return true;
100
101 } else {
102 numOfPrc = prcNum;
103 try {
104 Class<? extends Throwable> xCls = xClsSpec.asNativeSubclass(Throwable.class);
105
106 jpfException( getCaller(), xCls, args);
107
108 } catch (ClassCastException ccx){
109 fail("not a property type: " + xClsSpec);
110 } catch (ClassNotFoundException cnfx){
111 fail("property class not found: " + xClsSpec);
112 }
113 return false;
114 }
115 }
116
117 protected boolean mpVerifyPropertyViolation (int prcNum, TypeRef propertyClsSpec, String... args){
118 if (runDirectly) {
119 return true;
120
121 } else {
122 numOfPrc = prcNum;
123 try {
124 Class<? extends Property> propertyCls = propertyClsSpec.asNativeSubclass(Property.class);
125 propertyViolation( getCaller(), propertyCls, args);
126
127 } catch (ClassCastException ccx){
128 fail("not a property type: " + propertyClsSpec);
129 } catch (ClassNotFoundException cnfx){
130 fail("property class not found: " + propertyClsSpec);
131 }
132 return false;
133 }
134 }
135
136 protected boolean mpVerifyDeadlock (int prcNum, String... args){
137 if (runDirectly) {
138 return true;
139 } else {
140 numOfPrc = prcNum;
141 propertyViolation( getCaller(), NotDeadlockedProperty.class, args);
142 return false;
143 }
144 }
145 }