Merge #1241

1241: Print a proper compiler warning when no edition is selected r=JonasAlaif a=JonasAlaif Co-authored-by: Jonas <[email protected]>
viperproject · Nov 21, 2022 · e6e40f4 · e6e40f4
2 parents 81f5ba8 + d8ecade
commit e6e40f4
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 17 deletions.
diff --git a/prusti-tests/tests/cargotest.rs b/prusti-tests/tests/cargotest.rs
@@ -68,6 +68,8 @@ fn simple_assert_false() {
         .with_stderr(
             "\
 [CHECKING] foo v0.0.1 ([..])
+[WARNING] Prusti specifications are supported only from 2018 edition. Please specify the edition with adding a command line argument `--edition=2018` or `--edition=2021`.
+
 [ERROR] [Prusti: verification error] the asserted expression might not hold
  --> src/main.rs:1:13
   |
@@ -76,7 +78,8 @@ fn simple_assert_false() {
   |
   = note: this error originates in the macro `assert` (in Nightly builds, run with -Z macro-backtrace for more info)
 
-error: could not compile `foo` due to previous error
+warning: `foo` (bin \"foo\") generated 1 warning
+error: could not compile `foo` due to previous error; 1 warning emitted
 ",
         )
         .run();

diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs
@@ -60,6 +60,16 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls {
         compiler: &Compiler,
         queries: &'tcx Queries<'tcx>,
     ) -> Compilation {
+        if compiler.session().rust_2015() {
+            compiler
+                .session()
+                .struct_warn(
+                    "Prusti specifications are supported only from 2018 edition. Please \
+                 specify the edition with adding a command line argument `--edition=2018` or \
+                 `--edition=2021`.",
+                )
+                .emit();
+        }
         compiler.session().abort_if_errors();
         let (krate, _resolver, _lint_store) = &mut *queries.expansion().unwrap().peek_mut();
         if config::print_desugared_specs() {

diff --git a/prusti/src/driver.rs b/prusti/src/driver.rs
@@ -17,7 +17,7 @@ mod verifier;
 use arg_value::arg_value;
 use callbacks::PrustiCompilerCalls;
 use lazy_static::lazy_static;
-use log::{info, warn};
+use log::info;
 use prusti_common::{config, report::user, Stopwatch};
 use prusti_rustc_interface::interface::interface::try_print_query_stack;
 use std::{borrow::Cow, env, panic};
@@ -147,8 +147,6 @@ fn main() {
     // be called.
     let mut rustc_args = Vec::new();
     let mut is_codegen = false;
-    let mut contains_edition = false;
-    let mut only_print = false;
     for arg in original_rustc_args {
         if arg == "--codegen" || arg == "-C" {
             is_codegen = true;
@@ -160,22 +158,9 @@ fn main() {
                 rustc_args.push("-C".to_owned());
                 is_codegen = false;
             }
-            if arg == "--edition=2018" || arg == "--edition=2021" {
-                contains_edition = true;
-            }
-            if arg.starts_with("--print=") {
-                only_print = true;
-            }
             rustc_args.push(arg);
         }
     }
-    if !contains_edition && !only_print {
-        warn!(
-            "Specifications are supported only from 2018 edition. Please specify \
-               the edition with adding a command line argument `--edition=2018` or \
-               `--edition=2021`."
-        );
-    }
 
     let exit_code = prusti_rustc_interface::driver::catch_with_exit_code(move || {
         user::message(format!(