Mercurial > hg > Members > kono > jpf-core

annotate src/tests/gov/nasa/jpf/test/mc/basic/NoJPFExecTest.java @ 34:49be04cc6389 default tip java9-try

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cyclic dependency ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 19 Dec 2017 11:21:23 +0900
parents e15b03204dc7
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 }