Mercurial > hg > Members > kono > jpf-core

comparison doc/jpf-core/ErrorTraceGenerator.md @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 ## Error Trace Generator ##
2
3 This is a listener to output a lightweight error trace. It prints the instructions at POR boundaries or points where there are multiple choices. An example is shown below.
4
5 ~~~~~~~~
6
7 ====================### Lightweight Error Trace ###=======================
8
9
10 Length of Error Trace: 35
11 --------------------------------------------------- Thread1
12 Event.wait_for_event(oldclassic.java:79)
13 wait();
14 --------------------------------------------------- Thread2
15 SecondTask.run(oldclassic.java:129)
16 if (count == event2.count) { // <race> ditto
17 --------------------------------------------------- Thread2
18 SecondTask.run(oldclassic.java:127)
19 event1.signal_event(); // updates event1.count
20 --------------------------------------------------- Thread2
21 SecondTask.run(oldclassic.java:133)
22 count = event2.count; // <race> ditto
23 --------------------------------------------------- Thread1
24 FirstTask.run(oldclassic.java:103)
25 event1.wait_for_event();
26 --------------------------------------------------- Thread1
27
28 ~~~~~~~~
29
30 Configuration: **+listener=gov.nasa.jpf.listener.ErrorTraceGenerator**
31
32 Note the Error trace generator does not have the same memory bottlenecks as **report.console.property_violation=trace** that stores every bytecode instruction executed along the path from the start of the program to the error state. The error trace generator dynamically recreates the counterexample by tracing back to the start from the error state. The head of the error trace (list shown in the example) represents the last instruction in the error trace while the tail represents the first instruction.