Add support for iter next

[zhassan-aws]

Filing this tracking issue for unsupported predicates with bound regions.

This is an example program that triggers the issue:

fn main() {
    let a = [1, 2, 3];
    let _x = a.iter().next();
}

$ charon
   Compiling any v0.1.0 (/home/ubuntu/examples/aeneas/any)
error: Predicates with bound regions (i.e., `for<'a> ...`) are not supported yet
   --> /home/ubuntu/.rustup/toolchains/nightly-2023-06-02-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:131:1
    |
131 | / iterator! {struct Iter -> *const T, &'a T, const, {/* no mut */}, {
132 | |     fn is_sorted_by<F>(self, mut compare: F) -> bool
133 | |     where
134 | |         Self: Sized,
...   |
138 | |     }
139 | | }}
    | |__^
    |
    = note: this error originates in the macro `iterator` (in Nightly builds, run with -Z macro-backtrace for more info)

error: Ignoring the following function due to an error: DefId(2:42967 ~ core[6c80]::slice::iter::{impl#181}::find)
   --> /home/ubuntu/.rustup/toolchains/nightly-2023-06-02-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:131:1
    |
131 | / iterator! {struct Iter -> *const T, &'a T, const, {/* no mut */}, {
132 | |     fn is_sorted_by<F>(self, mut compare: F) -> bool
133 | |     where
134 | |         Self: Sized,
...   |
138 | |     }
139 | | }}
    | |__^
    |
    = note: this error originates in the macro `iterator` (in Nightly builds, run with -Z macro-backtrace for more info)

error: Predicates with bound regions (i.e., `for<'a> ...`) are not supported yet
   --> /home/ubuntu/.rustup/toolchains/nightly-2023-06-02-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:135:12
    |
135 |         F: FnMut(&Self::Item, &Self::Item) -> Option<Ordering>,
    |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: Ignoring the following function due to an error: DefId(2:42977 ~ core[6c80]::slice::iter::{impl#181}::is_sorted_by)
   --> /home/ubuntu/.rustup/toolchains/nightly-2023-06-02-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:132:5
    |
132 | /     fn is_sorted_by<F>(self, mut compare: F) -> bool
133 | |     where
134 | |         Self: Sized,
135 | |         F: FnMut(&Self::Item, &Self::Item) -> Option<Ordering>,
    | |_______________________________________________________________^

error: The external definition DefId(2:42977 ~ core[6c80]::slice::iter::{impl#181}::is_sorted_by) triggered errors. It is (transitively) used at the following location(s):
 --> src/main.rs:3:14
  |
3 |     let _x = a.iter().next();
  |              ^^^^^^^^^^^^^^^

error: The external definition DefId(2:42967 ~ core[6c80]::slice::iter::{impl#181}::find) triggered errors. It is (transitively) used at the following location(s):
 --> src/main.rs:3:14
  |
3 |     let _x = a.iter().next();
  |              ^^^^^^^^^^^^^^^

[ INFO charon_driver::export:101] [gexport]: Generated the partial (because we encountered errors) file: /home/ubuntu/examples/aeneas/any/any.llbc
[ ERROR charon_driver:231] The extraction encountered 4 errors
error: could not compile `any` (bin "any") due to 6 previous errors

[sonmarcho]

Yes, Charon doesn't support bound regions for now. I opened a related issue #79

[Nadrieril]

Closing as duplicate then