Module contract 

Contract DSL and abstract-state data structures. Contract and abstract-state data types used by the Senryx verifier.

This module owns the contract representation parsed from RAPx safety annotations. Numeric obligations use a small expression AST so contracts can describe relationships such as region.size >= 0, offset + len <= cap, and future layout-sensitive formulas without inventing new ad-hoc range types for every property.

Structs

ContractFactSet

The set of contract facts known to hold for one graph node.

ContractPlace

A place expression referenced by a contract.

NumericPredicate

A complete numeric predicate with explicit left and right expressions.

Enums

AlignState

Tracks pointer alignment status in the abstract domain.

ContractExpr

Numeric expression AST used by length and ValidNum contracts.

ContractProjection

A projection from a contract place root.

NumericOp

Arithmetic operators supported by contract expressions.

NumericUnaryOp

Unary operators supported by contract expressions.

PlaceBase

The root of a contract expression place.

PropertyContract

A parsed safety-property contract.

RelOp

Relational operators used by numeric predicates.