Mercurial > hg > Members > kono > jpf-core

annotate src/main/gov/nasa/jpf/vm/NoJPFExec.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.vm;
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.SystemAttribute;
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
21
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
22 /**
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
23 * InfoObject attr that flags a certain construct (field, method, class) is not supposed
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
24 * to be used under JPF. Useful for model classes that have or use features which have to be
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
25 * cut off / abstracted by means of native peers, and we want to catch violations as
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
26 * early as possible
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 NoJPFExec implements SystemAttribute {
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 // we only need one
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
31 public static final NoJPFExec SINGLETON = new NoJPFExec();
e15b03204dc7 added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked
Peter Mehlitz <pcmehlitz@gmail.com>
parents:
diff changeset
32 }