Skip to content

Proof Scripts

Jump to bottom
Hugo edited this page Sep 25, 2026 · 1 revision

Proof Scripts

Three Python runners sit at the repository root. They exist to prove a capability end to end — compile, run, collect — rather than to unit-test the code.

BTP-RUNTIME-ANALYZER.py — full sweep

Compiles every C/C++ source in test/, verifies each source produced an executable, then runs every binary with a 10 second timeout and prints stdout/stderr.

Before the directory sweep it runs a generated minimal C probe and asserts that runtime-analyzer builds an instrumented binary, executes it, captures the program output, and collects basic entry/exit lines.

python3 BTP-RUNTIME-ANALYZER.py
python3 BTP-RUNTIME-ANALYZER.py --timeout 10 -- --ct-no-alloc-trace --ct-no-trace --ct-bounds-no-abort

Non-zero binary exits are reported without failing the script, because some runtime tests abort on purpose. --strict-exit fails on any non-zero binary exit.

BTP-RUNTIME-ANALYZER_F4.py — minimal execution proof

Proves minimal execution of an instrumented binary and basic runtime collection. It generates a small C probe in runtime-analyzer-artifacts/, compiles it with runtime-analyzer, verifies the instrumented binary exists and is executable, then checks that the program output and the entry/exit collection were captured.

python3 BTP-RUNTIME-ANALYZER_F4.py
python3 BTP-RUNTIME-ANALYZER_F4.py --build-first

BTP-RUNTIME-ANALYZER_F11.py — bounds overflow proof

Proves runtime overflow detection through CoreTrace bounds instrumentation. It uses an existing ct_bounds_overflow fixture if test/ has one, otherwise it generates a small heap-overflow probe in runtime-analyzer-artifacts/.

The proof expects three things together:

  1. a generated instrumented binary,
  2. a runtime heap-buffer-overflow report,
  3. a non-zero bounds_errors collection count.

Checking the report and the counter is the point: it proves the runtime detected the overflow and that the collection saw it.

python3 BTP-RUNTIME-ANALYZER_F11.py
python3 BTP-RUNTIME-ANALYZER_F11.py --no-color

Status checks print the tested file name in purple, green OK for validated conditions, red NO for missing ones, and separate file reports with --------. --no-color drops the colouring.

Code style

./scripts/format.sh          # format
./scripts/format-check.sh    # verify only
cmake --build build --target format
cmake --build build --target format-check

Target version: clang-format 17, the version CI uses. The clang-format GitHub Actions job fails when formatting diverges.

Home

Clone this wiki locally