Add flag to add experimental iterator support

Author: vl0w

docs/dev-guide/src/config/flags.md

@@ -21,6 +21,7 @@
 | [`DUMP_VIPER_PROGRAM`](#dump_viper_program) | `bool` | `false` |
 | [`ENABLE_CACHE`](#enable_cache) | `bool` | `true` |
 | [`ENABLE_GHOST_CONSTRAINTS`](#enable_ghost_constraints) | `bool` | `false` |
+| [`ENABLE_ITERATORS`](#enable_iterators) | `bool` | `false` |
 | [`ENABLE_PURIFICATION_OPTIMIZATION`](#enable_purification_optimization) | `bool` | `false` |
 | [`ENABLE_VERIFY_ONLY_BASIC_BLOCK_PATH`](#enable_verify_only_basic_block_path) | `bool` | `false` |
 | [`ENCODE_BITVECTORS`](#encode_bitvectors) | `bool` | `false` |
@@ -141,6 +142,12 @@ on a generic type parameter) is satisfied.
 
 **This is an experimental feature**, because it is currently possible to introduce unsound verification behavior.
 
+## `ENABLE_ITERATORS`
+
+Enables support for iterators.
+
+**This is an experimental feature**, iterator support is still experimental.
+
 ## `ENABLE_PURIFICATION_OPTIMIZATION`
 
 When enabled, impure methods are optimized using the purification optimization, which tries to convert heap operations to pure (snapshot-based) operations.

prusti-common/src/config.rs

@@ -113,6 +113,7 @@ lazy_static! {
         settings.set_default("print_hash", false).unwrap();
         settings.set_default("enable_cache", true).unwrap();
         settings.set_default("enable_ghost_constraints", false).unwrap();
+        settings.set_default("enable_iterators", false).unwrap();
 
         // Flags for debugging Prusti that can change verification results.
         settings.set_default("disable_name_mangling", false).unwrap();
@@ -599,4 +600,9 @@ pub fn intern_names() -> bool {
 /// Enables ghost constraint parsing and resolving.
 pub fn enable_ghost_constraints() -> bool {
     read_setting("enable_ghost_constraints")
+}
+
+/// Enables (experimental) iterator support
+pub fn enable_iterators() -> bool {
+    read_setting("enable_iterators")
 }

prusti-viper/src/encoder/procedure_encoder.rs

@@ -2196,9 +2196,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                         }
 
                         "std::iter::Iterator::next" |
-                        "core::iter::Iterator::next" => {
+                        "core::iter::Iterator::next" if !config::enable_iterators() => {
                             return Err(SpannedEncodingError::unsupported(
-                                "iterators are not fully supported yet",
+                                "iterators are not fully supported yet, enable them with a feature flag",
                                 term.source_info.span,
                             ));
                         }