google · joshlf · Apr 7, 2026 · Apr 6, 2026
diff --git a/hermes/tests/fixtures/dst_layout/expected.stderr b/hermes/tests/fixtures/dst_layout/expected.stderr
@@ -0,0 +1 @@
+\n
diff --git a/hermes/tests/fixtures/dst_layout/hermes.toml b/hermes/tests/fixtures/dst_layout/hermes.toml
@@ -5,4 +5,5 @@ Minimal reproduction of KnownLayout bounding DstLayout's attributes.
 [test]
 # Temporarily allowing this to fail while we debug other things.
 expected_status = "known_bug"
+stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry", "--unsound-allow-is-valid"]
diff --git a/hermes/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/expected.stderr b/hermes/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/expected.stderr
@@ -0,0 +1,13 @@
+   Compiling test_7_1_phantom_fn v0.1.0 ([PROJECT_ROOT])
+warning: when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item
+
+
+thread 'rustc' (<ID>) panicked at src/errors.rs:278:13:
+when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+ERROR Compilation panicked
+error: could not compile `test_7_1_phantom_fn` (lib)
+
+Caused by:
+  process didn't exit successfully: `[CACHE_ROOT]/charon-driver [RUSTUP_TOOLCHAIN]/bin/rustc --crate-name test_7_1_phantom_fn --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata=<HASH> -C extra-filename=-<HASH> --out-dir [PROJECT_ROOT]/target/hermes/cargo_target/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/hermes/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/hermes/cargo_target/x86_64-unknown-linux-gnu/debug/deps -L dependency=[PROJECT_ROOT]/target/hermes/cargo_target/debug/deps --remap-path-prefix=tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn=/dummy` (exit status: 101)
+Error: Charon failed with status: exit status: 101
diff --git a/hermes/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/hermes.toml b/hermes/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/hermes.toml
@@ -5,4 +5,5 @@ Behavior: Uses conditionally compiled functions (`#[cfg(target_os = ...)]`). Ver
 
 [test]
 expected_status = "failure"
+stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]
diff --git a/hermes/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/expected.stderr b/hermes/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/expected.stderr
@@ -0,0 +1,17 @@
+   Compiling test_7_3_ghost_spec v0.1.0 ([PROJECT_ROOT])
+warning: when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item
+  --> src/lib.rs:18:36
+   |
+18 | pub fn linux_only() -> u32 { 100 }
+   |                                   ^
+
+
+thread 'rustc' (<ID>) panicked at src/errors.rs:278:13:
+when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+ERROR Compilation panicked
+error: could not compile `test_7_3_ghost_spec` (lib)
+
+Caused by:
+  process didn't exit successfully: `[CACHE_ROOT]/charon-driver [RUSTUP_TOOLCHAIN]/bin/rustc --crate-name test_7_3_ghost_spec --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata=<HASH> -C extra-filename=-<HASH> --out-dir [PROJECT_ROOT]/target/hermes/cargo_target/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/hermes/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/hermes/cargo_target/x86_64-unknown-linux-gnu/debug/deps -L dependency=[PROJECT_ROOT]/target/hermes/cargo_target/debug/deps --remap-path-prefix=tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec=/dummy` (exit status: 101)
+Error: Charon failed with status: exit status: 101
diff --git a/hermes/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/hermes.toml b/hermes/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/hermes.toml
@@ -5,4 +5,5 @@ Behavior: Provides annotated functions under `#[cfg]`. Verifies only the specifi
 
 [test]
 expected_status = "failure"
+stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]
diff --git a/hermes/tests/fixtures/edge_cases_charon/test_8_2_unions/expected.stderr b/hermes/tests/fixtures/edge_cases_charon/test_8_2_unions/expected.stderr
@@ -0,0 +1,22 @@
+Error: Aeneas failed for package 'test_8_2_unions' with status: exit status: 2
+stderr:
+Applied prepasses:  [----------------------------------------------------] 0/2 ⠋Applied prepasses:  [##########################--------------------------] 1/2 ⠋Applied prepasses:  [####################################################] 2/2 ✔️
+Uncaught exception:
+
+  (Failure
+    "unions are not supported\
+   \nSource: 'src/lib.rs', lines 2:0-5:1\
+   \nCompiler source: llbc/TypesAnalysis.ml, line 503")
+
+Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 120, characters 4-23
+Called from Aeneas__Errors.craise in file "Errors.ml" (inlined), line 126, characters 2-43
+Called from Aeneas__TypesAnalysis.analyze_type_decl in file "llbc/TypesAnalysis.ml", line 503, characters 19-74
+Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
+Called from Aeneas__TypesAnalysis.analyze_type_declaration_group.analyze in file "llbc/TypesAnalysis.ml", lines 554-556, characters 6-23
+Called from Aeneas__Interp.analyze_type_declarations.(fun) in file "interp/Interp.ml", line 31, characters 10-62
+Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
+Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 153, characters 19-66
+Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 290, characters 18-40
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2100, characters 31-71
+Called from Dune__exe__Main in file "Main.ml", lines 726-727, characters 8-37
+
diff --git a/hermes/tests/fixtures/edge_cases_charon/test_8_2_unions/hermes.toml b/hermes/tests/fixtures/edge_cases_charon/test_8_2_unions/hermes.toml
@@ -5,4 +5,5 @@ Behavior: Delcares a `pub union U { ... }` and accesses it in an `unsafe` block.
 
 [test]
 expected_status = "failure"
+stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]
diff --git a/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/expected.stderr b/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/expected.stderr
@@ -0,0 +1 @@
+\n
diff --git a/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml b/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml
@@ -7,4 +7,5 @@ Behavior: In an `isValid` boundary condition, queries the default instantiation
 # FIXME(#3089): Update the syntax in `lib.rs` to be valid Lean, and get this
 # passing.
 expected_status = "known_bug"
+stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry", "--unsound-allow-is-valid"]
diff --git a/hermes/tests/fixtures/edge_cases_logic/test_5_4_std_types/expected.stderr b/hermes/tests/fixtures/edge_cases_logic/test_5_4_std_types/expected.stderr
@@ -0,0 +1,24 @@
+[External Error] generated/Test54StdTypesTest54StdTypes<HASH>/Test54StdTypesTest54StdTypes<HASH>.lean: Function expected at
+  Vec
+but this term has type
+  ?m.1
+
+Note: Expected a function because this term is being applied to the argument
+  Std.U32
+[External Error] generated/Test54StdTypesTest54StdTypes<HASH>/Test54StdTypesTest54StdTypes<HASH>.lean: Function expected at
+  Vec
+but this term has type
+  ?m.1
+
+Note: Expected a function because this term is being applied to the argument
+  Std.U32
+[External Error] generated/Test54StdTypesTest54StdTypes<HASH>/Test54StdTypesTest54StdTypes<HASH>.lean: Function expected at
+  Vec
+but this term has type
+  ?m.1
+
+Note: Expected a function because this term is being applied to the argument
+  Std.U32
+
+Hint: The identifier `Vec` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
+Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.
diff --git a/hermes/tests/fixtures/edge_cases_logic/test_5_4_std_types/hermes.toml b/hermes/tests/fixtures/edge_cases_logic/test_5_4_std_types/hermes.toml
@@ -5,4 +5,5 @@ Behavior: Uses `Vec` and `String` directly in function signatures. Confirms the
 
 [test]
 expected_status = "failure"
+stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]
diff --git a/hermes/tests/fixtures/edge_cases_modules/test_6_1_external_crate/expected.stderr b/hermes/tests/fixtures/edge_cases_modules/test_6_1_external_crate/expected.stderr
@@ -0,0 +1 @@
+\n
diff --git a/hermes/tests/fixtures/edge_cases_modules/test_6_1_external_crate/hermes.toml b/hermes/tests/fixtures/edge_cases_modules/test_6_1_external_crate/hermes.toml
@@ -5,4 +5,5 @@ Behavior: Imports and uses `std::collections::HashMap` in a signature. Validates
 
 [test]
 expected_status = "known_bug"
+stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]
diff --git a/hermes/tests/fixtures/edge_cases_modules/test_6_3_renaming/expected.stderr b/hermes/tests/fixtures/edge_cases_modules/test_6_3_renaming/expected.stderr
@@ -0,0 +1 @@
+\n
diff --git a/hermes/tests/fixtures/edge_cases_modules/test_6_3_renaming/hermes.toml b/hermes/tests/fixtures/edge_cases_modules/test_6_3_renaming/hermes.toml
@@ -5,4 +5,5 @@ Behavior: Re-aliases `Vec` using `use ... as MyVec;`. Ensures Charon de-aliases
 
 [test]
 expected_status = "known_bug"
+stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]
diff --git a/hermes/tests/fixtures/edge_cases_mut_refs/test_3_3_ret_mut/expected.stderr b/hermes/tests/fixtures/edge_cases_mut_refs/test_3_3_ret_mut/expected.stderr
@@ -0,0 +1,31 @@
+[External Error] generated/Test33RetMutTest33RetMut<HASH>/Test33RetMutTest33RetMut<HASH>.lean: Function expected at
+  Vec
+but this term has type
+  ?m.1
+
+Note: Expected a function because this term is being applied to the argument
+  Std.U32
+[External Error] generated/Test33RetMutTest33RetMut<HASH>/Test33RetMutTest33RetMut<HASH>.lean: Function expected at
+  Vec
+but this term has type
+  ?m.1
+
+Note: Expected a function because this term is being applied to the argument
+  Std.U32
+[External Error] generated/Test33RetMutTest33RetMut<HASH>/Test33RetMutTest33RetMut<HASH>.lean: Function expected at
+  Vec
+but this term has type
+  ?m.1
+
+Note: Expected a function because this term is being applied to the argument
+  Std.U32
+[External Error] generated/Test33RetMutTest33RetMut<HASH>/Test33RetMutTest33RetMut<HASH>.lean: Function expected at
+  Vec
+but this term has type
+  ?m.1
+
+Note: Expected a function because this term is being applied to the argument
+  Std.U32
+
+Hint: The identifier `Vec` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
+Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.
diff --git a/hermes/tests/fixtures/edge_cases_mut_refs/test_3_3_ret_mut/hermes.toml b/hermes/tests/fixtures/edge_cases_mut_refs/test_3_3_ret_mut/hermes.toml
@@ -5,4 +5,5 @@ Behavior: Mutates a vector to return an inner value (`v.pop()`). Validates Aenea
 
 [test]
 expected_status = "failure"
+stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]
diff --git a/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/expected.stderr b/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/expected.stderr
@@ -0,0 +1 @@
+\n
diff --git a/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/hermes.toml b/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/hermes.toml
@@ -6,4 +6,5 @@ Behavior: Asserts that `fn theorem()`, `fn match()`, etc. are strictly escaped i
 [test]
 # FIXME(#3089): This should succeed
 expected_status = "known_bug"
+stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]