Mercurial > hg > Members > kono > jpf-core

annotate src/tests/gov/nasa/jpf/test/mc/basic/NoJPFExecTest.java @ 17:e15b03204dc7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked methods during class load time, which gets checked by ThreadInfo.enter(). Useful to flag methods which have to be intercepted/cut off when executing classes under JPF that can also be used outside. Especially useful to avoid the recursive JPF problem that can be caused by tests (which mix classpath and native_classpath). This currently throws a JPFException, but we could also turn this into a AssertionError in the SUT so that we get the SUT stack trace
author Peter Mehlitz <pcmehlitz@gmail.com>
date Mon, 23 Mar 2015 12:54:20 -0700
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
17
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
1 /*
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
2 * Copyright (C) 2015, United States Government, as represented by the
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
3 * Administrator of the National Aeronautics and Space Administration.
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
4 * All rights reserved.
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
5 *
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
8 * in compliance with the License. You may obtain a copy of the License at
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
9 *
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
10 * http://www.apache.org/licenses/LICENSE-2.0.
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
11 *
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
12 * Unless required by applicable law or agreed to in writing, software
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
13 * distributed under the License is distributed on an "AS IS" BASIS,
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
15 * See the License for the specific language governing permissions and
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
16 * limitations under the License.
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
17 */
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
18 package gov.nasa.jpf.test.mc.basic;
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
19
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
20 import gov.nasa.jpf.annotation.NoJPFExecution;
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
21 import gov.nasa.jpf.util.test.TestJPF;
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
22 import gov.nasa.jpf.util.TypeRef;
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
23 import org.junit.Test;
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
24
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
25 /**
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
26 * test for NoJPFExecution annotations
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
27 */
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
28 public class NoJPFExecTest extends TestJPF {
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
29
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
30 @NoJPFExecution
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
31 protected void foo(){
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
32 System.out.println("!! foo() should not be executed under JPF");
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
33 }
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
34
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
35 @Test
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
36 public void testNoJPFExec(){
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
37 if (verifyJPFException( new TypeRef("gov.nasa.jpf.JPFException"))){
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
38 foo();
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
39 }
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
40 }
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
41
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
42
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
43 @NoJPFExecution
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
44 protected void bar(){
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
45 System.out.println("!! bar() bytecode should not be executed under JPF");
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
46 }
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
47
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
48 @Test
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
49 public void testInterceptedNoJPFExec(){
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
50 if (verifyNoPropertyViolation()){
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
51 bar();
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
52 }
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
53 }
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
54
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
55 }