`snap` function can be used in normal code

[Patrick-6]

Using the snap function in normal code does not always cause a compiler error like in the first function. The second function causes Prusti to crash:

use prusti_contracts::*;

// This function does not cause a verification failure:
fn _test_should_fail(v: &u64) -> u64 {
    let s = snap(v); 
    let x = s + 1;
    x
}

// This function causes an internal error:
fn _test_internal_error(v: &u64) {
    let s = snap(v);
    prusti_assert!(&s === v);
}

thread 'rustc' panicked at 'internal error: entered unreachable code', prusti-viper\src\encoder\foldunfold\requirements.rs:449:38

The panicking code is here

[Aurel300]

Prusti should also forbid using other spec-only constructs in regular code. For example, old or time_credits (#1275). A similar check is already implemented for user-defined predicate! functions, it needs to be extended to the built-in functions.

[Patrick-6]

There should also be an error when attempting to use old inside a predicate:

use prusti_contracts::*;

predicate! {
    fn is_plus_one(value: &u64) -> bool {
        snap(value) == old(snap(value)) + 1
    }
}

#[ensures(is_plus_one(value))] // FAILS
// #[ensures(snap(value) == old(snap(value)) + 1)] // WORKS
fn add_one(value: &mut u64) {
    *value += 1;
}

Currently, this just causes an internal error:

[Prusti internal error] Prusti encountered an unexpected internal error
lib.rs(1, 1): We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
lib.rs(1, 1): Details: consistency error in test_crate::add_one: Consistency error: No matching identifier pre found of type Label. (@6.24)