Update tests for predicates in non-spec code

prusti-interface/src/specs/checker/spec_only_items_checks.rs

@@ -77,7 +77,7 @@ impl<'tcx> SpecCheckerStrategy<'tcx> for IllegalSpecOnlyItemsUsageChecker {
                         MultiSpan::from_span(usage_span),
                     )
                     .add_note(
-                        format!("this is a specification-only `{}`", item_kind.name()),
+                        format!("this is a specification-only {}", item_kind.name()),
                         def_span,
                     )
                 }

prusti-tests/tests/parse/fail/spec-only_in_non-spec.rs

@@ -1,5 +1,11 @@
 use prusti_contracts::*;
 
+predicate! {
+    fn pred() -> bool {
+        true
+    }
+}
+
 resource! {
     fn rsrc(amount: usize);
 }
@@ -20,6 +26,8 @@ fn main() {
     snap(&(1 + 1)); //~ ERROR using the built-in `snap` in non-specification code is not allowed
 
     snapshot_equality(1 + 1, 3); //~ ERROR using the built-in `snapshot_equality` in non-specification code is not allowed
+
+    pred(); //~ ERROR using a predicate in non-specification code is not allowed
 
     rsrc(12); //~ ERROR using a resource in non-specification code is not allowed
 

prusti-tests/tests/verify/ui/predicates/abstract-predicate-dont-call.stderr

@@ -1,34 +1,34 @@
-error: [Prusti: invalid specification] using predicate from non-specification code is not allowed
+error: [Prusti: invalid specification] using a predicate in non-specification code is not allowed
   --> $DIR/abstract-predicate-dont-call.rs:25:9
    |
 25 |         self.x.foo();
    |         ^^^^^^^^^^^^
    |
-note: this is a specification-only predicate function
+note: this is a specification-only predicate
   --> $DIR/abstract-predicate-dont-call.rs:6:9
    |
 6  |         fn foo(&self) -> bool;
    |         ^^^^^^^^^^^^^^^^^^^^^^
 
-error: [Prusti: invalid specification] using predicate from non-specification code is not allowed
+error: [Prusti: invalid specification] using a predicate in non-specification code is not allowed
   --> $DIR/abstract-predicate-dont-call.rs:30:5
    |
 30 |     x.foo();
    |     ^^^^^^^
    |
-note: this is a specification-only predicate function
+note: this is a specification-only predicate
   --> $DIR/abstract-predicate-dont-call.rs:6:9
    |
 6  |         fn foo(&self) -> bool;
    |         ^^^^^^^^^^^^^^^^^^^^^^
 
-error: [Prusti: invalid specification] using predicate from non-specification code is not allowed
+error: [Prusti: invalid specification] using a predicate in non-specification code is not allowed
   --> $DIR/abstract-predicate-dont-call.rs:35:13
    |
 35 |     assert!(s.foo());
    |             ^^^^^^^
    |
-note: this is a specification-only predicate function
+note: this is a specification-only predicate
   --> $DIR/abstract-predicate-dont-call.rs:6:9
    |
 6  |         fn foo(&self) -> bool;

prusti-tests/tests/verify/ui/predicates/dont-call.stderr

@@ -1,38 +1,38 @@
-error: [Prusti: invalid specification] using predicate from non-specification code is not allowed
+error: [Prusti: invalid specification] using a predicate in non-specification code is not allowed
   --> $DIR/dont-call.rs:13:14
    |
 13 |     let _x = pred_id(true);
    |              ^^^^^^^
    |
-note: this is a specification-only predicate function
+note: this is a specification-only predicate
   --> $DIR/dont-call.rs:6:5
    |
 6  | /     fn pred_id(x: bool) -> bool {
 7  | |         x
 8  | |     }
    | |_____^
 
-error: [Prusti: invalid specification] using predicate from non-specification code is not allowed
+error: [Prusti: invalid specification] using a predicate in non-specification code is not allowed
   --> $DIR/dont-call.rs:35:29
    |
 35 |                 illegal_ref(Self::inner_pred)
    |                             ^^^^^^^^^^^^^^^^
    |
-note: this is a specification-only predicate function
+note: this is a specification-only predicate
   --> $DIR/dont-call.rs:28:17
    |
 28 | /                 fn inner_pred(b: bool) -> bool {
 29 | |                     b
 30 | |                 }
    | |_________________^
 
-error: [Prusti: invalid specification] using predicate from non-specification code is not allowed
+error: [Prusti: invalid specification] using a predicate in non-specification code is not allowed
   --> $DIR/dont-call.rs:43:17
    |
 43 |     illegal_ref(pred_id);
    |                 ^^^^^^^
    |
-note: this is a specification-only predicate function
+note: this is a specification-only predicate
   --> $DIR/dont-call.rs:6:5
    |
 6  | /     fn pred_id(x: bool) -> bool {

prusti-tests/tests/verify/ui/predicates/trait-impl-dont-call.stderr

@@ -1,48 +1,48 @@
-error: [Prusti: invalid specification] using predicate from non-specification code is not allowed
+error: [Prusti: invalid specification] using a predicate in non-specification code is not allowed
   --> $DIR/trait-impl-dont-call.rs:30:5
    |
 30 |     MyTrait::foo(&s);
    |     ^^^^^^^^^^^^
    |
-note: this is a specification-only predicate function
+note: this is a specification-only predicate
   --> $DIR/trait-impl-dont-call.rs:5:9
    |
 5  |         fn foo(&self) -> bool;
    |         ^^^^^^^^^^^^^^^^^^^^^^
 
-error: [Prusti: invalid specification] using predicate from non-specification code is not allowed
+error: [Prusti: invalid specification] using a predicate in non-specification code is not allowed
   --> $DIR/trait-impl-dont-call.rs:31:5
    |
 31 |     s.foo();
    |     ^^^^^^^
    |
-note: this is a specification-only predicate function
+note: this is a specification-only predicate
   --> $DIR/trait-impl-dont-call.rs:5:9
    |
 5  |         fn foo(&self) -> bool;
    |         ^^^^^^^^^^^^^^^^^^^^^^
 
-error: [Prusti: invalid specification] using predicate from non-specification code is not allowed
+error: [Prusti: invalid specification] using a predicate in non-specification code is not allowed
   --> $DIR/trait-impl-dont-call.rs:32:5
    |
 32 |     MyStruct::bar(&s);
    |     ^^^^^^^^^^^^^
    |
-note: this is a specification-only predicate function
+note: this is a specification-only predicate
   --> $DIR/trait-impl-dont-call.rs:22:9
    |
 22 | /         fn bar(&self) -> bool {
 23 | |             true
 24 | |         }
    | |_________^
 
-error: [Prusti: invalid specification] using predicate from non-specification code is not allowed
+error: [Prusti: invalid specification] using a predicate in non-specification code is not allowed
   --> $DIR/trait-impl-dont-call.rs:33:5
    |
 33 |     s.bar();
    |     ^^^^^^^
    |
-note: this is a specification-only predicate function
+note: this is a specification-only predicate
   --> $DIR/trait-impl-dont-call.rs:22:9
    |
 22 | /         fn bar(&self) -> bool {