do not trust predicate functions when opting in to verification plus …

…regression tests #1187 (#1307)

prusti-interface/src/specs/mod.rs

@@ -359,14 +359,15 @@ fn get_procedure_spec_ids(def_id: DefId, attrs: &[ast::Attribute]) -> Option<Pro
         read_prusti_attr("pred_spec_id_ref", attrs)
             .map(|raw_spec_id| SpecIdRef::Predicate(parse_spec_id(raw_spec_id, def_id))),
     );
+    let is_predicate = matches!(spec_id_refs.last(), Some(SpecIdRef::Predicate(..)));
     debug!(
         "Function {:?} has specification ids {:?}",
         def_id, spec_id_refs
     );
 
     let pure = has_prusti_attr(attrs, "pure");
     let trusted = has_prusti_attr(attrs, "trusted")
-        || (config::opt_in_verification() && !has_prusti_attr(attrs, "verified"));
+        || (!is_predicate && config::opt_in_verification() && !has_prusti_attr(attrs, "verified"));
     let abstract_predicate = has_abstract_predicate_attr(attrs);
 
     if abstract_predicate || pure || trusted || !spec_id_refs.is_empty() {

prusti-tests/tests/verify_overflow/fail/issues/issue-1187-4.rs

@@ -0,0 +1,18 @@
+// compile-flags: -Popt_in_verification=true -Penable_type_invariants=true
+use prusti_contracts::*;
+
+fn main() {}
+
+#[derive(Copy, Clone)]
+#[invariant(self.bar > 0)]
+pub struct Foo {
+    pub bar: usize,
+}
+
+impl Foo {
+    #[verified]
+    pub const fn new(bar: usize) -> Self {
+        //~^ ERROR type invariants might not hold
+        Self { bar }
+    }
+}

prusti-tests/tests/verify_overflow/pass/issues/issue-1187-5.rs

@@ -0,0 +1,31 @@
+// compile-flags: -Popt_in_verification=true
+use prusti_contracts::*;
+
+fn main() {}
+
+predicate! {
+    fn baz(foo: &Foo) -> bool {
+        foo.bar > 0
+    }
+}
+
+#[derive(Copy, Clone)]
+pub struct Foo {
+    pub bar: usize,
+}
+
+impl Foo {
+    #[verified]
+    #[pure]
+    #[ensures(match result {
+        Some(foo) => baz(&foo),
+        None => true,
+    })]
+    pub const fn new(bar: usize) -> Option<Self> {
+        if bar > 0 {
+            Some(Self { bar })
+        } else {
+            None
+        }
+    }
+}