prusti-dev
prusti-dev copied to clipboard
Published
20 hours ago •
viperproject
viperproject
[Prusti internal error] generating fold-unfold Viper statements failed
I'm trying to create a struct in which one member is a linked list, and in the push() method I call the push() method of the List type, which has already been verified. I get the error:
[{
"resource": "/home/ramla/static_array_rb_tree/src/lib.rs",
"owner": "prusti",
"severity": 8,
"message": "[Prusti internal error] generating fold-unfold Viper statements failed (FailedToObtain(Pred(Local(Local { variable: _6: Ref(struct$m_TrustedRangeInclusive), position: Position { line: 0, column: 0, id: 0 } }), read)))",
"startLineNumber": 38,
"startColumn": 2,
"endLineNumber": 42,
"endColumn": 3
}]
I've mostly used the implementation provided in the user guide and the elements of the list are of type RangeInclusive.
pub struct StaticArrayLinkedList {
ll: List,
heap_initialized: bool
}
impl StaticArrayLinkedList {
pub fn push(&mut self, value: TrustedRangeInclusive) {
if self.heap_initialized {
self.ll.push(value);
}
}
}
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct TrustedRangeInclusive {
pub(crate) start: usize,
pub(crate) end: usize
}
impl TrustedRangeInclusive {
#[requires(start <= end)]
#[ensures(result.start == start)]
#[ensures(result.end == end)]
pub const fn new(start: usize, end: usize) -> Self {
Self{start, end}
}
#[pure]
pub fn overlap(&self, range2: &Self) -> bool {
(self.end > range2.start) || (range2.end > self.start)
}
pub fn to_range_inclusive(self) -> RangeInclusive<usize> {
RangeInclusive::new(self.start, self.end)
}
}
Prusti Assistant Output:
Run verification on /home/ramla/static_array_rb_tree/src/lib.rs...
Preparing verification run #195.
Killing 0 processes.
Run command '/home/ramla/.config/Code/User/globalStorage/viper-admin.prusti-assistant/prustiTools/LatestRelease/prusti/cargo-prusti --message-format=json'
Spawned PID: 3788
Output from '/home/ramla/.config/Code/User/globalStorage/viper-admin.prusti-assistant/prustiTools/LatestRelease/prusti/cargo-prusti --message-format=json' (20.8s):
┌──── Begin stdout ────┐
{"reason":"compiler-message","package_id":"static_array_rb_tree 0.1.0 (path+file:///home/ramla/static_array_rb_tree)","manifest_path":"/home/ramla/static_array_rb_tree/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"static_array_rb_tree","src_path":"/home/ramla/static_array_rb_tree/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"message":{"rendered":"warning: comparison is useless due to type limits\n --> src/static_array.rs:26:28\n |\n26 | forall(|i: usize| (0 <= i && i < 32) ==> old(self.arr[i]) == self.arr[i])\n | ^^^^^^\n |\n = note: `#[warn(unused_comparisons)]` on by default\n\n","children":[{"children":[],"code":null,"level":"note","message":"`#[warn(unused_comparisons)]` on by default","rendered":null,"spans":[]}],"code":{"code":"unused_comparisons","explanation":null},"level":"warning","message":"comparison is useless due to type limits","spans":[{"byte_end":537,"byte_start":531,"column_end":34,"column_start":28,"expansion":null,"file_name":"src/static_array.rs","is_primary":true,"label":null,"line_end":26,"line_start":26,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":34,"highlight_start":28,"text":" forall(|i: usize| (0 <= i && i < 32) ==> old(self.arr[i]) == self.arr[i])"}]}]}}
{"reason":"compiler-message","package_id":"static_array_rb_tree 0.1.0 (path+file:///home/ramla/static_array_rb_tree)","manifest_path":"/home/ramla/static_array_rb_tree/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"static_array_rb_tree","src_path":"/home/ramla/static_array_rb_tree/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"message":{"rendered":"warning: comparison is useless due to type limits\n --> src/static_array.rs:33:29\n |\n33 | forall(|i: usize| ((0 <= i && i < 32) && (i != peek_usize_range(&result))) ==> old(self.arr[i]) == self.arr[i])\n | ^^^^^^\n\n","children":[],"code":{"code":"unused_comparisons","explanation":null},"level":"warning","message":"comparison is useless due to type limits","spans":[{"byte_end":786,"byte_start":780,"column_end":35,"column_start":29,"expansion":null,"file_name":"src/static_array.rs","is_primary":true,"label":null,"line_end":33,"line_start":33,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":35,"highlight_start":29,"text":" forall(|i: usize| ((0 <= i && i < 32) && (i != peek_usize_range(&result))) ==> old(self.arr[i]) == self.arr[i])"}]}]}}
{"reason":"compiler-message","package_id":"static_array_rb_tree 0.1.0 (path+file:///home/ramla/static_array_rb_tree)","manifest_path":"/home/ramla/static_array_rb_tree/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"static_array_rb_tree","src_path":"/home/ramla/static_array_rb_tree/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"message":{"rendered":"warning: comparison is useless due to type limits\n --> src/linked_list.rs:29:30\n |\n29 | #[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> \n | ^^^^^^\n\n","children":[],"code":{"code":"unused_comparisons","explanation":null},"level":"warning","message":"comparison is useless due to type limits","spans":[{"byte_end":417,"byte_start":411,"column_end":36,"column_start":30,"expansion":null,"file_name":"src/linked_list.rs","is_primary":true,"label":null,"line_end":29,"line_start":29,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":36,"highlight_start":30,"text":"#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> "}]}]}}
{"reason":"compiler-message","package_id":"static_array_rb_tree 0.1.0 (path+file:///home/ramla/static_array_rb_tree)","manifest_path":"/home/ramla/static_array_rb_tree/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"static_array_rb_tree","src_path":"/home/ramla/static_array_rb_tree/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"message":{"rendered":"warning: comparison is useless due to type limits\n --> src/linked_list.rs:44:16\n |\n44 | #[requires(0 <= index && index < self.len())]\n | ^^^^^^^^^^\n\n","children":[],"code":{"code":"unused_comparisons","explanation":null},"level":"warning","message":"comparison is useless due to type limits","spans":[{"byte_end":711,"byte_start":701,"column_end":26,"column_start":16,"expansion":null,"file_name":"src/linked_list.rs","is_primary":true,"label":null,"line_end":44,"line_start":44,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":26,"highlight_start":16,"text":" #[requires(0 <= index && index < self.len())]"}]}]}}
{"reason":"compiler-message","package_id":"static_array_rb_tree 0.1.0 (path+file:///home/ramla/static_array_rb_tree)","manifest_path":"/home/ramla/static_array_rb_tree/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"static_array_rb_tree","src_path":"/home/ramla/static_array_rb_tree/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"message":{"rendered":"warning: comparison is useless due to type limits\n --> src/linked_list.rs:76:24\n |\n76 | forall(|i: usize| (0 <= i && i < self.len()) ==>\n | ^^^^^^\n\n","children":[],"code":{"code":"unused_comparisons","explanation":null},"level":"warning","message":"comparison is useless due to type limits","spans":[{"byte_end":1845,"byte_start":1839,"column_end":30,"column_start":24,"expansion":null,"file_name":"src/linked_list.rs","is_primary":true,"label":null,"line_end":76,"line_start":76,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":30,"highlight_start":24,"text":" forall(|i: usize| (0 <= i && i < self.len()) ==>"}]}]}}
{"reason":"compiler-message","package_id":"static_array_rb_tree 0.1.0 (path+file:///home/ramla/static_array_rb_tree)","manifest_path":"/home/ramla/static_array_rb_tree/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"static_array_rb_tree","src_path":"/home/ramla/static_array_rb_tree/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"message":{"rendered":"warning: comparison is useless due to type limits\n --> src/linked_list.rs:121:16\n |\n121 | #[requires(0 <= index && index <= self.len())]\n | ^^^^^^^^^^\n\n","children":[],"code":{"code":"unused_comparisons","explanation":null},"level":"warning","message":"comparison is useless due to type limits","spans":[{"byte_end":3124,"byte_start":3114,"column_end":26,"column_start":16,"expansion":null,"file_name":"src/linked_list.rs","is_primary":true,"label":null,"line_end":121,"line_start":121,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":26,"highlight_start":16,"text":" #[requires(0 <= index && index <= self.len())]"}]}]}}
{"reason":"compiler-message","package_id":"static_array_rb_tree 0.1.0 (path+file:///home/ramla/static_array_rb_tree)","manifest_path":"/home/ramla/static_array_rb_tree/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"static_array_rb_tree","src_path":"/home/ramla/static_array_rb_tree/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"message":{"rendered":"warning: comparison is useless due to type limits\n --> src/linked_list.rs:169:16\n |\n169 | #[requires(0 <= index && index < self.len())]\n | ^^^^^^^^^^\n\n","children":[],"code":{"code":"unused_comparisons","explanation":null},"level":"warning","message":"comparison is useless due to type limits","spans":[{"byte_end":4473,"byte_start":4463,"column_end":26,"column_start":16,"expansion":null,"file_name":"src/linked_list.rs","is_primary":true,"label":null,"line_end":169,"line_start":169,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":26,"highlight_start":16,"text":" #[requires(0 <= index && index < self.len())]"}]}]}}
{"reason":"compiler-message","package_id":"static_array_rb_tree 0.1.0 (path+file:///home/ramla/static_array_rb_tree)","manifest_path":"/home/ramla/static_array_rb_tree/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"static_array_rb_tree","src_path":"/home/ramla/static_array_rb_tree/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"message":{"rendered":"error: [Prusti internal error] generating fold-unfold Viper statements failed (FailedToObtain(Pred(Local(Local { variable: _6: Ref(struct$m_TrustedRangeInclusive), position: Position { line: 0, column: 0, id: 0 } }), read)))\n --> src/lib.rs:38:2\n |\n38 | / pub fn push(&mut self, value: TrustedRangeInclusive) {\n39 | | if self.heap_initialized {\n40 | | self.ll.push(value);\n41 | | }\n42 | | }\n | |_____^\n\n","children":[],"code":null,"level":"error","message":"[Prusti internal error] generating fold-unfold Viper statements failed (FailedToObtain(Pred(Local(Local { variable: _6: Ref(struct$m_TrustedRangeInclusive), position: Position { line: 0, column: 0, id: 0 } }), read)))","spans":[{"byte_end":1126,"byte_start":1012,"column_end":3,"column_start":2,"expansion":null,"file_name":"src/lib.rs","is_primary":true,"label":null,"line_end":42,"line_start":38,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":56,"highlight_start":2,"text":"\tpub fn push(&mut self, value: TrustedRangeInclusive) {"},{"highlight_end":29,"highlight_start":1,"text":"\t\tif self.heap_initialized {"},{"highlight_end":24,"highlight_start":1,"text":"\t\t\tself.ll.push(value);"},{"highlight_end":4,"highlight_start":1,"text":"\t\t}"},{"highlight_end":3,"highlight_start":1,"text":"\t}"}]}]}}
{"reason":"compiler-message","package_id":"static_array_rb_tree 0.1.0 (path+file:///home/ramla/static_array_rb_tree)","manifest_path":"/home/ramla/static_array_rb_tree/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"static_array_rb_tree","src_path":"/home/ramla/static_array_rb_tree/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"message":{"rendered":"error: aborting due to previous error; 7 warnings emitted\n\n","children":[],"code":null,"level":"error","message":"aborting due to previous error; 7 warnings emitted","spans":[]}}
{"reason":"build-finished","success":false}
└──── End stdout ──────┘
┌──── Begin stderr ────┐
Checking static_array_rb_tree v0.1.0 (/home/ramla/static_array_rb_tree)
[2022-08-02T20:38:59Z INFO prusti_driver] Prusti version: commit 4dfd34d 2021-11-22 16:35:31 UTC, built on 2021-11-22 16:40:49 UTC
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Received 29 functions to be verified:
[2022-08-02T20:39:00Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Starting: encoding to Viper
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - static_array::StaticArray::new (static_array_rb_tree::static_array::{impl#0}::new)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/static_array.rs:16:5: 16:31 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - trusted_range_inclusive::TrustedRangeInclusive::to_range_inclusive (static_array_rb_tree::trusted_range_inclusive::{impl#0}::to_range_inclusive)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/trusted_range_inclusive.rs:23:5: 23:61 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - StaticArrayLinkedList::push (static_array_rb_tree::{impl#0}::push)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/lib.rs:38:2: 38:54 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - static_array::StaticArray::push (static_array_rb_tree::static_array::{impl#0}::push)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/static_array.rs:35:2: 35:94 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - linked_list::replace (static_array_rb_tree::linked_list::replace)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/linked_list.rs:31:1: 31:47 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - linked_list::List::len (static_array_rb_tree::linked_list::{impl#0}::len)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/linked_list.rs:39:5: 39:31 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - linked_list::List::lookup (static_array_rb_tree::linked_list::{impl#0}::lookup)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/linked_list.rs:45:5: 45:64 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - linked_list::List::new (static_array_rb_tree::linked_list::{impl#0}::new)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/linked_list.rs:50:5: 50:25 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - linked_list::List::push (static_array_rb_tree::linked_list::{impl#0}::push)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/linked_list.rs:61:5: 61:56 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - linked_list::List::pop (static_array_rb_tree::linked_list::{impl#0}::pop)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/linked_list.rs:78:5: 78:59 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - linked_list::List::overlap (static_array_rb_tree::linked_list::{impl#0}::overlap)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/linked_list.rs:91:5: 91:65 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - linked_list::List::overlap_idx (static_array_rb_tree::linked_list::{impl#0}::overlap_idx)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/linked_list.rs:106:5: 106:96 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - linked_list::List::range_overlaps_in_list (static_array_rb_tree::linked_list::{impl#0}::range_overlaps_in_list)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/linked_list.rs:135:5: 135:97 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - linked_list::Link::len (static_array_rb_tree::linked_list::{impl#1}::len)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/linked_list.rs:153:5: 153:27 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - linked_list::Link::is_empty (static_array_rb_tree::linked_list::{impl#1}::is_empty)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/linked_list.rs:161:5: 161:31 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - linked_list::Link::lookup (static_array_rb_tree::linked_list::{impl#1}::lookup)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/linked_list.rs:170:5: 170:64 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - <trusted_range_inclusive::TrustedRangeInclusive as std::clone::Clone>::clone (static_array_rb_tree::trusted_range_inclusive::{impl#1}::clone)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/trusted_range_inclusive.rs:4:10: 4:15 (#47)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - <trusted_range_inclusive::TrustedRangeInclusive as std::cmp::PartialEq>::eq (static_array_rb_tree::trusted_range_inclusive::{impl#4}::eq)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/trusted_range_inclusive.rs:4:23: 4:32 (#49)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - <trusted_range_inclusive::TrustedRangeInclusive as std::cmp::PartialEq>::ne (static_array_rb_tree::trusted_range_inclusive::{impl#4}::ne)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/trusted_range_inclusive.rs:4:23: 4:32 (#49)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - <trusted_range_inclusive::TrustedRangeInclusive as std::cmp::Eq>::assert_receiver_is_total_eq (static_array_rb_tree::trusted_range_inclusive::{impl#6}::assert_receiver_is_total_eq)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/trusted_range_inclusive.rs:4:34: 4:36 (#50)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - trusted_range_inclusive::TrustedRangeInclusive::new (static_array_rb_tree::trusted_range_inclusive::{impl#0}::new)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/trusted_range_inclusive.rs:14:5: 14:55 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - trusted_range_inclusive::TrustedRangeInclusive::overlap (static_array_rb_tree::trusted_range_inclusive::{impl#0}::overlap)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/trusted_range_inclusive.rs:19:5: 19:49 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - trusted_option::peek_range (static_array_rb_tree::trusted_option::peek_range)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/trusted_option.rs:20:1: 20:87 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - trusted_option::peek_usize (static_array_rb_tree::trusted_option::peek_usize)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/trusted_option.rs:29:1: 29:55 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - <trusted_option::OptionRange as std::clone::Clone>::clone (static_array_rb_tree::trusted_option::{impl#3}::clone)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/trusted_option.rs:36:16: 36:21 (#97)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - trusted_option::OptionRange::is_none (static_array_rb_tree::trusted_option::{impl#0}::is_none)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/trusted_option.rs:44:5: 44:34 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - trusted_option::OptionRange::is_some (static_array_rb_tree::trusted_option::{impl#0}::is_some)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/trusted_option.rs:52:5: 52:34 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - trusted_option::OptionRange::peek (static_array_rb_tree::trusted_option::{impl#0}::peek)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/trusted_option.rs:58:5: 58:48 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] - trusted_result::peek_usize_range (static_array_rb_tree::trusted_result::peek_usize_range)
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Source: src/trusted_result.rs:20:1: 20:84 (#0)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: static_array::StaticArray::new (static_array_rb_tree::static_array::{impl#0}::new)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: trusted_range_inclusive::TrustedRangeInclusive::to_range_inclusive (static_array_rb_tree::trusted_range_inclusive::{impl#0}::to_range_inclusive)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: StaticArrayLinkedList::push (static_array_rb_tree::{impl#0}::push)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: static_array::StaticArray::push (static_array_rb_tree::static_array::{impl#0}::push)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: linked_list::replace (static_array_rb_tree::linked_list::replace)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: linked_list::List::len (static_array_rb_tree::linked_list::{impl#0}::len)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: linked_list::List::lookup (static_array_rb_tree::linked_list::{impl#0}::lookup)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: linked_list::List::new (static_array_rb_tree::linked_list::{impl#0}::new)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: linked_list::List::push (static_array_rb_tree::linked_list::{impl#0}::push)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: linked_list::List::pop (static_array_rb_tree::linked_list::{impl#0}::pop)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: linked_list::List::overlap (static_array_rb_tree::linked_list::{impl#0}::overlap)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: linked_list::List::overlap_idx (static_array_rb_tree::linked_list::{impl#0}::overlap_idx)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: linked_list::List::range_overlaps_in_list (static_array_rb_tree::linked_list::{impl#0}::range_overlaps_in_list)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: linked_list::Link::len (static_array_rb_tree::linked_list::{impl#1}::len)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: linked_list::Link::is_empty (static_array_rb_tree::linked_list::{impl#1}::is_empty)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: linked_list::Link::lookup (static_array_rb_tree::linked_list::{impl#1}::lookup)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: <trusted_range_inclusive::TrustedRangeInclusive as std::clone::Clone>::clone (static_array_rb_tree::trusted_range_inclusive::{impl#1}::clone)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: <trusted_range_inclusive::TrustedRangeInclusive as std::cmp::PartialEq>::eq (static_array_rb_tree::trusted_range_inclusive::{impl#4}::eq)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: <trusted_range_inclusive::TrustedRangeInclusive as std::cmp::PartialEq>::ne (static_array_rb_tree::trusted_range_inclusive::{impl#4}::ne)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: <trusted_range_inclusive::TrustedRangeInclusive as std::cmp::Eq>::assert_receiver_is_total_eq (static_array_rb_tree::trusted_range_inclusive::{impl#6}::assert_receiver_is_total_eq)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: trusted_range_inclusive::TrustedRangeInclusive::new (static_array_rb_tree::trusted_range_inclusive::{impl#0}::new)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: trusted_range_inclusive::TrustedRangeInclusive::overlap (static_array_rb_tree::trusted_range_inclusive::{impl#0}::overlap)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: trusted_option::peek_range (static_array_rb_tree::trusted_option::peek_range)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: trusted_option::peek_usize (static_array_rb_tree::trusted_option::peek_usize)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: <trusted_option::OptionRange as std::clone::Clone>::clone (static_array_rb_tree::trusted_option::{impl#3}::clone)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: trusted_option::OptionRange::is_none (static_array_rb_tree::trusted_option::{impl#0}::is_none)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: trusted_option::OptionRange::is_some (static_array_rb_tree::trusted_option::{impl#0}::is_some)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: trusted_option::OptionRange::peek (static_array_rb_tree::trusted_option::{impl#0}::peek)
[2022-08-02T20:39:00Z INFO prusti_viper::encoder::encoder] Encoding: trusted_result::peek_usize_range (static_array_rb_tree::trusted_result::peek_usize_range)
[2022-08-02T20:39:00Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Completed: encoding to Viper (0.454 seconds)
[2022-08-02T20:39:00Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Starting: optimizing Viper program
[2022-08-02T20:39:00Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Completed: optimizing Viper program (0.017 seconds)
[2022-08-02T20:39:00Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Starting: verifying Viper program
[2022-08-02T20:39:00Z INFO prusti_viper::verifier] Connecting to Prusti server at localhost:45965
[2022-08-02T20:39:20Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Completed: verifying Viper program (19.817 seconds)
error: could not compile `static_array_rb_tree` due to 2 previous errors; 7 warnings emitted
└──── End stderr ──────┘
Exit code 101, signal null.
Ignored diagnostic message: 'aborting due to previous error; 7 warnings emitted'
Rendering 2 diagnostics at file:///home/ramla/static_array_rb_tree/src/static_array.rs
Rendering 5 diagnostics at file:///home/ramla/static_array_rb_tree/src/linked_list.rs
Rendering 1 diagnostics at file:///home/ramla/static_array_rb_tree/src/lib.rs
