anodized_core/
lib.rs

1#![doc = include_str!("../README.md")]
2
3use syn::{Expr, Ident, Meta};
4
5pub mod annotate;
6pub mod instrument;
7
8#[cfg(test)]
9mod test_util;
10
11/// A spec specifies the intended behavior of a function or method.
12#[derive(Debug)]
13pub struct Spec {
14    /// Preconditions: conditions that must hold when the function is called.
15    pub requires: Vec<Condition>,
16    /// Invariants: conditions that must hold both when the function is called and when it returns.
17    pub maintains: Vec<Condition>,
18    /// Captures: expressions to snapshot at function entry for use in postconditions.
19    pub captures: Vec<Capture>,
20    /// Postconditions: conditions that must hold when the function returns.
21    pub ensures: Vec<PostCondition>,
22}
23
24/// A condition represented by a `bool`-valued expression.
25#[derive(Debug)]
26pub struct Condition {
27    /// The `bool`-valued expression.
28    pub expr: Expr,
29    /// **Static analyzers can safely ignore this field.**
30    ///
31    /// Build configuration filter to decide whether to add runtime checks.
32    /// Passed to a `cfg!()` guard in the instrumented function.
33    pub cfg: Option<Meta>,
34}
35
36/// A postcondition represented by a closure that takes the return value as a reference.
37#[derive(Debug)]
38pub struct PostCondition {
39    /// The closure that validates the postcondition, taking the function's
40    /// return value by reference, e.g. `|output| *output > 0`.
41    pub closure: syn::ExprClosure,
42    /// **Static analyzers can safely ignore this field.**
43    ///
44    /// Build configuration filter to decide whether to add runtime checks.
45    /// Passed to a `cfg!()` guard in the instrumented function.
46    pub cfg: Option<Meta>,
47}
48
49/// Captures an expression's value at function entry.
50#[derive(Debug)]
51pub struct Capture {
52    /// The expression to capture.
53    pub expr: Expr,
54    /// The identifier to bind the captured value to.
55    pub alias: Ident,
56}
anodized_core/lib.rs

anodized_core/
lib.rs
