wip

verus-lang · Jul 5, 2024 · a432617 · a432617
1 parent c3d2e50
commit a432617
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 3 deletions.
diff --git a/examples/foo.rs b/examples/foo.rs
@@ -0,0 +1,10 @@
+mod foo {
+    verus! {
+
+fn foo() {
+}
+
+// x
+// y
+} // verus!
+}
diff --git a/examples/ironfleet.rs b/examples/ironfleet.rs
@@ -2899,7 +2899,6 @@ pub open spec fn is_valid_lio_op<IdType, MessageType>(
 // send interaces.
 // LIoOpOrderingOKForAction
 // LIoOpSeqCompatibleWithReduction
-
 } // verus!
     // verus
 }
@@ -12360,7 +12359,6 @@ pub proof fn flatten_sets_singleton_auto<A>()
 
 // TODO(Tej): We strongly suspect there is a trigger loop in these auto
 // lemmas somewhere, but it's not easy to see from the profiler yet.
-
 } // verus!
     }
 }

diff --git a/examples/pagetable.rs b/examples/pagetable.rs
@@ -10722,7 +10722,6 @@ pub open spec fn next(s1: HWVariables, s2: HWVariables) -> bool {
 //         HWStep::TLBEvict { vaddr }                  => (),
 //     }
 // }
-
 } // verus!
     }
-Original file line number
+Diff line change
@@ Expand Up @@
     //         HWStep::TLBEvict { vaddr }                  => (),
     //     }
     // }
     } // verus!
         }
@@ Expand Down @@