Merge pull request #24 from os-checker/sync

Sync: nightly-2025-04-07 from kani

Author: zjp-CN

.github/index.html

@@ -53,7 +53,7 @@ <h2>Distributed Verification API docs</h2>
       <a href="./distributed_verification/">distributed_verification APIs</a>
     </li>
     <li>
-      <a href="./rustc/">Rustc Internal APIs</a> (nightly-xxxx-xx-xx) required by Charon
+      <a href="./rustc/">Rustc Internal APIs</a> (nightly-xxxx-xx-xx) required by Kani
     </li>
   </ul>
 </body>

kani

@@ -31,11 +31,13 @@ pub fn analyze(tcx: TyCtxt, src_map: &SourceMap) -> Vec<SerFunction> {
     let (mono_items, callgraph) = collect_reachable_items(tcx, &entries);
 
     // Filter out non kanitool functions.
-    mono_items
+    let mut proofs: Vec<_> = mono_items
         .iter()
-        .filter_map(|item| Function::new(item, &callgraph, tcx, src_map, |x| !x.attrs.is_empty()))
-        .map(|fun| SerFunction::new(fun, tcx, src_map))
-        .collect()
+        .filter_map(|f| Function::new(f, &callgraph, tcx, src_map, |x| !x.attrs.is_empty()))
+        .collect();
+    // Sort proofs by file path and source code.
+    proofs.sort_by(|a, b| (&*a.file, &*a.func).cmp(&(&*b.file, &*b.func)));
+    proofs.into_iter().map(|fun| SerFunction::new(fun, tcx, src_map)).collect()
 }
 
 /// A Rust funtion with its file source, attributes, and raw function content.

src/functions/mod.rs

@@ -14,7 +14,7 @@ pub struct SerFunction {
     pub attrs: Vec<String>,
     /// Raw function string, including name, signature, and body.
     pub func: String,
-    /// Recursive fnction calls inside the body.
+    /// Recursive function calls inside the body.
     pub callees: Vec<Callee>,
 }