Attribute Macro checked 

#[checked]

Discharge SPs.

NOTE: there is no check on whether the annotated is an expression or not.

Syntax Example

#![feature(stmt_expr_attributes)]
#![feature(proc_macro_hygiene)]
#![feature(register_tool)]
#![register_tool(rapx)]

// Tag SPs:
#[requires { SP1 }] unsafe fn foo() {}
#[requires { SP1, SP2 }] unsafe fn bar() {}

// Discharge SPs:
#[checked { SP1 }] unsafe { foo() };
#[checked { SP1: "reason" }] unsafe { foo() };
#[checked { SP1, SP2: "shared reason" }] unsafe { bar() };
#[checked { SP1: "reason1"; SP2: "reason2" }] unsafe { bar() };