Skip to content

Issues: diffblue/cbmc

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

Clear current search query, filters, and sorts
21 Open 249 Closed
21 Open 249 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

Huge SMT file and slow proof for simple array function aws Bugs or features of importance to AWS CBMC users aws-high blocker Code Contracts Function and loop contracts
#8617 opened Apr 3, 2025 by rod-chapman
@tautschnig @remi-delmas-3000 @rod-chapman
27
Default verbosity of output when using contracts aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts
#8483 opened Oct 24, 2024 by rod-chapman
@tautschnig
3
Function --enforce-contract causes global var precondition assertion to fail Code Contracts Function and loop contracts
#8429 opened Aug 29, 2024 by BeamRaceMuppet
3
Better side-effect checks for loop contracts Code Contracts Function and loop contracts
#8393 opened Jul 22, 2024 by qinheping
@qinheping
[Safety feature] Error when enforcing contracts twice Code Contracts Function and loop contracts
#7830 opened Jul 27, 2023 by JustusAdam
DFCC loop contracts crashes with VS bug Code Contracts Function and loop contracts
#7807 opened Jul 13, 2023 by qinheping
@remi-delmas-3000 @qinheping
2
Allow function call results to be interrogated with history variables aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts
#7802 opened Jul 7, 2023 by JustusAdam
__CPROVER_old is ignored when called form a spec function aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts Kani Bugs or features of importance to Kani Rust Verifier
#7775 opened Jun 21, 2023 by JustusAdam
2
Loop assigns inference does not compute may-alias for ID_member. aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts
#7604 opened Mar 20, 2023 by qinheping
@qinheping
s2n_record_writev standalone example aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts do not merge
#7357 opened Nov 16, 2022 by nwetzler • Draft
7 tasks
@nwetzler
20
Incorrect encoding of function pointer operations in CBMC aws Bugs or features of importance to AWS CBMC users bug Code Contracts Function and loop contracts
#7213 opened Oct 5, 2022 by feliperodri
@remi-delmas-3000
4
New CBMC syntax needed for assigns clause with quantifiers aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts feature request
#7212 opened Oct 5, 2022 by feliperodri
@remi-delmas-3000 @feliperodri @qinheping
1
Implement inductive check for assigns clauses in loop contracts aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts pending merge research idea
#7208 opened Oct 5, 2022 by feliperodri
1
@qinheping
goto-instrument internal error with function pointers aws Bugs or features of importance to AWS CBMC users bug Code Contracts Function and loop contracts
#7205 opened Oct 5, 2022 by feliperodri
@remi-delmas-3000
3
Implement a vacuity check for function contracts aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts research idea
#7204 opened Oct 5, 2022 by feliperodri
@remi-delmas-3000
Support reference to prior values (was "Support the deep-copy of history variables") aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts feature request
#7203 opened Oct 5, 2022 by feliperodri
@feliperodri
3
Trace expression evaluation in ensures clauses aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts enhancement
#7202 opened Oct 5, 2022 by feliperodri
@feliperodri @markrtuttle
Allow __CPROVER_old(expr) aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts feature request
#7200 opened Oct 5, 2022 by feliperodri
@feliperodri
Find a proper way to specify pointers to static objects in contract preconditions aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts feature request
#7195 opened Oct 5, 2022 by feliperodri
@remi-delmas-3000
Document recursive functions support in contracts aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts documentation
#7188 opened Oct 5, 2022 by feliperodri
@remi-delmas-3000
2
Requires and ensures clauses with descriptions aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts enhancement
#7181 opened Sep 30, 2022 by feliperodri
@nwetzler
1
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.