Skip to content

Verify safety of str iter functions (Challenge 22) #557

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jrey8343 wants to merge 16 commits into
base: main
Choose a base branch
from
Open

Verify safety of str iter functions (Challenge 22) #557

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
bdb88ae
Verify safety of char-related Searcher methods (Challenge 20)
jrey8343 Feb 6, 2026
fd5215c
Fix CI: remove loop invariants that cause CBMC assigns check interfer…
jrey8343 Feb 6, 2026
b51df2c
Abstract next_match/next_match_back with #[cfg(kani)] nondeterministi…
jrey8343 Feb 11, 2026
d763699
Fix arithmetic overflow in next_match/next_match_back Kani abstractions
jrey8343 Feb 21, 2026
4a9c0fc
Add UTF-8 boundary constraints, fix overflow, and improve docs
jrey8343 Apr 2, 2026
8e64315
Remove #[cfg(kani)] searcher abstractions; restore upstream pattern.rs
jrey8343 Aug 18, 2026
3c85fa3
Merge remote-tracking branch 'origin/main' into challenge-20-str-pattern
jrey8343 Aug 18, 2026
5fd9a4a
Add Challenge 20 harnesses verifying the real searcher code
jrey8343 Aug 19, 2026
347777d
Document the Challenge 20 haystack bound as an accepted limitation
jrey8343 Sep 2, 2026
2c5b3e7
Add the Searcher contract to CharSearcher::next_match/next_match_back
jrey8343 Sep 13, 2026
7ebd1d4
State the CharSearcher needle clause of C byte-wise
jrey8343 Sep 13, 2026
2a548ca
Write next_match_back's width clause without an addition
jrey8343 Sep 13, 2026
58a19c1
Merge remote-tracking branch 'origin/main' into challenge-20-str-pattern
jrey8343 Oct 7, 2026
256ac0c
Drop the memchr stub: cfg(kani) memchr is memchr_naive since #628
jrey8343 Oct 7, 2026
439dad2
Verify str iter functions (Challenge 22) over the Challenge 20 search…
jrey8343 Oct 7, 2026
fc08a7f
Retrigger CI: the macOS upstream_test runner died mid-step
jrey8343 Oct 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading
Loading