[hermes] Add some tests for Charon invocation

gherrit-pr-id: G60bb1cd41a5fade3144a05f2bdafb2a670059e03

Author: joshlf

tools/Cargo.lock

@@ -19,7 +19,8 @@ proc-macro2 = { version = "1.0.105", features = ["span-locations"] }
 rayon = "1.11.0"
 serde = { version = "1.0.228", features = ["derive"] }
 serde_json = "1.0.149"
-syn = { version = "2.0.114", features = ["full", "visit", "extra-traits", "parsing"] }
+syn = { version = "2.0.114", features = ["full", "visit", "extra-traits", "parsing", "printing"] }
+quote = "1.0"
 thiserror = "2.0.18"
 walkdir = "2.5.0"
 
@@ -31,6 +32,9 @@ assert_cmd = "2.1.2"
 tempfile = "3.24.0"
 predicates = "3.1.3"
 datatest-stable = "0.3.3"
+serde = { version = "1.0", features = ["derive"] }
+toml = "0.8"
+which = "6.0"
 
 [[test]]
 name = "integration"

tools/hermes/Cargo.toml

@@ -30,8 +30,11 @@ pub fn run_charon(args: &Args, roots: &Roots, packages: &[HermesArtifact]) -> Re
         // Fail fast on errors
         cmd.arg("--abort-on-error");
 
-        // Start translation from specific entry points
-        cmd.arg("--start-from").arg(artifact.start_from.join(","));
+        // Start translation from specific entry points. Sort to ensure
+        // deterministic ordering for testing (not important in production).
+        let mut start_from = artifact.start_from.clone();
+        start_from.sort();
+        cmd.arg("--start-from").arg(start_from.join(","));
 
         // Separator for the underlying cargo command
         cmd.arg("--");

tools/hermes/src/charon.rs

@@ -21,4 +21,13 @@ pub enum HermesError {
         span: SourceSpan,
         msg: String,
     },
+    #[error("Nested item error: {msg}")]
+    #[diagnostic(code(hermes::nested_item))]
+    NestedItemError {
+        #[source_code]
+        src: miette::NamedSource<String>,
+        #[label("this item is defined inside a function body")]
+        span: miette::SourceSpan,
+        msg: String,
+    },
 }