Disable recursive function call checking because it crashes.

viperproject · Jul 19, 2023 · c2990d5 · c2990d5
1 parent 0aeb4a3
commit c2990d5
Showing 1 changed file with 6 additions and 3 deletions.
diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs
@@ -145,13 +145,16 @@ impl<'tcx> Environment<'tcx> {
             true
         } else {
             let param_env = self.tcx().param_env(caller_def_id);
-            if let Some(instance) = self
+            if let Some(_instance) = self
                 .tcx()
                 .resolve_instance(param_env.and((called_def_id, call_substs)))
                 .unwrap()
             {
-                self.tcx()
-                    .mir_callgraph_reachable((instance, caller_def_id.expect_local()))
+                // FIXME: This call panics due to stolen MIR. Therefore, we
+                // unsoundly assume that the callee is not reachable.
+                // self.tcx()
+                //     .mir_callgraph_reachable((instance, caller_def_id.expect_local()))
+                false
             } else {
                 true
             }