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
15 Open 915 Closed
15 Open 915 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

Field sensitivity: account for array size in all index expressions bugfix Kani Bugs or features of importance to Kani Rust Verifier
#8579 opened Feb 3, 2025 by tautschnig Loading…
3 tasks done
@kroening @peterschrammel
1
goto-symex: assumed pointer equalities must update value set bugfix Symbolic Execution
#8494 opened Nov 4, 2024 by tautschnig Loading…
3 of 4 tasks
1
3
goto-symex: move level1 map to goto_statet bugfix Symbolic Execution
#8439 opened Sep 3, 2024 by tautschnig Loading…
3 tasks done
1
@tautschnig
Support comparing arrays of non-constant size with array_equal aws-high bugfix Symbolic Execution
#8208 opened Feb 16, 2024 by tautschnig Loading…
3 tasks done
1
@tautschnig @kroening @peterschrammel
3
Cleanup fmod vs IEEE remainder aws Bugs or features of importance to AWS CBMC users bugfix Kani Bugs or features of importance to Kani Rust Verifier
#7885 opened Sep 12, 2023 by tautschnig • Draft
4 tasks done
@tautschnig @martin-cs
1
Use extractbits to extract non-byte-fields from unions bugfix
#7861 opened Aug 21, 2023 by tautschnig • Draft
3 tasks done
@tautschnig
Variadic args/va_arg: handle unexpected va_list types bugfix
#7711 opened May 15, 2023 by tautschnig Loading…
3 tasks done
1
@kroening @peterschrammel
1
C front-end: ensure array type updates are consistent bugfix C Front End
#7610 opened Mar 22, 2023 by tautschnig Loading…
3 tasks done
1
@kroening
1
Linking: fix up all types before handling functions or objects aws Bugs or features of importance to AWS CBMC users bugfix
#7579 opened Mar 7, 2023 by tautschnig Loading…
2 of 3 tasks
@kroening
4
Expanding __CPROVER_{r,w,rw}_ok must not introduce overflow [depends-on: #6616] aws Bugs or features of importance to AWS CBMC users bugfix dependent - do not merge Property Instrumentation
#6656 opened Feb 10, 2022 by tautschnig Loading…
3 tasks done
@tautschnig
7
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
gen_nondet_array_init: arrays may have size 0 bugfix C Front End
#5342 opened May 13, 2020 by kroening Loading…
2 of 4 tasks
@kroening
4
Patch goto-analyzer reachable-functions json and xml output. bugfix
#4947 opened Jul 24, 2019 by markrtuttle Loading…
2 tasks
@markrtuttle
4
Stop asserting positive array size bugfix
#4928 opened Jul 19, 2019 by xbauch Loading…
4 of 7 tasks
@kroening
18
Fix various type conversion and deprecation warnings reported by Visual studio bugfix cleanup dependent - do not merge
#2310 opened Jun 7, 2018 by tautschnig • Draft
@tautschnig
18
ProTip! no:milestone will show everything without a milestone.