Mercurial > hg > Members > kono > jpf-core

annotate src/annotations/gov/nasa/jpf/annotation/NoJPFExecution.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.annotation;
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 java.lang.annotation.ElementType;
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
21 import java.lang.annotation.Retention;
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
22 import java.lang.annotation.RetentionPolicy;
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
23 import java.lang.annotation.Target;
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 *
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
27 * annotation used to specify that a method is only supposed to be
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
28 * executed when running outside JPF
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 * This is useful for model classes that have methods which are intercepted
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
31 * or cut off by native peers, and we want to ensure that we never execute
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
32 * these when running under JPF. The standard case for such assertions is
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
33 * if we refer to JPF itself, and we don't want to get recursive when already
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
34 * executing under JPF
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
35 */
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
36 @Retention(RetentionPolicy.RUNTIME)
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
37 @Target({ElementType.METHOD})
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
38 public @interface NoJPFExecution {
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
39 }