Comment unused implementation of type invariants

viperproject · Sep 30, 2020 · d7811b8 · d7811b8
1 parent 1e54799
commit d7811b8
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 16 deletions.
diff --git a/prusti-viper/src/encoder/spec_encoder.rs b/prusti-viper/src/encoder/spec_encoder.rs
@@ -46,18 +46,6 @@ pub fn encode_spec_assertion<'p, 'v: 'p, 'tcx: 'v>(
     spec_encoder.encode_assertion(assertion)
 }
 
-pub fn encode_simple_spec_assertion<'p, 'v: 'p, 'tcx: 'v>(
-    encoder: &'p Encoder<'v, 'tcx>,
-    target_args: &'p [vir::Expr],
-    assertion: &typed::Assertion<'tcx>,
-) -> vir::Expr {
-    let spec_encoder = SpecEncoder::new_simple(
-        encoder,
-        target_args,
-    );
-    spec_encoder.encode_assertion(assertion)
-}
-
 struct SpecEncoder<'p, 'v: 'p, 'tcx: 'v> {
     encoder: &'p Encoder<'v, 'tcx>,
     // FIXME: this should be the MIR of the `__spec` function

diff --git a/prusti-viper/src/encoder/type_encoder.rs b/prusti-viper/src/encoder/type_encoder.rs
@@ -558,10 +558,14 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> {
                         match spec {
                             typed::SpecificationSet::Struct(items) => {
                                 for item in items {
-                                    let enc = encode_simple_spec_assertion(
-                                        self.encoder,
-                                        &[],
-                                        &item.assertion
+                                    // let enc = encode_simple_spec_assertion(
+                                    //     self.encoder,
+                                    //     &[],
+                                    //     &item.assertion
+                                    // );
+                                    let enc = unimplemented!(
+                                        "TODO: type invariants need to be upgraded \
+                                        to the new compiler version"
                                     );
                                     // OPEN TODO: hacky fix here to convert the closure var to "self"...
                                     let enc = hacky_folder.fold(enc);