Repository navigation

Preconditions - #240

Merged

sipma merged 15 commits into

static-analysis-engineering:masterfrom

sipma:preconditions

May 27, 2026

Merged

Preconditions#240
sipma merged 15 commits into
static-analysis-engineering:masterfrom
sipma:preconditions

Commits on May 6, 2026
- CHB: add infrastructure for TrustedOsCmdString
  sipma
  committed
  2efbcbe
- CHB: proof obligation discharge of TrustedOsCmdString with constant strings
  sipma
  committed
  eec6583
- CHB: delegate format-string po to api
  sipma
  committed
  d47e7e9
- CHB: add format string to function capabilities
  sipma
  committed
  ba7747f
Commits on May 7, 2026
- CHB: convert preconditions to attributes
  sipma
  committed
  8ea4083
Commits on May 14, 2026
- CHB: consolidate proof obligation discharge
  sipma
  committed
  77c4ff4
- CHB: introduce command injection predicates
  sipma
  committed
  a2a55fd
- CHB: consolidate proof obligation discharge
  sipma
  committed
  f7e7402
- CHB:ARM: add reaching definitions for string buffers
  sipma
  committed
  6cea60d
- CHB: update for proof obligation discharge
  sipma
  committed
  87efe76
Commits on May 15, 2026
- CHB:replace BCAttributes with AttributesFunctionSemantics
  sipma
  committed
  7756b56
- CHB: move conversion to attributes to separate file
  sipma
  committed
  733c431
Commits on May 16, 2026
- CHB: update sprintf summaries
  sipma
  committed
  8d591de
- CHB: add format arguments to trusted-os-cmd-fmt-string po
  sipma
  committed
  049e8f6
Commits on May 25, 2026
- CHB:PO: delegate BlockWrite without external length term
  sipma
  committed
  4ae5796