AeneasVerif / charon

Interface with the rustc compiler for the purpose of program verification
Apache License 2.0
79 stars 14 forks source link

Support slice destructuring #320

Closed RaitoBezarius closed 1 month ago

RaitoBezarius commented 1 month ago

Code snippet that is not correctly supported:

let [a, b @ .., c] = x

Current Charon output:

On https://github.com/conradludgate/rustyguard rustyguard-types crate:


error: Unexpected ProjectionElem::Subslice
   --> rustyguard-types/src/lib.rs:189:22
    |
189 |         let [header, payload @ .., tag] = segments else {
    |                      ^^^^^^^

Expected behavior:

Equivalent to a = segments[0]; b = segments[1:n - 1]; c = segments[n - 1];