rapx 0.7.40

A static analysis platform for Rust program analysis and verification
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

//! Contract parsing, resolution, and rendering.
//!
//! Three front-ends (inline attributes, embedded JSON, and `pred!`-style
//! compound-property macros, plus the pest DSL for expressions) all funnel into
//! `Property::parse_list`, producing a single IR defined in [`types`].
//!
//! ## Layering
//!
//! Contracts go through two stages, each with its own type:
//!
//! ```text
//! #[rapx::requires(...)] text        std-*.json            pred!(...) / def_property
//!    └─ attr.rs ──▶ AttrProperty      └─ json.rs ──▶ JsonProperty   └─ compound.rs ──▶ CompoundSpec
//!                      └────────────────── builder.rs ──────────────────▶ Property   (Atom | Or)
//! ```
//!
//! Within the resolved IR, the naming follows granularity rather than stage:
//! `Property*` names the formula level (`Property`, `PropertyKind`,
//! `PropertyArg`), while `Contract*` names the expression sub-language that
//! fills `PropertyArg::Expr` (`ContractPlace`, `ContractExpr`,
//! `ContractProjection`).

pub(crate) mod attr;
pub(crate) mod builder;
pub(crate) mod compound;
pub(crate) mod json;
pub(crate) mod pest_conv;
pub(crate) mod pest_grammar;
pub(crate) mod place;
pub(crate) mod render;
pub(crate) mod resolve;
pub(crate) mod spec;
pub(crate) mod types;

pub(crate) use types::*;