Run with Ctrl/⌘ + Enter while editing. Examples opens any program of the regression suite with its settings.
→ callee parameters, ↩ a return; ⇢ a write to a flow-insensitive global, final that global's final value
⊔ i: [0,5]paths meet, so the value covers more than this step
run_voblint: call and answer
Analyzer input, returned report, and solver trace.
Input to the Isabelle-generated run_voblint function, and its returned answer after render_report, which converts states to text. The output is serialized field by field using Isabelle's field and constructor names. Each abstract value is rendered by
its own analysis; the presentation layer only replaces ASCII symbol names such
as <top> with glyphs such as ⊤. Integers
too large for a JSON number appear as strings. The editor annotations, state
inspector, and graph are drawn from this answer by untrusted presentation code.
Run the analysis to see the call and its answer.
Input
Output
Solver trace
Solver steps recorded during the run, as printed by voblint --trace --verbose. The trace includes solved unknowns, queries and answers, side effects, updates, destabilizations, and call routing. It uses Goblint-aligned terms and indentation for query depth. A banner marks where the solver asks for a
procedure's result.
The solver result is the exported computation of proved equations, and the trace calls come from code equations proved equal to the untraced ones. The trace is an unverified observation of that computation, recorded by a hook that returns nothing, swallows exceptions and never touches solver state. The solve replay further down is an unverified visualization of the trace.
State inspector
Graph
Compiled control-flow graph with one node per program point and a state for each context.
Solve replay Step through the solve on the graph, one solver event at a time.
Steps through the solve on the control-flow graph, one solver step at a time. The solver starts from the program's exit and queries backward toward the entry. Each node shows the current value at that program point and context. Each context has a separate box, with one node per unknown. The circle at the top of each box is an entry seed. Calls publish the entry state there, and the entry equation reads it.
A reducer constructs the displayed states from the JSON Lines trace recorded during the solve. This visualization is outside the proof.
Solve stack
Open queries, innermost first. Each unknown waits for the one above it to answer.
Routes
Each call the solver evaluated, and the callee context its entry state was routed to.
Counters
Per unknown so far: right-hand-side evaluations, updates that changed its value, and removals from the stable set.
| unknown | eval | upd | destab |
|---|