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
7 Open 475 Closed
7 Open 475 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
CBMC wavefront does not terminate on simple decreases clause in loop aws Bugs or features of importance to AWS CBMC users blocker bug
#8301 opened May 21, 2024 by rod-chapman
@remi-delmas-3000 @qinheping
8
New option --mmio-regions to specify memory regions aws Bugs or features of importance to AWS CBMC users blocker Kani Bugs or features of importance to Kani Rust Verifier Property Instrumentation Version 7
#6747 opened Mar 23, 2022 by tautschnig Loading…
3 of 5 tasks
@tautschnig
11
goto_check_c: observe check pragmas annotated to individual expressions aws Bugs or features of importance to AWS CBMC users blocker bugfix Kani Bugs or features of importance to Kani Rust Verifier Property Instrumentation
#6616 opened Jan 30, 2022 by tautschnig Loading…
2 of 3 tasks
1
@tautschnig
3
Byte extract lowering: support extracting non-byte-aligned arrays blocker
#6488 opened Nov 29, 2021 by tautschnig Loading…
3 tasks done
@tautschnig @kroening @peterschrammel
7
label_properties: do not rely on source_locationt's get_function() blocker
#4131 opened Feb 8, 2019 by tautschnig Loading…
3 of 4 tasks
@tautschnig @kroening
@remi-delmas-3000 @peterschrammel
22
Consistently use unsigned/size_t in big-int [blocks: #2310] blocker cleanup
#2452 opened Jun 25, 2018 by tautschnig Loading…
@kroening
10
ProTip! Follow long discussions with comments:>50.