Commit c176f19
Update for toolchain nightly-2025-07-10 + Fix loop-invariant (model-checking#417)
This PR replaces the failed PR
model-checking#413 by fixing the
loop invariant for `small_slice_eq`.
Automated PR (413) description:
This is an automated PR to merge library subtree updates from 2025-07-02
(rust-lang@71e4c00)
to 2025-07-10
(rust-lang@e43d139)
(inclusive) into main. git merge resulted in conflicts, which require
manual resolution. Files were commited with merge conflict markers. Do
not remove or edit the following annotations:
git-subtree-dir: library
git-subtree-split: d836404
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---------
Signed-off-by: Ayush Singh <[email protected]>
Signed-off-by: xizheyin <[email protected]>
Co-authored-by: Guillaume Gomez <[email protected]>
Co-authored-by: Jakub Beránek <[email protected]>
Co-authored-by: David Wood <[email protected]>
Co-authored-by: Neal <[email protected]>
Co-authored-by: Tomoaki Kobayashi <[email protected]>
Co-authored-by: Daniel Paoliello <[email protected]>
Co-authored-by: Marijn Schouten <[email protected]>
Co-authored-by: Marijn Schouten <[email protected]>
Co-authored-by: Jubilee <[email protected]>
Co-authored-by: Benoît du Garreau <[email protected]>
Co-authored-by: bors <[email protected]>
Co-authored-by: Trevor Gross <[email protected]>
Co-authored-by: Aniket Mishra <[email protected]>
Co-authored-by: satiscugcat <[email protected]>
Co-authored-by: Jacob Pratt <[email protected]>
Co-authored-by: Jeremy Smart <[email protected]>
Co-authored-by: Mara Bos <[email protected]>
Co-authored-by: Urgau <[email protected]>
Co-authored-by: Zachary S <[email protected]>
Co-authored-by: Trevor Gross <[email protected]>
Co-authored-by: Tim (Theemathas) Chirananthavat <[email protected]>
Co-authored-by: Alice Ryhl <[email protected]>
Co-authored-by: Folkert de Vries <[email protected]>
Co-authored-by: Kornel <[email protected]>
Co-authored-by: LimpSquid <[email protected]>
Co-authored-by: Daniel Bloom <[email protected]>
Co-authored-by: Ed Page <[email protected]>
Co-authored-by: The Miri Cronjob Bot <[email protected]>
Co-authored-by: Chai T. Rex <[email protected]>
Co-authored-by: Valdemar Erk <[email protected]>
Co-authored-by: bjorn3 <[email protected]>
Co-authored-by: Samuel Tardieu <[email protected]>
Co-authored-by: binarycat <[email protected]>
Co-authored-by: Tshepang Mbambo <[email protected]>
Co-authored-by: Matthias Krüger <[email protected]>
Co-authored-by: mejrs <[email protected]>
Co-authored-by: Laine Taffin Altman <[email protected]>
Co-authored-by: Oli Scherer <[email protected]>
Co-authored-by: MetaNova <[email protected]>
Co-authored-by: Kurt Heiritz (pseudo) <[email protected]>
Co-authored-by: krikera <[email protected]>
Co-authored-by: Pavel Grigorenko <[email protected]>
Co-authored-by: Michael Goulet <[email protected]>
Co-authored-by: Bastian Kersting <[email protected]>
Co-authored-by: Deadbeef <[email protected]>
Co-authored-by: Cheng Xu <[email protected]>
Co-authored-by: Chris Denton <[email protected]>
Co-authored-by: наб <[email protected]>
Co-authored-by: kilavvy <[email protected]>
Co-authored-by: Ralf Jung <[email protected]>
Co-authored-by: zachs18 <[email protected]>
Co-authored-by: dianqk <[email protected]>
Co-authored-by: Nurzhan Sakén <[email protected]>
Co-authored-by: Benjamin Schulz <[email protected]>
Co-authored-by: Amanieu d'Antras <[email protected]>
Co-authored-by: Josh Stone <[email protected]>
Co-authored-by: klensy <[email protected]>
Co-authored-by: clubby789 <[email protected]>
Co-authored-by: Jana Dönszelmann <[email protected]>
Co-authored-by: Urgau <[email protected]>
Co-authored-by: Ayush Singh <[email protected]>
Co-authored-by: Ben Kimock <[email protected]>
Co-authored-by: Joshua Gentry <[email protected]>
Co-authored-by: dvdsk <[email protected]>
Co-authored-by: Yotam Ofek <[email protected]>
Co-authored-by: Simonas Kazlauskas <[email protected]>
Co-authored-by: xizheyin <[email protected]>
Co-authored-by: 许杰友 Jieyou Xu (Joe) <[email protected]>
Co-authored-by: Md. Yeasin Arafat <[email protected]>
Co-authored-by: Esteban Küber <[email protected]>
Co-authored-by: gitbot <git@bot>
Co-authored-by: Michael Tautschnig <[email protected]>1 parent e4bedab commit c176f19
File tree
115 files changed
+1421
-992
lines changed- library
- alloctests/tests
- alloc/src
- collections
- vec
- coretests/tests
- num/dec2flt
- core
- src
- alloc
- array
- cell
- ffi
- fmt
- hash
- intrinsics
- io
- iter/sources
- mem
- num
- dec2flt
- ops
- pin
- ptr
- slice
- sort
- stable
- str
- portable-simd/crates/core_simd/src
- rtstartup
- rustc-std-workspace-core
- std
- src
- ffi
- io
- os
- android
- linux
- net/linux_ext
- unix
- sync
- mpmc
- sys
- net/connection
- socket
- uefi
- pal
- hermit
- itron
- sgx
- teeos
- uefi
- unix
- unsupported
- wasi
- wasm/atomics
- windows
- xous
- path
- random
- thread
- tests
- thread_local
- tool_config
- verifast-proofs/alloc/collections
- linked_list.rs-negative
- original
- verified
- linked_list.rs
- original
- verified
Some content is hidden
Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.
115 files changed
+1421
-992
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
429 | 429 | | |
430 | 430 | | |
431 | 431 | | |
432 | | - | |
| 432 | + | |
433 | 433 | | |
434 | 434 | | |
435 | | - | |
| 435 | + | |
436 | 436 | | |
437 | 437 | | |
438 | 438 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
191 | 191 | | |
192 | 192 | | |
193 | 193 | | |
194 | | - | |
| 194 | + | |
195 | 195 | | |
196 | 196 | | |
197 | 197 | | |
| |||
1098 | 1098 | | |
1099 | 1099 | | |
1100 | 1100 | | |
1101 | | - | |
1102 | | - | |
1103 | | - | |
1104 | | - | |
1105 | | - | |
1106 | | - | |
1107 | | - | |
1108 | | - | |
1109 | | - | |
1110 | | - | |
1111 | | - | |
1112 | | - | |
1113 | | - | |
1114 | | - | |
1115 | | - | |
1116 | | - | |
1117 | | - | |
1118 | | - | |
1119 | | - | |
1120 | | - | |
1121 | | - | |
1122 | | - | |
1123 | | - | |
1124 | | - | |
1125 | | - | |
1126 | | - | |
1127 | | - | |
1128 | | - | |
1129 | | - | |
1130 | | - | |
1131 | | - | |
1132 | | - | |
1133 | | - | |
1134 | | - | |
1135 | | - | |
1136 | | - | |
1137 | | - | |
1138 | | - | |
1139 | | - | |
1140 | | - | |
1141 | | - | |
1142 | | - | |
1143 | | - | |
1144 | | - | |
1145 | | - | |
1146 | | - | |
1147 | | - | |
1148 | | - | |
1149 | | - | |
1150 | | - | |
1151 | | - | |
1152 | | - | |
1153 | | - | |
1154 | | - | |
1155 | | - | |
1156 | | - | |
1157 | | - | |
1158 | | - | |
1159 | | - | |
1160 | | - | |
1161 | | - | |
1162 | | - | |
1163 | | - | |
1164 | | - | |
1165 | | - | |
1166 | | - | |
1167 | | - | |
1168 | | - | |
1169 | | - | |
1170 | | - | |
1171 | | - | |
1172 | | - | |
1173 | | - | |
1174 | | - | |
1175 | | - | |
1176 | | - | |
1177 | | - | |
1178 | | - | |
1179 | | - | |
1180 | | - | |
1181 | | - | |
1182 | | - | |
1183 | | - | |
1184 | | - | |
1185 | | - | |
1186 | | - | |
1187 | | - | |
1188 | | - | |
1189 | | - | |
1190 | | - | |
1191 | | - | |
1192 | | - | |
1193 | | - | |
1194 | | - | |
1195 | | - | |
1196 | | - | |
1197 | | - | |
1198 | | - | |
1199 | | - | |
1200 | | - | |
1201 | | - | |
1202 | | - | |
1203 | | - | |
1204 | | - | |
1205 | | - | |
1206 | | - | |
1207 | | - | |
1208 | | - | |
1209 | | - | |
1210 | 1101 | | |
1211 | 1102 | | |
1212 | 1103 | | |
| |||
1259 | 1150 | | |
1260 | 1151 | | |
1261 | 1152 | | |
1262 | | - | |
1263 | | - | |
| 1153 | + | |
| 1154 | + | |
| 1155 | + | |
| 1156 | + | |
| 1157 | + | |
1264 | 1158 | | |
1265 | 1159 | | |
1266 | 1160 | | |
| |||
1322 | 1216 | | |
1323 | 1217 | | |
1324 | 1218 | | |
| 1219 | + | |
| 1220 | + | |
| 1221 | + | |
| 1222 | + | |
| 1223 | + | |
| 1224 | + | |
| 1225 | + | |
| 1226 | + | |
| 1227 | + | |
| 1228 | + | |
| 1229 | + | |
| 1230 | + | |
| 1231 | + | |
| 1232 | + | |
| 1233 | + | |
| 1234 | + | |
| 1235 | + | |
| 1236 | + | |
| 1237 | + | |
| 1238 | + | |
| 1239 | + | |
| 1240 | + | |
| 1241 | + | |
| 1242 | + | |
| 1243 | + | |
| 1244 | + | |
| 1245 | + | |
| 1246 | + | |
| 1247 | + | |
| 1248 | + | |
| 1249 | + | |
| 1250 | + | |
| 1251 | + | |
| 1252 | + | |
| 1253 | + | |
| 1254 | + | |
| 1255 | + | |
| 1256 | + | |
| 1257 | + | |
| 1258 | + | |
| 1259 | + | |
| 1260 | + | |
| 1261 | + | |
| 1262 | + | |
| 1263 | + | |
| 1264 | + | |
| 1265 | + | |
| 1266 | + | |
| 1267 | + | |
| 1268 | + | |
| 1269 | + | |
| 1270 | + | |
| 1271 | + | |
| 1272 | + | |
| 1273 | + | |
| 1274 | + | |
| 1275 | + | |
| 1276 | + | |
| 1277 | + | |
| 1278 | + | |
| 1279 | + | |
| 1280 | + | |
| 1281 | + | |
| 1282 | + | |
| 1283 | + | |
| 1284 | + | |
| 1285 | + | |
| 1286 | + | |
| 1287 | + | |
| 1288 | + | |
| 1289 | + | |
| 1290 | + | |
| 1291 | + | |
| 1292 | + | |
| 1293 | + | |
| 1294 | + | |
| 1295 | + | |
| 1296 | + | |
| 1297 | + | |
| 1298 | + | |
| 1299 | + | |
| 1300 | + | |
| 1301 | + | |
| 1302 | + | |
| 1303 | + | |
| 1304 | + | |
| 1305 | + | |
| 1306 | + | |
| 1307 | + | |
| 1308 | + | |
| 1309 | + | |
| 1310 | + | |
| 1311 | + | |
| 1312 | + | |
| 1313 | + | |
| 1314 | + | |
| 1315 | + | |
| 1316 | + | |
| 1317 | + | |
| 1318 | + | |
| 1319 | + | |
| 1320 | + | |
| 1321 | + | |
| 1322 | + | |
| 1323 | + | |
| 1324 | + | |
| 1325 | + | |
| 1326 | + | |
| 1327 | + | |
1325 | 1328 | | |
1326 | 1329 | | |
1327 | 1330 | | |
| |||
1602 | 1605 | | |
1603 | 1606 | | |
1604 | 1607 | | |
1605 | | - | |
| 1608 | + | |
| 1609 | + | |
| 1610 | + | |
1606 | 1611 | | |
1607 | 1612 | | |
1608 | 1613 | | |
| |||
2127 | 2132 | | |
2128 | 2133 | | |
2129 | 2134 | | |
2130 | | - | |
2131 | | - | |
2132 | | - | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1031 | 1031 | | |
1032 | 1032 | | |
1033 | 1033 | | |
1034 | | - | |
| 1034 | + | |
1035 | 1035 | | |
1036 | 1036 | | |
1037 | 1037 | | |
| |||
1047 | 1047 | | |
1048 | 1048 | | |
1049 | 1049 | | |
1050 | | - | |
| 1050 | + | |
1051 | 1051 | | |
1052 | 1052 | | |
1053 | 1053 | | |
| |||
1074 | 1074 | | |
1075 | 1075 | | |
1076 | 1076 | | |
1077 | | - | |
1078 | | - | |
1079 | | - | |
1080 | | - | |
1081 | | - | |
1082 | | - | |
1083 | | - | |
1084 | | - | |
1085 | | - | |
1086 | | - | |
1087 | | - | |
1088 | | - | |
1089 | | - | |
1090 | | - | |
1091 | | - | |
1092 | | - | |
1093 | | - | |
1094 | | - | |
1095 | | - | |
1096 | | - | |
1097 | | - | |
1098 | | - | |
1099 | | - | |
1100 | | - | |
1101 | | - | |
1102 | | - | |
1103 | | - | |
1104 | | - | |
1105 | | - | |
1106 | | - | |
1107 | | - | |
1108 | | - | |
1109 | | - | |
1110 | | - | |
1111 | | - | |
1112 | 1077 | | |
1113 | 1078 | | |
1114 | 1079 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
108 | 108 | | |
109 | 109 | | |
110 | 110 | | |
| 111 | + | |
111 | 112 | | |
112 | 113 | | |
| 114 | + | |
113 | 115 | | |
114 | 116 | | |
115 | 117 | | |
| |||
135 | 137 | | |
136 | 138 | | |
137 | 139 | | |
138 | | - | |
139 | 140 | | |
140 | 141 | | |
141 | 142 | | |
| |||
0 commit comments