comparison src/tests/gov/nasa/jpf/test/mc/basic/ExceptionInjectorTest.java @ 0:61d41facf527

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.test.mc.basic;
20
21 import gov.nasa.jpf.util.test.TestJPF;
22
23 import java.io.File;
24 import java.io.IOException;
25
26 import org.junit.Test;
27
28 /**
29 * regression test for ExceptionInjector listener
30 */
31 public class ExceptionInjectorTest extends TestJPF {
32
33 @Test
34 public void testAbsLine () {
35 if (verifyNoPropertyViolation("+listener=.listener.ExceptionInjector",
36 "+ei.exception=java.lang.ArithmeticException@gov.nasa.jpf.test.mc.basic.ExceptionInjectorTest:41")){
37 boolean handled = false;
38 try {
39 int x = 10;
40 int y = 2;
41 int z = x / y; // <<<< perfectly fine, but we want it to blow up , line 41
42 } catch (ArithmeticException ax){ // ..so that we can check the handler
43 handled = true;
44 System.out.println("got it handled");
45 ax.printStackTrace();
46 }
47
48 assert handled : "failed to throw exception";
49 }
50 }
51
52 static class Zapp extends RuntimeException {
53 Zapp (String details){
54 super(details);
55 }
56 }
57
58 // NOTE - offsets count from the first statement line in the method body
59 @Test
60 public void testMethodOffset () {
61 if (verifyNoPropertyViolation("+listener=.listener.ExceptionInjector",
62 "+ei.exception=gov.nasa.jpf.test.mc.basic.ExceptionInjectorTest$Zapp(\"gotcha\")@gov.nasa.jpf.test.mc.basic.ExceptionInjectorTest.testMethodOffset():6")){
63 boolean handled = false;
64 try {
65 int x = 10;
66 int y = 2;
67 int z = x / y; // <<<< method offset +6: perfectly fine, but we want it to blow up
68 } catch (Zapp x){ // ..so that we can check the handler
69 handled = true;
70 System.out.println(x);
71 }
72
73 assert handled : "failed to throw exception";
74 }
75 }
76
77 @Test
78 public void testCallee () {
79 if (verifyNoPropertyViolation("+listener=.listener.ExceptionInjector",
80 "+ei.exception=java.io.IOException@java.io.File.createTempFile(java.lang.String,java.lang.String)")){
81 boolean handled = false;
82 try {
83 File f = File.createTempFile("foo", "bar");
84 } catch (IOException x){ // if the temp file could not be created (how do you force this?)
85 handled = true;
86 x.printStackTrace();
87 }
88
89 assert handled : "failed to throw exception";
90 }
91
92 }
93
94 }