Temporarily remove snap from spec-only checks

viperproject · Jul 18, 2023 · 7b772d1 · 7b772d1
1 parent e114508
commit 7b772d1
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 3 deletions.
diff --git a/prusti-interface/src/specs/checker/spec_only_items_checks.rs b/prusti-interface/src/specs/checker/spec_only_items_checks.rs
@@ -252,12 +252,13 @@ impl<'v, 'tcx: 'v> NonSpecExprVisitor<'tcx> for CheckSpecOnlyItemsVisitor<'tcx>
 
         // all the builtin specification functions in prusti_contracts
         // Needs to be updated when more are added!
-        static BUILTIN_SPEC_FUNCS: [&str; 6] = [
+        static BUILTIN_SPEC_FUNCS: [&str; 5] = [
             "before_expiry",
             "old",
             "forall",
             "exists",
-            "snap",
+            //"snap", // FIXME: `snap` might have been used in impure code in the past, so it's
+            //temporatily commented out. It should be uncommented here eventually.
             "snapshot_equality",
         ];
 

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
@@ -23,7 +23,8 @@ fn main() {
 
     exists("the", "end"); //~ ERROR using the built-in `exists` in non-specification code is not allowed
 
-    snap(&(1 + 1)); //~ ERROR using the built-in `snap` in non-specification code is not allowed
+    //snap(&(1 + 1)); // ERROR using the built-in `snap` in non-specification code is not allowed
+    // FIXME: this check for `snap` should be uncommented in future
 
     snapshot_equality(1 + 1, 3); //~ ERROR using the built-in `snapshot_equality` in non-specification code is not allowed