diff --git a/prusti-interface/src/specs/checker/spec_only_items_checks.rs b/prusti-interface/src/specs/checker/spec_only_items_checks.rs index 37d2d99c879..721d1800b1f 100644 --- a/prusti-interface/src/specs/checker/spec_only_items_checks.rs +++ b/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, ) } diff --git a/prusti-tests/tests/parse/fail/spec-only_in_non-spec.rs b/prusti-tests/tests/parse/fail/spec-only_in_non-spec.rs index 5141d4ea6d9..b91083a57e7 100644 --- a/prusti-tests/tests/parse/fail/spec-only_in_non-spec.rs +++ b/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 diff --git a/prusti-tests/tests/verify/ui/predicates/abstract-predicate-dont-call.stderr b/prusti-tests/tests/verify/ui/predicates/abstract-predicate-dont-call.stderr index b182a2d27c6..ea715af5dcb 100644 --- a/prusti-tests/tests/verify/ui/predicates/abstract-predicate-dont-call.stderr +++ b/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; diff --git a/prusti-tests/tests/verify/ui/predicates/dont-call.stderr b/prusti-tests/tests/verify/ui/predicates/dont-call.stderr index 97fe5c402e2..5fa65007311 100644 --- a/prusti-tests/tests/verify/ui/predicates/dont-call.stderr +++ b/prusti-tests/tests/verify/ui/predicates/dont-call.stderr @@ -1,10 +1,10 @@ -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 { @@ -12,13 +12,13 @@ note: this is a specification-only predicate function 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 { @@ -26,13 +26,13 @@ note: this is a specification-only predicate function 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 { diff --git a/prusti-tests/tests/verify/ui/predicates/trait-impl-dont-call.stderr b/prusti-tests/tests/verify/ui/predicates/trait-impl-dont-call.stderr index 7a680f9f97d..dd0230b21f9 100644 --- a/prusti-tests/tests/verify/ui/predicates/trait-impl-dont-call.stderr +++ b/prusti-tests/tests/verify/ui/predicates/trait-impl-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/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 { @@ -36,13 +36,13 @@ note: this is a specification-only predicate function 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 {