Temporarily remove The snap command lets you install, configure, refr…

…esh and remove snaps.

Snaps are packages that work across many different Linux distributions,
enabling secure delivery and operation of the latest apps and utilities.

Usage: snap <command> [<options>...]

Commonly used commands can be classified as follows:

           Basics: find, info, install, remove, list
          ...more: refresh, revert, switch, disable, enable, create-cohort
          History: changes, tasks, abort, watch
          Daemons: services, start, stop, restart, logs
      Permissions: connections, interface, connect, disconnect
    Configuration: get, set, unset, wait
      App Aliases: alias, aliases, unalias, prefer
          Account: login, logout, whoami
        Snapshots: saved, save, check-snapshot, restore, forget
           Device: model, reboot, recovery
     Quota Groups: set-quota, remove-quota, quotas, quota
  Validation Sets: validate
        ... Other: warnings, okay, known, ack, version
      Development: validate

For more information about a command, run 'snap help <command>'.
For a short summary of all commands, run 'snap help --all'. from spec-only checks

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",
         ];
 

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