ui tests: Make pretty-llbc the default behavior

AeneasVerif · Apr 12, 2024 · 7e58ea8 · 7e58ea8
1 parent 40fd5df
commit 7e58ea8
Show file tree

Hide file tree

Showing 8 changed files with 3 additions and 15 deletions.
diff --git a/charon/tests/ui.rs b/charon/tests/ui.rs
@@ -25,7 +25,6 @@ enum TestKind {
     KnownFailure,
     KnownPanic,
     Skip,
-    Unspecified,
 }
 
 struct MagicComments {
@@ -40,7 +39,7 @@ struct MagicComments {
 
 static HELP_STRING: &str = unindent!(
     "Options are:
-    - `//@ output=pretty-llbc`: record the pretty-printed llbc;
+    - `//@ output=pretty-llbc`: record the pretty-printed llbc (default);
     - `//@ known-failure`: a test that is expected to fail.
     - `//@ known-panic`: a test that is expected to panic.
     - `//@ skip`: skip the test.
@@ -56,7 +55,7 @@ static HELP_STRING: &str = unindent!(
 fn parse_magic_comments(input_path: &std::path::Path) -> anyhow::Result<MagicComments> {
     // Parse the magic comments.
     let mut comments = MagicComments {
-        test_kind: TestKind::Unspecified,
+        test_kind: TestKind::PrettyLlbc,
         cli_opts: CliOpts::default(),
         check_output: true,
         auxiliary_crates: Vec::new(),
@@ -141,10 +140,6 @@ fn path_to_crate_name(path: &Path) -> Option<String> {
 }
 
 fn perform_test(test_case: &Case, action: Action) -> anyhow::Result<()> {
-    if matches!(test_case.magic_comments.test_kind, TestKind::Unspecified) {
-        bail!("Test must start with a magic comment that determines its kind. {HELP_STRING}");
-    }
-
     // Dependencies
     // Vec of (crate name, path to crate.rs, path to libcrate.rlib).
     let deps: Vec<(String, PathBuf, String)> = test_case
@@ -216,7 +211,7 @@ fn perform_test(test_case: &Case, action: Action) -> anyhow::Result<()> {
                 bail!("Compilation failed: {stderr}")
             }
         }
-        TestKind::Skip | TestKind::Unspecified => unreachable!(),
+        TestKind::Skip => unreachable!(),
     }
     if test_case.magic_comments.check_output {
         let actual = snapbox::Data::text(stderr).map_text(snapbox::utils::normalize_lines);

diff --git a/charon/tests/ui/issue-118-generic-copy.rs b/charon/tests/ui/issue-118-generic-copy.rs
@@ -1,4 +1,3 @@
-//@ output=pretty-llbc
 #![allow(unused)]
 
 #[derive(Clone, Copy)]

diff --git a/charon/tests/ui/issue-4-traits.rs b/charon/tests/ui/issue-4-traits.rs
@@ -1,4 +1,3 @@
-//@ output=pretty-llbc
 use std::convert::TryInto;
 fn trait_error(s: &[u8]) {
     let _array: [u8; 4] = s.try_into().unwrap();

diff --git a/charon/tests/ui/issue-45-misc.rs b/charon/tests/ui/issue-45-misc.rs
@@ -1,4 +1,3 @@
-//@ output=pretty-llbc
 pub fn map(x: [i32; 256]) -> [i32; 256] {
     x.map(|v| v)
 }

diff --git a/charon/tests/ui/issue-72-hash-missing-impl.rs b/charon/tests/ui/issue-72-hash-missing-impl.rs
@@ -1,4 +1,3 @@
-//@ output=pretty-llbc
 pub trait Hasher {}
 
 pub struct DefaultHasher;

diff --git a/charon/tests/ui/issue-73-extern.rs b/charon/tests/ui/issue-73-extern.rs
@@ -1,4 +1,3 @@
-//@ output=pretty-llbc
 #![feature(extern_types)]
 extern "C" {
     fn foo(x: i32);

diff --git a/charon/tests/ui/issue-92-nonpositive-variant-indices.rs b/charon/tests/ui/issue-92-nonpositive-variant-indices.rs
@@ -1,4 +1,3 @@
-//@ output=pretty-llbc
 enum Ordering {
     Less = -1,
     Equal = 0,

diff --git a/charon/tests/ui/issue-97-missing-parent-item-clause.rs b/charon/tests/ui/issue-97-missing-parent-item-clause.rs
@@ -1,4 +1,3 @@
-//@ output=pretty-llbc
 pub trait Ord {}
 
 pub struct AVLTree<T> {