extern crate prusti_contracts;
use prusti_contracts::*;
fn main() {
let xs: [u8; 10] = Default::default();
let mut v: std::vec::Vec<&u8> = std::vec::Vec::new();
let mut i = 0;
while i < 10 {
v.push(&xs[i]); // error
i += 1;
}
}
mir dump showing bb6
```
// WARNING: This output format is intended for human consumers only
// and is subject to change without notice. Knock yourself out.
fn main() -> () {
let mut _0: ();
let _1: [u8; 10];
let mut _4: bool;
let mut _5: usize;
let _6: ();
let mut _7: &mut std::vec::Vec<&u8>;
let _8: &u8;
let _9: usize;
let mut _10: usize;
let mut _11: bool;
let mut _12: (usize, bool);
scope 1 {
debug xs => _1;
let mut _2: std::vec::Vec<&u8>;
scope 2 {
debug v => _2;
let mut _3: usize;
scope 3 {
debug i => _3;
}
}
}
bb0: {
_1 = <[u8; 10] as Default>::default() -> [return: bb1, unwind continue];
}
bb1: {
_2 = Vec::<&u8>::new() -> [return: bb2, unwind continue];
}
bb2: {
_3 = const 0_usize;
goto -> bb3;
}
bb3: {
_5 = _3;
_4 = Lt(move _5, const 10_usize);
switchInt(move _4) -> [0: bb8, otherwise: bb4];
}
bb4: {
_7 = &mut _2;
_9 = _3;
_10 = const 10_usize;
_11 = Lt(_9, _10);
assert(move _11, "index out of bounds: the length is {} but the index is {}", move _10, _9) -> [success: bb5, unwind: bb10];
}
bb5: {
_8 = &_1[_9];
_6 = Vec::<&u8>::push(move _7, _8) -> [return: bb6, unwind: bb10];
}
bb6: {
_12 = CheckedAdd(_3, const 1_usize);
assert(!move (_12.1: bool), "attempt to compute `{} + {}`, which would overflow", _3, const 1_usize) -> [success: bb7, unwind: bb10];
}
bb7: {
_3 = move (_12.0: usize);
goto -> bb3;
}
bb8: {
drop(_2) -> [return: bb9, unwind continue];
}
bb9: {
return;
}
bb10 (cleanup): {
drop(_2) -> [return: bb11, unwind terminate(cleanup)];
}
bb11 (cleanup): {
resume;
}
}
main::{constant#0}: usize = {
let mut _0: usize;
bb0: {
_0 = const 10_usize;
return;
}
}
```
Prusti version: 0.2.2, commit 0d4a8d4 2024-03-26 13:08:03 UTC, built on 2024-03-26 13:20:57 UTC
mir dump showing bb6
``` // WARNING: This output format is intended for human consumers only // and is subject to change without notice. Knock yourself out. fn main() -> () { let mut _0: (); let _1: [u8; 10]; let mut _4: bool; let mut _5: usize; let _6: (); let mut _7: &mut std::vec::Vec<&u8>; let _8: &u8; let _9: usize; let mut _10: usize; let mut _11: bool; let mut _12: (usize, bool); scope 1 { debug xs => _1; let mut _2: std::vec::Vec<&u8>; scope 2 { debug v => _2; let mut _3: usize; scope 3 { debug i => _3; } } } bb0: { _1 = <[u8; 10] as Default>::default() -> [return: bb1, unwind continue]; } bb1: { _2 = Vec::<&u8>::new() -> [return: bb2, unwind continue]; } bb2: { _3 = const 0_usize; goto -> bb3; } bb3: { _5 = _3; _4 = Lt(move _5, const 10_usize); switchInt(move _4) -> [0: bb8, otherwise: bb4]; } bb4: { _7 = &mut _2; _9 = _3; _10 = const 10_usize; _11 = Lt(_9, _10); assert(move _11, "index out of bounds: the length is {} but the index is {}", move _10, _9) -> [success: bb5, unwind: bb10]; } bb5: { _8 = &_1[_9]; _6 = Vec::<&u8>::push(move _7, _8) -> [return: bb6, unwind: bb10]; } bb6: { _12 = CheckedAdd(_3, const 1_usize); assert(!move (_12.1: bool), "attempt to compute `{} + {}`, which would overflow", _3, const 1_usize) -> [success: bb7, unwind: bb10]; } bb7: { _3 = move (_12.0: usize); goto -> bb3; } bb8: { drop(_2) -> [return: bb9, unwind continue]; } bb9: { return; } bb10 (cleanup): { drop(_2) -> [return: bb11, unwind terminate(cleanup)]; } bb11 (cleanup): { resume; } } main::{constant#0}: usize = { let mut _0: usize; bb0: { _0 = const 10_usize; return; } } ```Prusti version: 0.2.2, commit 0d4a8d4 2024-03-26 13:08:03 UTC, built on 2024-03-26 13:20:57 UTC