[hermes] Parse Hermes attributes

gherrit-pr-id: Ib659c95874d275713cc813788024b49e87a8873d

Author: joshlf

tools/hermes/src/parse.rs

@@ -188,15 +188,28 @@ fn process_file_recursive<'a>(
                 let mut full_path = current_prefix.clone();
                 full_path.extend(item.module_path);
 
-                use parse::ParsedItem::*;
                 match &item.item {
                     // Unreliable syntaxes: we have no way of reliably naming
                     // these in Charon's `--start-from` argument, so we fall
                     // back to naming the parent module.
-                    Impl(_) | ImplItemFn(_) | TraitItemFn(_) => {
+                    parse::ParsedItem::Impl(_) => {
                         let start_from = full_path.join("::");
                         path_tx.send((name.clone(), start_from)).unwrap();
                     }
+                    parse::ParsedItem::Function(f) => match &f.item {
+                        parse::FunctionItem::Impl(_) | parse::FunctionItem::Trait(_) => {
+                            let start_from = full_path.join("::");
+                            path_tx.send((name.clone(), start_from)).unwrap();
+                        }
+                        parse::FunctionItem::Free(_) => {
+                            if let Some(item_name) = item.item.name() {
+                                full_path.push(item_name);
+                                let start_from = full_path.join("::");
+                                log::debug!("Found entry point: {}", start_from);
+                                path_tx.send((name.clone(), start_from)).unwrap();
+                            }
+                        }
+                    },
                     // Reliable syntaxes: target the specific item.
                     _ => {
                         if let Some(item_name) = item.item.name() {

tools/hermes/src/scanner.rs

@@ -1 +1 @@
-Unclosed ```lean block
+Unclosed Hermes block in documentation.

tools/hermes/tests/fixtures/broken_doc_block/expected_stderr.txt

@@ -1,3 +1,3 @@
-/// ```lean
+/// ```lean, hermes
 /// unclosed block
 fn foo() {}

tools/hermes/tests/fixtures/broken_doc_block/source/src/lib.rs

@@ -1,4 +1,4 @@
-/// ```lean
+/// ```lean, hermes
 /// theorem main_proof : True := trivial
 /// ```
 pub fn main_proof() {}

tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/app/src/lib.rs

@@ -1,6 +1,6 @@
 #[cfg(target_os = "haiku")]
 mod ghost {
-    /// ```lean
+    /// ```lean, hermes
     /// ```
     pub fn hidden() {}
 }

tools/hermes/tests/fixtures/cfg_blind_spot/source/src/lib.rs

@@ -1,3 +1,3 @@
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn utils_a() {}

tools/hermes/tests/fixtures/collision/expected/crates/a/src/lib.rs

@@ -1,3 +1,3 @@
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn utils_b() {}

tools/hermes/tests/fixtures/collision/expected/crates/b/src/lib.rs

@@ -1,3 +1,3 @@
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn utils_a() {}

tools/hermes/tests/fixtures/collision/source/crates/a/src/lib.rs

@@ -1,3 +1,3 @@
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn utils_b() {}