vstd: add no_unwind to swap spec

verus-lang · Nov 14, 2024 · 4edba7d · 4edba7d
1 parent 658fd94
commit 4edba7d
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/source/vstd/std_specs/core.rs b/source/vstd/std_specs/core.rs
@@ -95,6 +95,8 @@ pub fn ex_swap<T>(a: &mut T, b: &mut T)
     ensures
         *a == *old(b),
         *b == *old(a),
+    opens_invariants none
+    no_unwind
 {
     core::mem::swap(a, b)
 }