Skip to content

Commit

Permalink
Solve #61 and fix grammar
Browse files Browse the repository at this point in the history
  • Loading branch information
karoliineh authored Jun 26, 2024
1 parent d3b0747 commit f93eb24
Showing 1 changed file with 9 additions and 7 deletions.
16 changes: 9 additions & 7 deletions Readme.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ The Integration of the static analyzer [Goblint](https://github.com/goblint/anal
2. Download [GobPie plugin](https://nightly.link/goblint/GobPie/workflows/build/master/gobpie-plugin.zip) and unzip the archive.
3. Install the extension into VSCode with `code --install-extension gobpie-0.0.4.vsix`.

When installing goblint locally (as recommended), **make sure that GobPie can find the correct version Goblint**.
When installing goblint locally (as recommended), **make sure that GobPie can find the correct version of Goblint**.
This can be done in two ways:

* Setting the location of the Goblint executable used by GobPie in `gobpie.json`:
Expand All @@ -20,7 +20,7 @@ This can be done in two ways:
```
The *installation path* is the path to your Goblint installation.
* Activating the right opam switch before starting vscode:
* Activating the right opam switch before starting VS Code:
```shell
eval $(opam env --switch=<switch name> --set-switch)
code .
Expand Down Expand Up @@ -53,6 +53,8 @@ Example GobPie configuration file `gobpie.json`:
* `abstractDebugging` - if [abstract debugging](#abstract-debugging) is enabled (this automatically enables ARG generation) (optional, default `false`)
* `showCfg` - if the code actions for showing the function's CFGs are shown (optional, default `false`)
* `incrementalAnalyisis` - if Goblint should use incremental analysis (disabling this may, in some cases, improve the stability of Goblint) (optional, default `true`)
* `explodeGroupWarnings` - if Goblint's group warnings are "exploded", meaning that the group warning is shown at each location of an individual warning within it, or if they are not "exploded", meaning the group warning is shown only at a single defined location.
Currently, it only affects data race warnings, so if enabled, the data race warning will be shown at the location of each of the accesses, and if disabled, the warning will be shown only at the variable that is accessed. (optional, default `true`).

#### Goblint configuration

Expand All @@ -76,14 +78,14 @@ GobPie includes a special debugger called an **abstract debugger**, that uses th
Once GobPie is installed and configured (see previous two sections), the debugger can be started by simply selecting "C (GobPie Abstract Debugger)" from the Run and Debug panel in VS Code and starting the debugger as normal.
Note: Abstract debugging is disabled by default. It must be explicitly enabled in `gobpie.json` before starting GobPie.

The debugger supports breakpoints, including conditional breakpoints, shows the call stack and values of variables, allows interactively evaluating expressions and setting watch expressions and supports most standard stepping operations.
The debugger supports breakpoints, including conditional breakpoints, shows the call stack and values of variables, allows interactive evaluation of expressions and setting watch expressions, and supports most standard stepping operations.

In general the abstract debugger works analogously to a normal debugger, but instead of stepping through a running program, it steps through the program ARG generated by Goblint during analysis.
In general, the abstract debugger works analogously to a normal debugger, but instead of stepping through a running program, it steps through the program's ARG generated by Goblint during analysis.
Values of variables and expressions are obtained from the Goblint base analysis and are represented using the base analysis abstract domain.
The function call stack is constructed by traversing the ARG from the current node to the program entrypoint.
In case of multiple possible call stacks all possible callers at the location where call stacks diverge are shown. To view the call stack of one possible caller the restart frame operation can be used to restart the frame of the desired caller, which moves the active location to the start of the selected caller's frame.
The function call stack is constructed by traversing the ARG from the current node to the program entry point.
In case of multiple possible call stacks, all possible callers at the location where call stacks diverge are shown. To view the call stack of one possible caller, the restart frame operation can be used to restart the frame of the desired caller, which moves the active location to the start of the selected caller's frame.

When there are multiple possible ARG nodes at the location of a breakpoint then all possible ARG nodes are shown at the same time as threads.
When there are multiple possible ARG nodes at the location of a breakpoint, then all possible ARG nodes are shown at the same time as threads.
When a step is made in one thread, an equivalent step is made in all other threads. An equivalent step is one that leads to the same CFG node. This means that all threads are synchronized such that stepping to an ARG node in one thread ensures that all threads are at an ARG node with the same corresponding CFG node.

## Developing
Expand Down

0 comments on commit f93eb24

Please sign in to comment.