Fix parsing error in desugared specifications

Type asccription has been removed by RFC 803: rust-lang/rfcs#3307
viperproject · Jun 30, 2023 · 852891b · 852891b
1 parent fe877bd
commit 852891b
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 18 deletions.
diff --git a/prusti-contracts/prusti-contracts/tests/pass/true.rs b/prusti-contracts/prusti-contracts/tests/pass/true.rs
@@ -3,7 +3,6 @@
 
 // These feature flags are not needed when executing under Prusti
 // because it generates them for us.
-#![cfg_attr(feature = "prusti", feature(type_ascription))]
 #![cfg_attr(feature = "prusti", feature(register_tool))]
 #![cfg_attr(feature = "prusti", register_tool(prusti))]
 

diff --git a/prusti-contracts/prusti-specs/src/rewriter.rs b/prusti-contracts/prusti-specs/src/rewriter.rs
@@ -105,30 +105,21 @@ impl AstRewriter {
         // - `item_span` is set to `expr.span()` so that any errors reported
         //   for the spec item will be reported on the span of the expression
         //   written by the user
-        // - `((#expr) : bool)` syntax is used to report type errors in the
+        // - `let ...: bool = #expr` syntax is used to report type errors in the
         //   expression with the correct error message, i.e. that the expected
         //   type is `bool`, not that the expected *return* type is `bool`
-        // - `!!(...)` is used to fix an edge-case when the expression consists
-        //   of a single identifier; without the double negation, the `Return`
-        //   terminator in MIR has a span set to the one character just after
-        //   the identifier
-        let (return_type, return_modifier) = match &spec_type {
-            SpecItemType::Termination => (
-                quote_spanned! {item_span => Int},
-                quote_spanned! {item_span => Int::new(0) + },
-            ),
-            SpecItemType::Predicate(return_type) => (return_type.clone(), TokenStream::new()),
-            _ => (
-                quote_spanned! {item_span => bool},
-                quote_spanned! {item_span => !!},
-            ),
+        let return_type = match &spec_type {
+            SpecItemType::Termination => quote_spanned! {item_span => Int},
+            SpecItemType::Predicate(return_type) => return_type.clone(),
+            _ => quote_spanned! {item_span => bool},
         };
         let mut spec_item: syn::ItemFn = parse_quote_spanned! {item_span=>
             #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)]
             #[prusti::spec_only]
             #[prusti::spec_id = #spec_id_str]
             fn #item_name() -> #return_type {
-                #return_modifier ((#expr) : #return_type)
+                let prusti_result: #return_type = #expr;
+                prusti_result
             }
         };
 

diff --git a/prusti/src/driver.rs b/prusti/src/driver.rs
@@ -209,7 +209,6 @@ fn main() {
         }
 
         rustc_args.push("-Zalways-encode-mir".to_owned());
-        rustc_args.push("-Zcrate-attr=feature(type_ascription)".to_owned());
         rustc_args.push("-Zcrate-attr=feature(stmt_expr_attributes)".to_owned());
         rustc_args.push("-Zcrate-attr=feature(register_tool)".to_owned());
         rustc_args.push("-Zcrate-attr=register_tool(prusti)".to_owned());