• Home
  • Features
  • Pricing
  • Docs
  • Announcements
  • Sign In

vbpf / prevail / 22081081213
88%

Build:
DEFAULT BRANCH: main
Ran 17 Feb 2026 12:10AM UTC
Jobs 2
Files 74
Run time 1min
Badge
Embed ▾
README BADGES
x

If you need to use a raster PNG badge, change the '.svg' to '.png' in the link

Markdown

Textile

RDoc

HTML

Rst

16 Feb 2026 11:57PM UTC coverage: 87.142% (+0.02%) from 87.121%
22081081213

push

github

web-flow
Replace patricia tree with std::map (#1008)

Empirically, the median collection holds ~3 cells, overlap queries hit
<5% of the time, and the offset map is <1% of verifier runtime. At these
sizes, the patricia tree provided no benefit over std::map while adding
an external dependency.

- Remove radix_tree submodule dependency and offset_t bit-manipulation helpers
- Replace patricia tree with std::map<offset_t, std::set<Cell>>
- Simplify Cell to a plain struct with public (offset, size) fields
- Use defaulted == and <=> instead of manual comparison operators
- Replace Interval-based overlap check with direct integer arithmetic
- Move to_interval, symbolic_overlap, operator<< to free functions
- Inline get_scalar() as variable_registry->cell_var() at all call sites
- Document offset bound invariant in Cell::overlap
- Add assert(sz > 0) in Cell::overlap to document the invariant
- Simplify largest-cell lookup in get_overlap_cells_symbolic_offset:
  std::set is already sorted by (offset, size), so *rbegin() suffices
- Fix bug in backward scan of get_overlap_cells: remove early break
  that could skip overlapping cells at earlier offsets (a bucket with
  small cells may not overlap while an earlier bucket with larger
  cells does)
- Add assertion that offset <= EBPF_TOTAL_STACK_SIZE before the
gsl::narrow<int> conversion, documenting the precondition that
makes the narrowing safe.
- Add regression test for backward scan early-break bug

YAML test: writing to a sub-range of a cell must kill the cell so that a subsequent full-range
load returns unknown rather than the stale value.
The observation r0.svalue=0 (consistent mode) passes when the cell is correctly
havoced (0 is consistent with unknown) but fails when the stale
value r0.svalue=99 persists.

Verified: test fails when both the old remove_cell (no tombstone
cleanup) and the early break are reintroduced.
- Extract cell_var(kind, cell) helper to reduce repetition of
  variable_registry->cell_var(kind, c... (continued)

57 of 59 new or added lines in 1 file covered. (96.61%)

2 existing lines in 1 file now uncovered.

9319 of 10694 relevant lines covered (87.14%)

3049375.43 hits per line

New Missed Lines in Diff

Lines Coverage ∆ File
2
86.67
0.47% src/crab/array_domain.cpp

Uncovered Existing Lines

Lines Coverage ∆ File
2
86.67
0.47% src/crab/array_domain.cpp
Jobs
ID Job ID Ran Files Coverage
1 run-Release - 22081081213.1 17 Feb 2026 12:10AM UTC 74
86.26
GitHub Action Run
2 run-Debug - 22081081213.2 17 Feb 2026 12:49AM UTC 74
85.02
GitHub Action Run
Source Files on build 22081081213
  • Tree
  • List 74
  • Changed 1
  • Source Changed 0
  • Coverage Changed 1
Coverage ∆ File Lines Relevant Covered Missed Hits/Line
  • Back to Repo
  • 3745b88e on github
  • Prev Build on main (#22071284931)
  • Next Build on main (#22153083365)
  • Delete
STATUS · Troubleshooting · Open an Issue · Sales · Support · CAREERS · ENTERPRISE · START FREE · SCHEDULE DEMO
ANNOUNCEMENTS · TWITTER · TOS & SLA · Supported CI Services · What's a CI service? · Automated Testing

© 2026 Coveralls, Inc