[hermes] Warn on #[cfg_attr(..., path = "...")]

tools/hermes/src/parse.rs

@@ -271,6 +271,16 @@ where
             });
         }
 
+        if let Some(path_attr) = extract_cfg_attr_path(&node.attrs) {
+            log::warn!(
+                "Module '{}' uses a #[cfg_attr(..., path = \"{}\")] directive. \
+                 Hermes does not currently evaluate conditional paths; \
+                 Hermes annotations in this file may be ignored.",
+                mod_name,
+                path_attr
+            );
+        }
+
         trace!("Entering module: {}", mod_name);
         self.current_path.push(mod_name);
         syn::visit::visit_item_mod(self, node);
@@ -447,6 +457,34 @@ fn extract_path_attr(attrs: &[Attribute]) -> Option<String> {
     None
 }
 
+/// Extracts the `...` from `#[cfg_attr(..., path = "...")]` if present.
+fn extract_cfg_attr_path(attrs: &[Attribute]) -> Option<String> {
+    for attr in attrs {
+        if attr.path().is_ident("cfg_attr") {
+            let mut found_path = None;
+            // The syntax is `#[cfg_attr(condition, attr1, attr2, ...)]`; we
+            // parse the nested meta items.
+            let _ = attr.parse_nested_meta(|meta| {
+                if meta.path.is_ident("path") {
+                    if let Ok(value) = meta.value() {
+                        if let Ok(lit) = value.parse::<Lit>() {
+                            if let Lit::Str(lit_str) = lit {
+                                found_path = Some(lit_str.value());
+                            }
+                        }
+                    }
+                }
+                Ok(())
+            });
+
+            if let Some(p) = found_path {
+                return Some(p);
+            }
+        }
+    }
+    None
+}
+
 fn span_to_miette(span: proc_macro2::Span) -> SourceSpan {
     let range = span.byte_range();
     SourceSpan::new(range.start.into(), range.end - range.start)

tools/hermes/tests/fixtures/warn_cfg_attr_path/expected_status.txt

@@ -0,0 +1 @@
+success

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

@@ -0,0 +1 @@
+Hermes does not currently evaluate conditional paths

tools/hermes/tests/fixtures/warn_cfg_attr_path/rust_log.txt

@@ -0,0 +1 @@
+warn

tools/hermes/tests/fixtures/warn_cfg_attr_path/source/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "warn_cfg_attr_path"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

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

@@ -0,0 +1,7 @@
+#[cfg_attr(unix, path = "sys_unix.rs")]
+mod sys; // This triggers the warning
+
+/// ```lean
+/// theorem demo : True := trivial
+/// ```
+pub fn demo() {} // Included so the overall verification command succeeds

tools/hermes/tests/integration.rs

@@ -90,6 +90,13 @@ exec "{1}" "$@"
         // (normally, the path includes a hash of the crate's path).
         .env("HERMES_TEST_DIR_NAME", "hermes_test_target");
 
+    // Tests can specify the log level.
+    let env_log_file = test_case_root.join("rust_log.txt");
+    if env_log_file.exists() {
+        let log_level = fs::read_to_string(env_log_file)?;
+        cmd.env("RUST_LOG", log_level.trim());
+    }
+
     // Mock JSON integration
     let mock_json_file = test_case_root.join("mock_charon_output.json");
     if mock_json_file.exists() {