secrust 0.1.0-alpha.3

A Rust crate for source-level verification using Weakest Precondition calculus.
Documentation 
1
2
3
4
5
6
7
8
9
10
11

use syn::ExprReturn;
use quote::quote;
use crate::cfg_builder::{CfgBuilder, CfgNode};

impl CfgBuilder {
    pub fn handle_return_statement(&mut self, expr_return: &ExprReturn) {
        let return_expr = expr_return.expr.as_ref().map(|expr| quote!(#expr).to_string()).unwrap_or_default();
        let return_node = self.add_node(CfgNode::new_return(return_expr, expr_return.clone()));
        self.current_node = Some(return_node);
    }
}