1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
[[92mInfo[39m ] Imported: tests/llbc/string_chars.llbc
[[91mError[39m] In file SymbolicToPure.ml, line 588:
ADTs containing borrows are not supported yet
Source: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20
Uncaught exception:
(Failure
"In file SymbolicToPure.ml, line 588:\
\nIn file SymbolicToPure.ml, line 588:\
\nADTs containing borrows are not supported yet\
\nSource: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20\
\nSource: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20")
Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76
Called from Aeneas__SymbolicToPure.translate_type_decl in file "SymbolicToPure.ml", line 588, characters 2-113
Called from Aeneas__SymbolicToPure.translate_type_decls.(fun) in file "SymbolicToPure.ml", line 3923, characters 15-42
Called from Stdlib__List.filter_map.aux in file "list.ml", line 258, characters 14-17
Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 229, characters 19-64
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 981, characters 4-33
Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61
|
