2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
19 package gov.nasa.jpf.listener;
22 import gov.nasa.jpf.Config;
23 import gov.nasa.jpf.JPF;
24 import gov.nasa.jpf.PropertyListenerAdapter;
25 import gov.nasa.jpf.annotation.JPFOption;
26 import gov.nasa.jpf.report.ConsolePublisher;
27 import gov.nasa.jpf.report.Publisher;
28 import gov.nasa.jpf.report.PublisherExtension;
29 import gov.nasa.jpf.search.Search;
30 import gov.nasa.jpf.vm.ChoiceGenerator;
31 import gov.nasa.jpf.vm.Instruction;
32 import gov.nasa.jpf.vm.VM;
33 import gov.nasa.jpf.vm.SystemState;
35 import java.io.PrintWriter;
38 * A lightweight listener to generate the error trace by printing
39 * the program instructions at transition boundaries. The idea is to have
40 * a shorter trace output that only shows the choices
42 public class ErrorTraceGenerator extends PropertyListenerAdapter implements PublisherExtension {
44 protected ChoiceGenerator<?>[] trace;
46 @JPFOption(type = "Boolean", key = "etg.show_insn", defaultValue = "true", comment = "print instruction that caused CG")
47 protected boolean showInsn = true;
49 @JPFOption(type = "Boolean", key = "etg.show_loc", defaultValue = "true", comment = "print source location that caused CG")
50 protected boolean showLoc = true;
52 @JPFOption(type = "Boolean", key = "etg.show_src", defaultValue = "true", comment = "print source line that caused CG")
53 protected boolean showSrc = true;
55 public ErrorTraceGenerator(Config conf, JPF jpf) {
56 jpf.addPublisherExtension(ConsolePublisher.class, this);
58 showInsn = conf.getBoolean("etg.show_insn", showInsn);
59 showSrc = conf.getBoolean("etg.show_src", showLoc);
60 showLoc = conf.getBoolean("etg.show_loc", showSrc);
64 public void publishPropertyViolation (Publisher p){
65 PrintWriter pw = p.getOut();
67 p.publishTopicStart("error trace choices");
71 for (ChoiceGenerator<?> cg : trace){
72 int tid = cg.getThreadInfo().getId();
73 Instruction insn = cg.getInsn();
75 if (!cg.isCascaded()){
76 pw.printf("#%2d [tid=%2d] ", i++, tid);
83 if (!cg.isCascaded()){
85 String loc = insn.getFilePos();
93 pw.println( insn.getMethodInfo());
97 pw.printf("\tinstruction: [pc=%d] %s\n", insn.getPosition(), insn);
101 String srcLine = insn.getSourceLine();
102 if (srcLine == null){
103 srcLine = "[no source]";
105 srcLine = srcLine.trim();
107 pw.print("\tsource: ");
108 pw.println( srcLine);
116 public void propertyViolated(Search search) {
117 VM vm = search.getVM();
118 SystemState ss = vm.getSystemState();
119 trace = ss.getChoiceGenerators();