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