-
Notifications
You must be signed in to change notification settings - Fork 2
Breakpoints (advanced guide)
This page provides some additional information on breakpoints.
Basic information is available on these pages:
Unlike traditional debuggers where breakpoints are mostly associated with a line in the program code and with optionally some boolean expression that must be met, Inspector breakpoints may break without reference to a specific line in the source code. It then becomes important to know when exactly do they hit.
For most hit conditions, the breakpoint stops the program just before the event that triggers it. For example, if you use the instruction_type
hit condition, it stops before the instruction of the specified type (this is a reversal from how JPF Inspector worked before the 2016 update).
Some hit conditions, however, hit only after the event. For example, object_created
stops execution after the new instance is created. In these cases, execution is stopped just before the next instruction that would be executed, in any thread, after the triggering event occurs.
There are other ways execution can pause, too; the comprehensive list is:
- Breakpoint hit: This will always leave you just before an instruction, you can perform any actions as normal.
-
Choice generator prompt: You can inspect program state using
print
and select a choice usingcg select
. However, at this point, there may not be a valid program counter and back-stepping features will not work. -
Break: The command
break
can stop the program at many points. No stepping commands are guaranteed to work while execution is paused this way.
In traditional debuggers, each breakpoint has an associated hit count which is the number of times it was triggered. The user may then specify that he or she only wants to be informed when the hit count reaches a specified number, for example.
JPF Inspector breakpoints also have a hit counter but they have two of them:
- the path hit count behaves as hit counters in ordinary debuggers and limits related to hit count use this hit counter; i.e. the "hit count check" in the command
create breakpoint
uses this counter. JPF may backtrack through a breakpoint, in which case the path hit count is decremented. - the total hit count is the total number of times this breakpoint was hit while this instance of JPF Inspector was running; it maintains its value even through backtracking, and it maintains its value even through multiple
run
commands that rerun JPF. Total hit count is informational only and you cannot set any conditions related to it.
A breakpoint may be in one of three states (its state may be specified in the create breakpoint
command):
-
enable
(en
) which means that when the breakpoint's hit condition becomes true, execution is stopped and information about the breakpoint is printed to the console. The hit counts are updated -
log
which means that execution won't be stopped, but information about the hit will be printed to the Inspector console; hit counts will be updated, though -
disable
(dis
) which means that the breakpoint's hit counts are still being updated but that the user won't be informed when the breakpoint hits and execution will continue as normal
It is possible to change a breakpoint's state using the command change breakpoint
.
In the configuration files, you may set up "ignored classes" (see JPF Inspector Configuration). If a breakpoint hit condition would be true inside one of these ignored classes, then the hit is totally ignored and not even hit counts are incremented.
-
User Documentation
-
User Guide
- Legacy User Guide
- Tutorial: Debugging an example application
- [How-to: Add the Inspector to your application](User Guide#launching-jpf-inspector)
- How-to: Use the Inspector with Symbolic Pathfinder
- Advanced topics
- GUI
- Extensibility
-
User Guide
-
Maintainer Documentation
- History
- 2016 Changelog
- [JPF Startup sequence](JPF Startup)
- [JPF Inspector Startup sequence](JPF Inspector Startup)
- [JPF Inspector Architecture](JPF Inspector Architecture)
- Migration from JPF6 to JPF8
- Naming and Code Style
- Threads in JPF Inspector
- Hierarchies
- Javadoc Class Documentation