anodized_core/
lib.rs

1#![doc = include_str!("../README.md")]
2
3use proc_macro2::Span;
4use syn::{Expr, Meta, Pat};
5
6pub mod annotate;
7pub mod instrument;
8
9#[cfg(test)]
10mod test_util;
11
12/// Specifies the intended behavior of a function or method.
13#[derive(Debug)]
14pub struct Spec {
15    /// Preconditions: conditions that must hold when the function is called.
16    pub requires: Vec<PreCondition>,
17    /// Invariants: conditions that must hold both when the function is called and when it returns.
18    pub maintains: Vec<PreCondition>,
19    /// Captures: expressions to snapshot at function entry for use in postconditions.
20    pub captures: Vec<Capture>,
21    /// Postconditions: conditions that must hold when the function returns.
22    pub ensures: Vec<PostCondition>,
23    /// The span in the source code, from which this spec was parsed
24    span: Span,
25}
26
27impl Spec {
28    /// Returns `true` if the spec contract is empty (specifies nothing), otherwise returns `false`
29    pub fn is_empty(&self) -> bool {
30        self.requires.is_empty()
31            && self.maintains.is_empty()
32            && self.ensures.is_empty()
33            && self.captures.is_empty()
34    }
35    /// Call to construct an error from the whole spec
36    pub fn spec_err(&self, message: &str) -> syn::Error {
37        syn::Error::new::<&str>(self.span, message)
38    }
39}
40
41/// A precondition represented by a `bool`-valued expression.
42#[derive(Debug)]
43pub struct PreCondition {
44    /// The closure that validates the precondition,
45    /// takes no input, e.g. `|| input.is_valid()`.
46    pub closure: syn::ExprClosure,
47    /// **Static analyzers can safely ignore this field.**
48    ///
49    /// Build configuration filter to decide whether to add runtime checks.
50    /// Passed to a `cfg!()` guard in the instrumented function.
51    pub cfg: Option<Meta>,
52}
53
54/// A postcondition represented by a closure that takes the return value as a reference.
55#[derive(Debug)]
56pub struct PostCondition {
57    /// The closure that validates the postcondition, taking the function's
58    /// return value by reference, e.g. `|output| *output > 0`.
59    pub closure: syn::ExprClosure,
60    /// **Static analyzers can safely ignore this field.**
61    ///
62    /// Build configuration filter to decide whether to add runtime checks.
63    /// Passed to a `cfg!()` guard in the instrumented function.
64    pub cfg: Option<Meta>,
65}
66
67/// Captures an expression's value at function entry.
68#[derive(Debug)]
69pub struct Capture {
70    /// The expression to capture.
71    pub expr: Expr,
72    /// The pattern to bind/destructure the captured value.
73    pub pat: Pat,
74}
anodized_core/lib.rs

anodized_core/
lib.rs
