"Creusot contracts not loaded" error message (#1404)

creusot-rs · Mar 3, 2025 · d1fa591 · d1fa591
2 parents 8b949c1 + 0de5ebb
commit d1fa591
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 14 deletions.
diff --git a/creusot/src/contracts_items/diagnostic_items.rs b/creusot/src/contracts_items/diagnostic_items.rs
@@ -14,9 +14,12 @@ pub(crate) enum AreContractsLoaded {
 
 macro_rules! contracts_items {
     (
-        $(
-            $kind:tt $name:path [ $symbol:literal ] $is_name:ident $get_name:ident
-        )*
+        $(#[$std_items:meta])?
+        {
+            $(
+                $kind:tt $name:path [ $symbol:literal ] $is_name:ident $get_name:ident
+            )*
+        }
     ) => {
         $(
             #[doc = concat!("Check if `def_id` is the `", stringify!($name), "` ", contracts_items!(@kind $kind))]
@@ -32,6 +35,16 @@ macro_rules! contracts_items {
             }
         )*
 
+        contracts_items! {
+            @are_contracts_loaded
+            $(#[$std_items])?
+            $($symbol)*
+        }
+    };
+    (@kind fn) => { "function" };
+    (@kind type) => { "type" };
+    (@are_contracts_loaded #[$std_items:meta] $($symbol:literal)*) => {};
+    (@are_contracts_loaded $($symbol:literal)*) => {
         /// Call this at the earlist point possible: if `creusot-contracts` is not loaded, we
         /// need to immediatly crash.
         pub(crate) fn are_contracts_loaded(tcx: TyCtxt) -> AreContractsLoaded {
@@ -53,11 +66,9 @@ macro_rules! contracts_items {
             }
         }
     };
-    (@kind fn) => { "function" };
-    (@kind type) => { "type" };
 }
 
-contracts_items! {
+contracts_items! {{
     fn inv                               ["creusot_invariant_internal"]
         is_inv_function                 get_inv_function
     fn resolve                           ["creusot_resolve"]
@@ -84,12 +95,6 @@ contracts_items! {
         is_ghost_deref_mut              get_ghost_deref_mut
     fn IndexLogic::index_logic           ["creusot_index_logic_method"]
         is_index_logic                  get_index_logic
-    fn Deref::deref                      ["deref_method"]
-        is_deref                        get_deref
-    fn Deref::deref_mut                  ["deref_mut_method"]
-        is_deref_mut                    get_deref_mut
-    fn Box::new                          ["box_new"]
-        is_box_new                      get_box_new
     fn FnOnceExt::precondition           ["fn_once_impl_precond"]
         is_fn_once_impl_precond         get_fn_once_impl_precond
     fn FnOnceExt::postcondition_once     ["fn_once_impl_postcond"]
@@ -106,4 +111,13 @@ contracts_items! {
         is_snap_ty                      get_snap_ty
     type GhostBox                        ["ghost_box"]
         is_ghost_ty                     get_ghost_ty
-}
+}}
+
+contracts_items! { #[std_items] {
+    fn Deref::deref                      ["deref_method"]
+        is_deref                        get_deref
+    fn Deref::deref_mut                  ["deref_mut_method"]
+        is_deref_mut                    get_deref_mut
+    fn Box::new                          ["box_new"]
+        is_box_new                      get_box_new
+}}
diff --git a/creusot/src/translation.rs b/creusot/src/translation.rs
@@ -38,7 +38,7 @@ pub(crate) fn before_analysis(ctx: &mut TranslationCtx) -> Result<(), Box<dyn st
 
     match are_contracts_loaded(ctx.tcx) {
         AreContractsLoaded::Yes => {},
-        AreContractsLoaded::No => ctx.fatal_error(DUMMY_SP, "The `creusot_contracts` crate is not loaded. You will not be able to verify any code using Creusot until you do so.").emit(),
+        AreContractsLoaded::No => ctx.fatal_error(DUMMY_SP, "The `creusot_contracts` crate is not loaded. You will not be able to verify any code using Creusot until you do so.").with_note("Don't forget to actually use creusot_contracts: `use creusot_contracts::*;`").emit(),
         AreContractsLoaded::MissingItems(missing) => {
             let mut message = String::from("The `creusot_contracts` crate is loaded, but the following items are missing: ");
             for (i, item) in missing.iter().enumerate() {