From a2ca3101d536861c1ff627d77ff011767b255093 Mon Sep 17 00:00:00 2001 From: mimo31 Date: Tue, 18 Jul 2023 17:17:56 +0200 Subject: [PATCH] Temporarily remove The snap command lets you install, configure, refresh 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 [...] 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 '. 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 | 5 +++-- prusti-tests/tests/parse/fail/spec-only_in_non-spec.rs | 3 ++- 2 files changed, 5 insertions(+), 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 index 721d1800b1f..bfa7cf21bac 100644 --- 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 index b91083a57e7..e79fdb7fe15 100644 --- 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