pub fn parse_defs(source: &str) -> Vec<DefSpec>Expand description
Parse a source fragment containing block-shaped contract definitions
(Name(params) { body }) into a list of DefSpecs.
This is the format produced by the pred! macro and used by the bundled
assets/*-contracts.rs files:
MySafeRead(p: Ptr, T: Ty, n: Expr) { NonNull(p) && Align(p, T) && Allocated(p, T, n) }Each def 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.