add loop-invariants and harnesses #16
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…#428) This is an automated PR to merge library subtree updates from 2025-07-14 (rust-lang/rust@e9182f1) to 2025-07-21 (rust-lang/rust@9982d64) (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: 62f8613 --------- Signed-off-by: Ayush Singh <[email protected]> Signed-off-by: xizheyin <[email protected]> Signed-off-by: Huang Qi <[email protected]> Co-authored-by: Marijn Schouten <[email protected]> Co-authored-by: Oli Scherer <[email protected]> Co-authored-by: Ralf Jung <[email protected]> Co-authored-by: Matthias Krüger <[email protected]> Co-authored-by: наб <[email protected]> Co-authored-by: bors <[email protected]> Co-authored-by: klensy <[email protected]> Co-authored-by: Folkert de Vries <[email protected]> Co-authored-by: clubby789 <[email protected]> Co-authored-by: Tsukasa OI <[email protected]> Co-authored-by: Jana Dönszelmann <[email protected]> Co-authored-by: Deadbeef <[email protected]> Co-authored-by: Guillaume Gomez <[email protected]> Co-authored-by: Daniel Paoliello <[email protected]> Co-authored-by: Urgau <[email protected]> Co-authored-by: Michael Goulet <[email protected]> Co-authored-by: Jacob Pratt <[email protected]> Co-authored-by: The Miri Cronjob Bot <[email protected]> Co-authored-by: Ayush Singh <[email protected]> Co-authored-by: Trevor Gross <[email protected]> Co-authored-by: Kurt Heiritz (pseudo) <[email protected]> Co-authored-by: Jubilee <[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: Chris Denton <[email protected]> Co-authored-by: Md. Yeasin Arafat <[email protected]> Co-authored-by: mejrs <[email protected]> Co-authored-by: Jakub Beránek <[email protected]> Co-authored-by: Amanieu d'Antras <[email protected]> Co-authored-by: ltdk <[email protected]> Co-authored-by: okaneco <[email protected]> Co-authored-by: kilavvy <[email protected]> Co-authored-by: Pavel Grigorenko <[email protected]> Co-authored-by: Esteban Küber <[email protected]> Co-authored-by: sayantn <[email protected]> Co-authored-by: George Tokmaji <[email protected]> Co-authored-by: Moulins <[email protected]> Co-authored-by: Josh Stone <[email protected]> Co-authored-by: Trevor Gross <[email protected]> Co-authored-by: B I Mohammed Abbas <[email protected]> Co-authored-by: Benoît du Garreau <[email protected]> Co-authored-by: Josh Triplett <[email protected]> Co-authored-by: yukang <[email protected]> Co-authored-by: Roger Curley <[email protected]> Co-authored-by: LevitatingBusinessMan (Rein Fernhout) <[email protected]> Co-authored-by: Harvey Hunt <[email protected]> Co-authored-by: Colten <[email protected]> Co-authored-by: Huang Qi <[email protected]> Co-authored-by: nazo6 <[email protected]> Co-authored-by: León Orell Valerian Liehr <[email protected]> Co-authored-by: Orson Peters <[email protected]> Co-authored-by: René Kijewski <[email protected]> Co-authored-by: Nik Revenco <[email protected]> Co-authored-by: Tim (Theemathas) Chirananthavat <[email protected]> Co-authored-by: Samuel Tardieu <[email protected]> Co-authored-by: Travis Cross <[email protected]> Co-authored-by: David Mládek <[email protected]> Co-authored-by: Cameron Steffen <[email protected]> Co-authored-by: Martin Ombura Jr <[email protected]> Co-authored-by: Luigi Sartor Piucco <[email protected]> Co-authored-by: Rémy Rakic <[email protected]> Co-authored-by: Nurzhan Sakén <[email protected]> Co-authored-by: gitbot <git@bot> Co-authored-by: Michael Tautschnig <[email protected]>
…#432) This is an automated PR to merge library subtree updates from 2025-07-21 (rust-lang/rust@9982d64) to 2025-07-30 (rust-lang/rust@ba7e63b) (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: 2f8dad2 --------- Signed-off-by: xizheyin <[email protected]> Signed-off-by: Ayush Singh <[email protected]> Co-authored-by: Marijn Schouten <[email protected]> Co-authored-by: Roger Curley <[email protected]> Co-authored-by: Ralf Jung <[email protected]> Co-authored-by: Josh Triplett <[email protected]> Co-authored-by: Matthias Krüger <[email protected]> Co-authored-by: Folkert de Vries <[email protected]> Co-authored-by: okaneco <[email protected]> Co-authored-by: Folkert de Vries <[email protected]> Co-authored-by: Sayantan Chakraborty <[email protected]> Co-authored-by: nazo6 <[email protected]> Co-authored-by: bors <[email protected]> Co-authored-by: Jakub Beránek <[email protected]> Co-authored-by: Orson Peters <[email protected]> Co-authored-by: León Orell Valerian Liehr <[email protected]> Co-authored-by: xizheyin <[email protected]> Co-authored-by: Deadbeef <[email protected]> Co-authored-by: René Kijewski <[email protected]> Co-authored-by: Nik Revenco <[email protected]> Co-authored-by: The Miri Cronjob Bot <[email protected]> Co-authored-by: Tim (Theemathas) Chirananthavat <[email protected]> Co-authored-by: Chris Denton <[email protected]> Co-authored-by: Samuel Tardieu <[email protected]> Co-authored-by: Travis Cross <[email protected]> Co-authored-by: Amanieu d'Antras <[email protected]> Co-authored-by: Oli Scherer <[email protected]> Co-authored-by: David Mládek <[email protected]> Co-authored-by: SunkenPotato <[email protected]> Co-authored-by: Cameron Steffen <[email protected]> Co-authored-by: Martin Ombura Jr <[email protected]> Co-authored-by: Madhav Madhusoodanan <[email protected]> Co-authored-by: sayantn <[email protected]> Co-authored-by: Trevor Gross <[email protected]> Co-authored-by: WANG Rui <[email protected]> Co-authored-by: Luigi Sartor Piucco <[email protected]> Co-authored-by: Julien THILLARD <[email protected]> Co-authored-by: The rustc-josh-sync Cronjob Bot <[email protected]> Co-authored-by: usamoi <[email protected]> Co-authored-by: Rémy Rakic <[email protected]> Co-authored-by: Nurzhan Sakén <[email protected]> Co-authored-by: ltdk <[email protected]> Co-authored-by: bjorn3 <[email protected]> Co-authored-by: Guillaume Gomez <[email protected]> Co-authored-by: Evgenii Zheltonozhskii <[email protected]> Co-authored-by: roblabla <[email protected]> Co-authored-by: 许杰友 Jieyou Xu (Joe) <[email protected]> Co-authored-by: Ayush Singh <[email protected]> Co-authored-by: Kornel <[email protected]> Co-authored-by: Jonas Platte <[email protected]> Co-authored-by: Alex Crichton <[email protected]> Co-authored-by: Zachary S <[email protected]> Co-authored-by: Jeremy Smart <[email protected]> Co-authored-by: Ivan Tadeu Ferreira Antunes Filho <[email protected]> Co-authored-by: Alisa Sireneva <[email protected]> Co-authored-by: Trevor Gross <[email protected]> Co-authored-by: Jacob Pratt <[email protected]> Co-authored-by: Scott McMurray <[email protected]> Co-authored-by: xonx <[email protected]> Co-authored-by: Yosh <[email protected]> Co-authored-by: joboet <[email protected]> Co-authored-by: Stuart Cook <[email protected]> Co-authored-by: Connor Tsui <[email protected]> Co-authored-by: Aandreba <[email protected]> Co-authored-by: Lucas Werkmeister <[email protected]> Co-authored-by: gitbot <git@bot> Co-authored-by: Michael Tautschnig <[email protected]>
…#437) This is an automated PR to merge library subtree updates from 2025-07-30 (rust-lang/rust@ba7e63b) to 2025-07-31 (rust-lang/rust@3048886), inclusive. This is a clean merge, no conflicts were detected. **Do not remove or edit the following annotations:** git-subtree-dir: library git-subtree-split: af745a4 --------- Signed-off-by: xizheyin <[email protected]> Signed-off-by: Ayush Singh <[email protected]> Co-authored-by: Roger Curley <[email protected]> Co-authored-by: Ralf Jung <[email protected]> Co-authored-by: Marijn Schouten <[email protected]> Co-authored-by: Josh Triplett <[email protected]> Co-authored-by: Matthias Krüger <[email protected]> Co-authored-by: Folkert de Vries <[email protected]> Co-authored-by: okaneco <[email protected]> Co-authored-by: Folkert de Vries <[email protected]> Co-authored-by: Sayantan Chakraborty <[email protected]> Co-authored-by: nazo6 <[email protected]> Co-authored-by: bors <[email protected]> Co-authored-by: Jakub Beránek <[email protected]> Co-authored-by: Orson Peters <[email protected]> Co-authored-by: León Orell Valerian Liehr <[email protected]> Co-authored-by: xizheyin <[email protected]> Co-authored-by: Deadbeef <[email protected]> Co-authored-by: René Kijewski <[email protected]> Co-authored-by: Nik Revenco <[email protected]> Co-authored-by: The Miri Cronjob Bot <[email protected]> Co-authored-by: Tim (Theemathas) Chirananthavat <[email protected]> Co-authored-by: Chris Denton <[email protected]> Co-authored-by: Samuel Tardieu <[email protected]> Co-authored-by: Travis Cross <[email protected]> Co-authored-by: Amanieu d'Antras <[email protected]> Co-authored-by: Oli Scherer <[email protected]> Co-authored-by: David Mládek <[email protected]> Co-authored-by: SunkenPotato <[email protected]> Co-authored-by: Cameron Steffen <[email protected]> Co-authored-by: Martin Ombura Jr <[email protected]> Co-authored-by: Madhav Madhusoodanan <[email protected]> Co-authored-by: sayantn <[email protected]> Co-authored-by: Trevor Gross <[email protected]> Co-authored-by: WANG Rui <[email protected]> Co-authored-by: Luigi Sartor Piucco <[email protected]> Co-authored-by: Julien THILLARD <[email protected]> Co-authored-by: The rustc-josh-sync Cronjob Bot <[email protected]> Co-authored-by: usamoi <[email protected]> Co-authored-by: Rémy Rakic <[email protected]> Co-authored-by: Nurzhan Sakén <[email protected]> Co-authored-by: ltdk <[email protected]> Co-authored-by: bjorn3 <[email protected]> Co-authored-by: Guillaume Gomez <[email protected]> Co-authored-by: Evgenii Zheltonozhskii <[email protected]> Co-authored-by: roblabla <[email protected]> Co-authored-by: 许杰友 Jieyou Xu (Joe) <[email protected]> Co-authored-by: Ayush Singh <[email protected]> Co-authored-by: Kornel <[email protected]> Co-authored-by: Jonas Platte <[email protected]> Co-authored-by: Alex Crichton <[email protected]> Co-authored-by: Zachary S <[email protected]> Co-authored-by: Jeremy Smart <[email protected]> Co-authored-by: Ivan Tadeu Ferreira Antunes Filho <[email protected]> Co-authored-by: Alisa Sireneva <[email protected]> Co-authored-by: Trevor Gross <[email protected]> Co-authored-by: Jacob Pratt <[email protected]> Co-authored-by: Scott McMurray <[email protected]> Co-authored-by: xonx <[email protected]> Co-authored-by: Yosh <[email protected]> Co-authored-by: joboet <[email protected]> Co-authored-by: Stuart Cook <[email protected]> Co-authored-by: Connor Tsui <[email protected]> Co-authored-by: Aandreba <[email protected]> Co-authored-by: Lucas Werkmeister <[email protected]> Co-authored-by: gitbot <git@bot>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <[email protected]>
…g#435) Preconditions generated by Claude for files containing `__iterator_get_unchecked`. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Fedor Ryabinin <[email protected]> Co-authored-by: Michael Tautschnig <[email protected]> Co-authored-by: Felipe R. Monteiro <[email protected]>
…#441) This is an automated PR to merge library subtree updates from 2025-07-31 (rust-lang/rust@3048886) to 2025-08-01 (rust-lang/rust@adcb3d3), inclusive. This is a clean merge, no conflicts were detected. **Do not remove or edit the following annotations:** git-subtree-dir: library git-subtree-split: 158ca24 --------- Signed-off-by: xizheyin <[email protected]> Signed-off-by: Ayush Singh <[email protected]> Co-authored-by: Ralf Jung <[email protected]> Co-authored-by: Marijn Schouten <[email protected]> Co-authored-by: Josh Triplett <[email protected]> Co-authored-by: Matthias Krüger <[email protected]> Co-authored-by: Folkert de Vries <[email protected]> Co-authored-by: okaneco <[email protected]> Co-authored-by: Folkert de Vries <[email protected]> Co-authored-by: Sayantan Chakraborty <[email protected]> Co-authored-by: nazo6 <[email protected]> Co-authored-by: bors <[email protected]> Co-authored-by: Jakub Beránek <[email protected]> Co-authored-by: Orson Peters <[email protected]> Co-authored-by: León Orell Valerian Liehr <[email protected]> Co-authored-by: xizheyin <[email protected]> Co-authored-by: Deadbeef <[email protected]> Co-authored-by: René Kijewski <[email protected]> Co-authored-by: Nik Revenco <[email protected]> Co-authored-by: The Miri Cronjob Bot <[email protected]> Co-authored-by: Tim (Theemathas) Chirananthavat <[email protected]> Co-authored-by: Chris Denton <[email protected]> Co-authored-by: Samuel Tardieu <[email protected]> Co-authored-by: Travis Cross <[email protected]> Co-authored-by: Amanieu d'Antras <[email protected]> Co-authored-by: Oli Scherer <[email protected]> Co-authored-by: David Mládek <[email protected]> Co-authored-by: SunkenPotato <[email protected]> Co-authored-by: Cameron Steffen <[email protected]> Co-authored-by: Martin Ombura Jr <[email protected]> Co-authored-by: Madhav Madhusoodanan <[email protected]> Co-authored-by: sayantn <[email protected]> Co-authored-by: Trevor Gross <[email protected]> Co-authored-by: WANG Rui <[email protected]> Co-authored-by: Luigi Sartor Piucco <[email protected]> Co-authored-by: Julien THILLARD <[email protected]> Co-authored-by: The rustc-josh-sync Cronjob Bot <[email protected]> Co-authored-by: usamoi <[email protected]> Co-authored-by: Rémy Rakic <[email protected]> Co-authored-by: Nurzhan Sakén <[email protected]> Co-authored-by: ltdk <[email protected]> Co-authored-by: bjorn3 <[email protected]> Co-authored-by: Guillaume Gomez <[email protected]> Co-authored-by: Evgenii Zheltonozhskii <[email protected]> Co-authored-by: roblabla <[email protected]> Co-authored-by: 许杰友 Jieyou Xu (Joe) <[email protected]> Co-authored-by: Ayush Singh <[email protected]> Co-authored-by: Kornel <[email protected]> Co-authored-by: Jonas Platte <[email protected]> Co-authored-by: Alex Crichton <[email protected]> Co-authored-by: Zachary S <[email protected]> Co-authored-by: Jeremy Smart <[email protected]> Co-authored-by: Ivan Tadeu Ferreira Antunes Filho <[email protected]> Co-authored-by: Alisa Sireneva <[email protected]> Co-authored-by: Trevor Gross <[email protected]> Co-authored-by: Jacob Pratt <[email protected]> Co-authored-by: Scott McMurray <[email protected]> Co-authored-by: xonx <[email protected]> Co-authored-by: Yosh <[email protected]> Co-authored-by: joboet <[email protected]> Co-authored-by: Stuart Cook <[email protected]> Co-authored-by: Connor Tsui <[email protected]> Co-authored-by: Aandreba <[email protected]> Co-authored-by: Lucas Werkmeister <[email protected]> Co-authored-by: Balt <[email protected]> Co-authored-by: Tsukasa OI <[email protected]> Co-authored-by: gitbot <git@bot> Co-authored-by: Michael Tautschnig <[email protected]> Co-authored-by: Felipe R. Monteiro <[email protected]>
The previous link for ESBMC is now dead, breaking the CI. This updates goto transcoder to use the latest version of ESBMC.
…#447) This is an automated PR to merge library subtree updates from 2025-08-01 (rust-lang/rust@adcb3d3) to 2025-08-06 (rust-lang/rust@ec7c026) (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: 7112d06 --------- Signed-off-by: Ayush Singh <[email protected]> Co-authored-by: Folkert de Vries <[email protected]> Co-authored-by: Matthias Krüger <[email protected]> Co-authored-by: Deadbeef <[email protected]> Co-authored-by: bors <[email protected]> Co-authored-by: René Kijewski <[email protected]> Co-authored-by: Nik Revenco <[email protected]> Co-authored-by: The Miri Cronjob Bot <[email protected]> Co-authored-by: Tim (Theemathas) Chirananthavat <[email protected]> Co-authored-by: Jakub Beránek <[email protected]> Co-authored-by: Chris Denton <[email protected]> Co-authored-by: Samuel Tardieu <[email protected]> Co-authored-by: Travis Cross <[email protected]> Co-authored-by: Amanieu d'Antras <[email protected]> Co-authored-by: Oli Scherer <[email protected]> Co-authored-by: David Mládek <[email protected]> Co-authored-by: SunkenPotato <[email protected]> Co-authored-by: Ralf Jung <[email protected]> Co-authored-by: Cameron Steffen <[email protected]> Co-authored-by: Martin Ombura Jr <[email protected]> Co-authored-by: Madhav Madhusoodanan <[email protected]> Co-authored-by: sayantn <[email protected]> Co-authored-by: León Orell Valerian Liehr <[email protected]> Co-authored-by: Trevor Gross <[email protected]> Co-authored-by: WANG Rui <[email protected]> Co-authored-by: Folkert de Vries <[email protected]> Co-authored-by: Luigi Sartor Piucco <[email protected]> Co-authored-by: Julien THILLARD <[email protected]> Co-authored-by: The rustc-josh-sync Cronjob Bot <[email protected]> Co-authored-by: Marijn Schouten <[email protected]> Co-authored-by: usamoi <[email protected]> Co-authored-by: Rémy Rakic <[email protected]> Co-authored-by: Alisa Sireneva <[email protected]> Co-authored-by: Josh Triplett <[email protected]> Co-authored-by: Nurzhan Sakén <[email protected]> Co-authored-by: ltdk <[email protected]> Co-authored-by: bjorn3 <[email protected]> Co-authored-by: Guillaume Gomez <[email protected]> Co-authored-by: Evgenii Zheltonozhskii <[email protected]> Co-authored-by: roblabla <[email protected]> Co-authored-by: 许杰友 Jieyou Xu (Joe) <[email protected]> Co-authored-by: Ayush Singh <[email protected]> Co-authored-by: Kornel <[email protected]> Co-authored-by: Jonas Platte <[email protected]> Co-authored-by: Alex Crichton <[email protected]> Co-authored-by: Zachary S <[email protected]> Co-authored-by: Jeremy Smart <[email protected]> Co-authored-by: Ivan Tadeu Ferreira Antunes Filho <[email protected]> Co-authored-by: okaneco <[email protected]> Co-authored-by: Trevor Gross <[email protected]> Co-authored-by: Jacob Pratt <[email protected]> Co-authored-by: Scott McMurray <[email protected]> Co-authored-by: xonx <[email protected]> Co-authored-by: Yosh <[email protected]> Co-authored-by: joboet <[email protected]> Co-authored-by: Stuart Cook <[email protected]> Co-authored-by: Connor Tsui <[email protected]> Co-authored-by: Aandreba <[email protected]> Co-authored-by: Lucas Werkmeister <[email protected]> Co-authored-by: Orson Peters <[email protected]> Co-authored-by: Balt <[email protected]> Co-authored-by: Tsukasa OI <[email protected]> Co-authored-by: Nico Lehmann <[email protected]> Co-authored-by: stifskere <[email protected]> Co-authored-by: Kivooeo <[email protected]> Co-authored-by: gitbot <git@bot> Co-authored-by: Michael Tautschnig <[email protected]> Co-authored-by: Felipe R. Monteiro <[email protected]>
This is an automated PR to update Kani metrics. The metrics have been updated by running `./scripts/run-kani.sh --run metrics`. Co-authored-by: github-merge-queue <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Resolves #ISSUE-NUMBER
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.