@@ -1737,44 +1737,26 @@ pub trait MachineCallback<'tcx, T>: VisitProvenance {
1737
1737
/// Type alias for boxed machine callbacks with generic argument type.
1738
1738
pub type DynMachineCallback < ' tcx , T > = Box < dyn MachineCallback < ' tcx , T > + ' tcx > ;
1739
1739
1740
- /// Creates a callback for blocking operations with captured state.
1740
+ /// Creates a `DynMachineCallback`:
1741
1741
///
1742
- /// When a thread blocks on a resource (as defined in `enum BlockReason`), this callback
1743
- /// executes once that resource becomes available. The callback captures needed
1744
- /// variables and handles the completion of the blocking operation.
1745
- ///
1746
- /// # Example
1747
1742
/// ```rust
1748
- /// // Block thread until mutex is available
1749
- /// this.block_thread(
1750
- /// BlockReason::Mutex,
1751
- /// None,
1752
- /// callback!(
1753
- /// @capture<'tcx> {
1754
- /// mutex_ref: MutexRef,
1755
- /// retval: Scalar,
1756
- /// dest: MPlaceTy<'tcx>,
1757
- /// }
1758
- /// |this, unblock: UnblockKind| {
1759
- /// // Verify successful mutex acquisition
1760
- /// assert_eq!(unblock, UnblockKind::Ready);
1761
- ///
1762
- /// // Enter critical section
1763
- /// this.mutex_lock(&mutex_ref);
1764
- ///
1765
- /// // Process protected data and store result
1766
- /// this.write_scalar(retval, &dest)?;
1767
- ///
1768
- /// // Exit critical section implicitly when callback completes
1769
- /// interp_ok(())
1770
- /// }
1771
- /// ),
1772
- /// );
1743
+ /// callback!(
1744
+ /// @capture<'tcx> {
1745
+ /// var1: Ty1,
1746
+ /// var2: Ty2<'tcx>,
1747
+ /// }
1748
+ /// |this, arg: ArgTy| {
1749
+ /// // Implement the callback here.
1750
+ /// todo!()
1751
+ /// }
1752
+ /// )
1773
1753
/// ```
1754
+ ///
1755
+ /// All the argument types must implement `VisitProvenance`.
1774
1756
#[ macro_export]
1775
1757
macro_rules! callback {
1776
1758
( @capture<$tcx: lifetime $( , ) ? $( $lft: lifetime) ,* >
1777
- { $( $name: ident: $type: ty) ,* $( , ) ? }
1759
+ { $( $name: ident: $type: ty) ,* $( , ) ? }
1778
1760
|$this: ident, $arg: ident: $arg_ty: ty| $body: expr $( , ) ?) => { {
1779
1761
struct Callback <$tcx, $( $lft) ,* > {
1780
1762
$( $name: $type, ) *
0 commit comments