Slice and array indexing should be supported in triggers

[vakaras]

trafficstars

Currently, using s[i] in a trigger where s is an array or a slice causes Prusti to crash.

[Pointerbender]

@vakaras In case the refactoring is not a blocker for adding support for triggers on domain functions, and if it's not a super non-trivial fix, maybe I could take a stab at implementing this one? :)

[vakaras]

Thanks! This code is likely to be rewritten during the refactoring, but I think it would be still worth trying to figure out how to actually do it.

[fpoli]

Implemented in #858 by @Pointerbender. Thanks!

@vakaras Do you prefer to keep this issue open because of the following todo, or can I close?

The test prusti-tests/tests/verify/pass/issues/issue-812-4.rs is currently ignored because it triggers a todo!() in the new vir high encoder here: https://github.com/viperproject/prusti-dev/blob/66c90d5dae9040eb68b2f0d2689faa480b10e8d6/prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs#L26-L35

[vakaras]

@vakaras Do you prefer to keep this issue open because of the following todo, or can I close?

The test prusti-tests/tests/verify/pass/issues/issue-812-4.rs is currently ignored because it triggers a todo!() in the new vir high encoder here: https://github.com/viperproject/prusti-dev/blob/66c90d5dae9040eb68b2f0d2689faa480b10e8d6/prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs#L26-L35

Let's keep it open.