pub(crate) fn parse_compounds(source: &str) -> Vec<CompoundSpec>Expand description
Parse a source fragment containing block-shaped contract definitions
(Name(params) { body }) into a list of CompoundSpecs.
This is the format produced by the pred! macro and used by the bundled
assets/*-compound-properties.rs files:
MySafeRead(p: Ptr, T: Ty, n: Expr) { NonNull(p) && Align(p, T) && Allocated(p, T, n) }Each compound may be preceded by /// doc lines (shown as the human-readable
meaning in reports); // comments and blank lines are skipped. The body
supports && (conjunction) and || (disjunction) of Tag(arg, ...) calls,
plus ( ... ) grouping for a conjunction used as a single disjunct.