Skip to content

Issues: creusot-rs/creusot

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

110 Open 345 Closed
110 Open 345 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Erasing ghost/snapshot code is unsound soundness Enhance soundness
#1455 opened Mar 24, 2025 by arnaudgolfouse
1
Make contract inference work with simple functions
#1453 opened Mar 20, 2025 by xldenis
2
postcondition and precondition don't work with function pointers easy enhancement New feature or request known-fix Issue for which we know a fix, that we "just" need to implement.
#1452 opened Mar 20, 2025 by xldenis
1
Handle missing things in creusot-contracts more gracefully cargo-creusot Issue is related to the `cargo-creusot` and more generally the porcelain around creusot enhancement New feature or request error-messages Improve error messages toolchain Installation, distribution, dependencies
#1447 opened Mar 19, 2025 by Lysxia
cargo creusot prove takes too long when iterating on failed goals.
#1446 opened Mar 19, 2025 by xldenis
Postconditions generated for closure specifications do not verify the axiom they should verify bug Something isn't working high-priority Given a high priority known-fix Issue for which we know a fix, that we "just" need to implement. soundness Enhance soundness
#1445 opened Mar 18, 2025 by jhjourdan
Match with no branches in pearlite crash Creusot crashes with a panic and dumps a stack trace easy low-priority Given a low priority pearlite Improve pearlite
#1439 opened Mar 13, 2025 by arnaudgolfouse
1
Wrong instantiation in the termination check bug Something isn't working crash Creusot crashes with a panic and dumps a stack trace
#1438 opened Mar 13, 2025 by arnaudgolfouse
1
How to specify a crate without verify it? enhancement New feature or request low-priority Given a low priority
#1427 opened Mar 11, 2025 by Halbaroth
12
Spans for invariants that are block expressions (for let bindings) are a little wrong low-priority Given a low priority
#1426 opened Mar 11, 2025 by Lysxia
Should we leverage the local variable mutability?
#1415 opened Mar 4, 2025 by jhjourdan
Provide a cargo creusot command to update a project cargo-creusot Issue is related to the `cargo-creusot` and more generally the porcelain around creusot toolchain Installation, distribution, dependencies
#1409 opened Mar 3, 2025 by ia0
1
Add a list of supported/unsupported Rust features doc Improve documentation
#1401 opened Mar 3, 2025 by Halbaroth
3
The constant prophecy analysis fails when a borrow is captured by a closure enhancement New feature or request low-priority Given a low priority
#1398 opened Mar 2, 2025 by jhjourdan
We need a proper error message when old is applied to something which is not a variable bug Something isn't working error-messages Improve error messages
#1397 opened Mar 2, 2025 by jhjourdan
The old keyword seems to re-enables borrow checking bug Something isn't working pearlite Improve pearlite
#1396 opened Mar 2, 2025 by jhjourdan
Build Why3 with Coq support toolchain Installation, distribution, dependencies
#1393 opened Mar 2, 2025 by suhr
13
Support for unsafe operations that Creusot can support enhancement New feature or request
#1379 opened Feb 25, 2025 by ia0
12
Better support for sequences enhancement New feature or request
#1363 opened Feb 17, 2025 by jhjourdan
Bitwise : add support for bitwise shifts and negation in pearlite easy enhancement New feature or request pearlite Improve pearlite
#1360 opened Feb 17, 2025 by jhjourdan
install: Don't overwrite IDE settings in why3.conf cargo-creusot Issue is related to the `cargo-creusot` and more generally the porcelain around creusot enhancement New feature or request
#1349 opened Feb 7, 2025 by Lysxia
Make --test why3 display why3find status internal Improve build-from-source and test-suite
#1347 opened Feb 7, 2025 by Lysxia
"intro" combinator for universal quantifiers enhancement New feature or request
#1343 opened Feb 5, 2025 by Lysxia
3
#[open] functions and termination enhancement New feature or request
#1338 opened Feb 3, 2025 by arnaudgolfouse
1
Debug implementation causes Creusot ICE bug Something isn't working
#1337 opened Feb 2, 2025 by xldenis
6
ProTip! What’s not been updated in a month: updated:<2025-02-27.