prusti-dev icon indicating copy to clipboard operation
prusti-dev copied to clipboard

Support `old(..)` in quantifier triggers

Open Pointerbender opened this issue 3 years ago • 0 comments

Currently Prusti supports Expr::{Local, Const, FuncApp, DomainFuncApp} in quantifier triggers:

https://github.com/viperproject/prusti-dev/blob/0f079017d1fb75f0264b1e652746f16266a25773/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs#L303-L311

Should these also be supported when wrapped in old(..), i.e. Expr::LabelledOld? Down at the Prusti level, there are some cases where this is hard-coded, but currently it is not possible for end-users to write a similar specification:

https://github.com/viperproject/prusti-dev/blob/0f079017d1fb75f0264b1e652746f16266a25773/prusti-viper/src/encoder/procedure_encoder.rs#L5118-L5123

For example, such user specifications maybe be needed when extern_specing <[T]>::copy_within.

Pointerbender avatar Apr 13 '22 12:04 Pointerbender