Skip to content

Commit ceaa320

Browse files
tautschnigtautschnig
authored
Merge branch 'main' into add-rewards
2 parents dbec660 + 2a203c5 commit ceaa320

File tree

417 files changed

+17308
-8874
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

417 files changed

+17308
-8874
lines changed

‎.github/workflows/flux.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ on:
99

1010
env:
1111
FIXPOINT_VERSION: "556104ba5508891c357b0bdf819ce706e93d9349"
12-
FLUX_VERSION: "ebafb8d0ca32d8c0fcd2a0cfef6b1b4bd4dc4a6f"
12+
FLUX_VERSION: "a17246965a8752e3d3d4e3559865311048bb61f7"
1313

1414
jobs:
1515
check-flux-on-core:

‎.github/workflows/verifast-negative.yml

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -30,16 +30,16 @@ jobs:
3030
- name: Install VeriFast
3131
run: |
3232
cd ~
33-
curl -OL https://github.com/verifast/verifast/releases/download/25.02/verifast-25.02-linux.tar.gz
34-
# https://github.com/verifast/verifast/attestations/4911733
35-
echo '5d5c87d11b3d735f44c3f0ca52aebc89e3c4d1119d98ef25188d07cb57ad65e8 verifast-25.02-linux.tar.gz' | shasum -a 256 -c
36-
tar xf verifast-25.02-linux.tar.gz
33+
curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
34+
# https://github.com/verifast/verifast/attestations/8998468
35+
echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b verifast-25.07-linux.tar.gz' | shasum -a 256 -c
36+
tar xf verifast-25.07-linux.tar.gz
3737
3838
- name: Install the Rust toolchain used by VeriFast
39-
run: rustup toolchain install nightly-2024-11-23
39+
run: rustup toolchain install nightly-2025-04-09
4040

4141
- name: Run VeriFast Verification
4242
run: |
43-
export PATH=~/verifast-25.02/bin:$PATH
43+
export PATH=~/verifast-25.07/bin:$PATH
4444
cd verifast-proofs
4545
bash check-verifast-proofs-negative.sh

‎.github/workflows/verifast.yml

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -27,17 +27,17 @@ jobs:
2727
- name: Install VeriFast
2828
run: |
2929
cd ~
30-
curl -OL https://github.com/verifast/verifast/releases/download/25.02/verifast-25.02-linux.tar.gz
31-
# https://github.com/verifast/verifast/attestations/4911733
32-
echo '5d5c87d11b3d735f44c3f0ca52aebc89e3c4d1119d98ef25188d07cb57ad65e8 verifast-25.02-linux.tar.gz' | shasum -a 256 -c
33-
tar xf verifast-25.02-linux.tar.gz
30+
curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
31+
# https://github.com/verifast/verifast/attestations/8998468
32+
echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b verifast-25.07-linux.tar.gz' | shasum -a 256 -c
33+
tar xf verifast-25.07-linux.tar.gz
3434
3535
- name: Install the Rust toolchain used by VeriFast
36-
run: rustup toolchain install nightly-2024-11-23
36+
run: rustup toolchain install nightly-2025-04-09
3737

3838
- name: Run VeriFast Verification
3939
run: |
40-
export PATH=~/verifast-25.02/bin:$PATH
40+
export PATH=~/verifast-25.07/bin:$PATH
4141
cd verifast-proofs
4242
bash check-verifast-proofs.sh
4343

‎doc/src/challenges/0005-linked-list.md

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,11 @@
11
# Challenge 5: Verify functions iterating over inductive data type: `linked_list`
22

3-
- **Status:** Open
3+
- **Status:** Resolved
44
- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
55
- **Start date:** *2024/07/01*
6-
- **End date:** *2025/04/10*
6+
- **End date:** *2025/08/12*
77
- **Reward:** *20000 USD*
8+
- **Contributors:** [Bart Jacobs](https://github.com/btj)
89

910
-------------------
1011

‎doc/src/challenges/0019-rawvec.md

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,11 @@
1-
# Challenge 25: Verify the safety of `RawVec` functions
1+
# Challenge 19: Verify the safety of `RawVec` functions
22

3-
- **Status:** Open
3+
- **Status:** Resolved
44
- **Tracking Issue:** [#283](https://github.com/model-checking/verify-rust-std/issues/283)
55
- **Start date:** *2025-03-07*
6-
- **End date:** *2025-10-17*
6+
- **End date:** *2025-08-12*
77
- **Reward:** *10000 USD*
8+
- **Contributors:** [Bart Jacobs](https://github.com/btj)
89

910
-------------------
1011

‎doc/src/tools.md

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,7 @@ please see the [Tool Application](general-rules.md#tool-applications) section.
1111

1212
| Tool | CI Status |
1313
|---------------------|-------|
14+
| ESBMC (GOTO-Transcoder) | [![ESBMC](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml) |
15+
| Flux | [![Flux](https://github.com/model-checking/verify-rust-std/actions/workflows/flux.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/flux.yml) |
1416
| Kani Rust Verifier | [![Kani](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml) |
15-
| GOTO-Transcoder (ESBMC) | [![GOTO-Transcoder](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml) |
1617
| VeriFast for Rust | [![VeriFast](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml) |
17-
18-
19-
20-

‎library/Cargo.lock

Lines changed: 2 additions & 4 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎library/alloc/src/boxed.rs

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1672,7 +1672,7 @@ unsafe impl<#[may_dangle] T: ?Sized, A: Allocator> Drop for Box<T, A> {
16721672
#[cfg(not(no_global_oom_handling))]
16731673
#[stable(feature = "rust1", since = "1.0.0")]
16741674
impl<T: Default> Default for Box<T> {
1675-
/// Creates a `Box<T>`, with the `Default` value for T.
1675+
/// Creates a `Box<T>`, with the `Default` value for `T`.
16761676
#[inline]
16771677
fn default() -> Self {
16781678
let mut x: Box<mem::MaybeUninit<T>> = Box::new_uninit();
@@ -1695,6 +1695,7 @@ impl<T: Default> Default for Box<T> {
16951695
#[cfg(not(no_global_oom_handling))]
16961696
#[stable(feature = "rust1", since = "1.0.0")]
16971697
impl<T> Default for Box<[T]> {
1698+
/// Creates an empty `[T]` inside a `Box`.
16981699
#[inline]
16991700
fn default() -> Self {
17001701
let ptr: Unique<[T]> = Unique::<[T; 0]>::dangling();
@@ -1716,6 +1717,19 @@ impl Default for Box<str> {
17161717
}
17171718
}
17181719

1720+
#[cfg(not(no_global_oom_handling))]
1721+
#[stable(feature = "pin_default_impls", since = "CURRENT_RUSTC_VERSION")]
1722+
impl<T> Default for Pin<Box<T>>
1723+
where
1724+
T: ?Sized,
1725+
Box<T>: Default,
1726+
{
1727+
#[inline]
1728+
fn default() -> Self {
1729+
Box::into_pin(Box::<T>::default())
1730+
}
1731+
}
1732+
17191733
#[cfg(not(no_global_oom_handling))]
17201734
#[stable(feature = "rust1", since = "1.0.0")]
17211735
impl<T: Clone, A: Allocator + Clone> Clone for Box<T, A> {

‎library/alloc/src/collections/btree/map.rs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,8 @@ pub(super) const MIN_LEN: usize = node::MIN_LEN_AFTER_SPLIT;
135135
/// ]);
136136
/// ```
137137
///
138+
/// ## `Entry` API
139+
///
138140
/// `BTreeMap` implements an [`Entry API`], which allows for complex
139141
/// methods of getting, setting, updating and removing keys and their values:
140142
///
@@ -382,6 +384,7 @@ impl<'a, K: 'a, V: 'a> Default for Iter<'a, K, V> {
382384
/// documentation for more.
383385
///
384386
/// [`iter_mut`]: BTreeMap::iter_mut
387+
#[must_use = "iterators are lazy and do nothing unless consumed"]
385388
#[stable(feature = "rust1", since = "1.0.0")]
386389
pub struct IterMut<'a, K: 'a, V: 'a> {
387390
range: LazyLeafRange<marker::ValMut<'a>, K, V>,
@@ -391,7 +394,6 @@ pub struct IterMut<'a, K: 'a, V: 'a> {
391394
_marker: PhantomData<&'a mut (K, V)>,
392395
}
393396

394-
#[must_use = "iterators are lazy and do nothing unless consumed"]
395397
#[stable(feature = "collection_debug", since = "1.17.0")]
396398
impl<K: fmt::Debug, V: fmt::Debug> fmt::Debug for IterMut<'_, K, V> {
397399
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

‎library/alloc/src/ffi/c_str.rs

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1099,7 +1099,7 @@ impl From<&CStr> for CString {
10991099
}
11001100
}
11011101

1102-
#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
1102+
#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
11031103
impl PartialEq<CStr> for CString {
11041104
#[inline]
11051105
fn eq(&self, other: &CStr) -> bool {
@@ -1112,7 +1112,7 @@ impl PartialEq<CStr> for CString {
11121112
}
11131113
}
11141114

1115-
#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
1115+
#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
11161116
impl PartialEq<&CStr> for CString {
11171117
#[inline]
11181118
fn eq(&self, other: &&CStr) -> bool {
@@ -1126,7 +1126,7 @@ impl PartialEq<&CStr> for CString {
11261126
}
11271127

11281128
#[cfg(not(no_global_oom_handling))]
1129-
#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
1129+
#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
11301130
impl PartialEq<Cow<'_, CStr>> for CString {
11311131
#[inline]
11321132
fn eq(&self, other: &Cow<'_, CStr>) -> bool {
@@ -1221,7 +1221,7 @@ impl CStr {
12211221
}
12221222
}
12231223

1224-
#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
1224+
#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
12251225
impl PartialEq<CString> for CStr {
12261226
#[inline]
12271227
fn eq(&self, other: &CString) -> bool {
@@ -1235,7 +1235,7 @@ impl PartialEq<CString> for CStr {
12351235
}
12361236

12371237
#[cfg(not(no_global_oom_handling))]
1238-
#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
1238+
#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
12391239
impl PartialEq<Cow<'_, Self>> for CStr {
12401240
#[inline]
12411241
fn eq(&self, other: &Cow<'_, Self>) -> bool {
@@ -1249,7 +1249,7 @@ impl PartialEq<Cow<'_, Self>> for CStr {
12491249
}
12501250

12511251
#[cfg(not(no_global_oom_handling))]
1252-
#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
1252+
#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
12531253
impl PartialEq<CStr> for Cow<'_, CStr> {
12541254
#[inline]
12551255
fn eq(&self, other: &CStr) -> bool {
@@ -1263,7 +1263,7 @@ impl PartialEq<CStr> for Cow<'_, CStr> {
12631263
}
12641264

12651265
#[cfg(not(no_global_oom_handling))]
1266-
#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
1266+
#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
12671267
impl PartialEq<&CStr> for Cow<'_, CStr> {
12681268
#[inline]
12691269
fn eq(&self, other: &&CStr) -> bool {
@@ -1277,7 +1277,7 @@ impl PartialEq<&CStr> for Cow<'_, CStr> {
12771277
}
12781278

12791279
#[cfg(not(no_global_oom_handling))]
1280-
#[stable(feature = "c_string_eq_c_str", since = "CURRENT_RUSTC_VERSION")]
1280+
#[stable(feature = "c_string_eq_c_str", since = "1.90.0")]
12811281
impl PartialEq<CString> for Cow<'_, CStr> {
12821282
#[inline]
12831283
fn eq(&self, other: &CString) -> bool {

0 commit comments

Comments
 (0)