Skip to content

Commit 9252871

Browse files
authored
[hermes] Track output for more integration tests (#3209)
gherrit-pr-id: G5hqizeipgnmwhocpqscopsoqtirndpdi
1 parent 001feb5 commit 9252871

36 files changed

Lines changed: 440 additions & 9 deletions

File tree

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
\n

hermes/tests/fixtures/dst_layout/hermes.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,4 +5,5 @@ Minimal reproduction of KnownLayout bounding DstLayout's attributes.
55
[test]
66
# Temporarily allowing this to fail while we debug other things.
77
expected_status = "known_bug"
8+
stderr_file = "expected.stderr"
89
args = ["verify", "--allow-sorry", "--unsound-allow-is-valid"]
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
Compiling test_7_1_phantom_fn v0.1.0 ([PROJECT_ROOT])
2+
warning: when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item
3+
4+
5+
thread 'rustc' (<ID>) panicked at src/errors.rs:278:13:
6+
when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item
7+
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
8+
ERROR Compilation panicked
9+
error: could not compile `test_7_1_phantom_fn` (lib)
10+
11+
Caused by:
12+
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)
13+
Error: Charon failed with status: exit status: 101

hermes/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/hermes.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,4 +5,5 @@ Behavior: Uses conditionally compiled functions (`#[cfg(target_os = ...)]`). Ver
55

66
[test]
77
expected_status = "failure"
8+
stderr_file = "expected.stderr"
89
args = ["verify", "--allow-sorry"]
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
Compiling test_7_3_ghost_spec v0.1.0 ([PROJECT_ROOT])
2+
warning: when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item
3+
--> src/lib.rs:18:36
4+
|
5+
18 | pub fn linux_only() -> u32 { 100 }
6+
| ^
7+
8+
9+
thread 'rustc' (<ID>) panicked at src/errors.rs:278:13:
10+
when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item
11+
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
12+
ERROR Compilation panicked
13+
error: could not compile `test_7_3_ghost_spec` (lib)
14+
15+
Caused by:
16+
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)
17+
Error: Charon failed with status: exit status: 101

hermes/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/hermes.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,4 +5,5 @@ Behavior: Provides annotated functions under `#[cfg]`. Verifies only the specifi
55

66
[test]
77
expected_status = "failure"
8+
stderr_file = "expected.stderr"
89
args = ["verify", "--allow-sorry"]
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
Error: Aeneas failed for package 'test_8_2_unions' with status: exit status: 2
2+
stderr:
3+
Applied prepasses: [----------------------------------------------------] 0/2 ⠋Applied prepasses: [##########################--------------------------] 1/2 ⠋Applied prepasses: [####################################################] 2/2 ✔️
4+
Uncaught exception:
5+
6+
(Failure
7+
"unions are not supported\
8+
\nSource: 'src/lib.rs', lines 2:0-5:1\
9+
\nCompiler source: llbc/TypesAnalysis.ml, line 503")
10+
11+
Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 120, characters 4-23
12+
Called from Aeneas__Errors.craise in file "Errors.ml" (inlined), line 126, characters 2-43
13+
Called from Aeneas__TypesAnalysis.analyze_type_decl in file "llbc/TypesAnalysis.ml", line 503, characters 19-74
14+
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
15+
Called from Aeneas__TypesAnalysis.analyze_type_declaration_group.analyze in file "llbc/TypesAnalysis.ml", lines 554-556, characters 6-23
16+
Called from Aeneas__Interp.analyze_type_declarations.(fun) in file "interp/Interp.ml", line 31, characters 10-62
17+
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
18+
Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 153, characters 19-66
19+
Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 290, characters 18-40
20+
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2100, characters 31-71
21+
Called from Dune__exe__Main in file "Main.ml", lines 726-727, characters 8-37
22+

hermes/tests/fixtures/edge_cases_charon/test_8_2_unions/hermes.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,4 +5,5 @@ Behavior: Delcares a `pub union U { ... }` and accesses it in an `unsafe` block.
55

66
[test]
77
expected_status = "failure"
8+
stderr_file = "expected.stderr"
89
args = ["verify", "--allow-sorry"]
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
\n

hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,4 +7,5 @@ Behavior: In an `isValid` boundary condition, queries the default instantiation
77
# FIXME(#3089): Update the syntax in `lib.rs` to be valid Lean, and get this
88
# passing.
99
expected_status = "known_bug"
10+
stderr_file = "expected.stderr"
1011
args = ["verify", "--allow-sorry", "--unsound-allow-is-valid"]

0 commit comments

Comments
 (0)