-
Notifications
You must be signed in to change notification settings - Fork 284
Pull requests: diffblue/cbmc
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
[RFC] Make conversion failures in the propositional back-end fatal [depends-on: #6914, #6915]
dependent - do not merge
RFC
Request for comment
#6655
opened Feb 9, 2022 by
tautschnig
•
Draft
2 of 4 tasks
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
C library: atexit
C Front End
Needs rebase
#6604
opened Jan 21, 2022 by
tautschnig
•
Draft
3 tasks done
Move rounding_mode_identifier() to configt
cleanup
#6555
opened Dec 31, 2021 by
tautschnig
Loading…
2 of 3 tasks
goto-contracts: Separate front-end for contracts
do not review
#6526
opened Dec 9, 2021 by
tautschnig
•
Draft
7 tasks
local_bitvector_analysist: track whether an object may be alive
#6525
opened Dec 9, 2021 by
tautschnig
•
Draft
2 of 4 tasks
Byte extract lowering: support extracting non-byte-aligned arrays
blocker
#6488
opened Nov 29, 2021 by
tautschnig
Loading…
3 tasks done
expand value_sett::apply_code_rec
cleanup
#6446
opened Nov 8, 2021 by
kroening
Loading…
2 of 3 tasks
goto-symex: expand unknown points-to values to all objects
#6442
opened Nov 5, 2021 by
tautschnig
•
Draft
2 of 5 tasks
__CPROVER_r/w_ok does not require null or a valid pointer
aws
Bugs or features of importance to AWS CBMC users
#6416
opened Oct 26, 2021 by
kroening
Loading…
3 of 4 tasks
is_invalid_pointer is now defined as a bi-implication
aws
Bugs or features of importance to AWS CBMC users
do not merge
#6366
opened Sep 25, 2021 by
kroening
Loading…
2 of 3 tasks
remove encoding of arrays of bools into bitvector
SMT Backend Interface
#6206
opened Jun 28, 2021 by
kroening
Loading…
2 of 4 tasks
[RFC] Two new failing tests demonstrating updates outside member bounds
RFC
Request for comment
Tests
#6101
opened May 10, 2021 by
tautschnig
•
Draft
3 tasks done
Value set dereferencing: do not treat struct prefixes as equal
#5876
opened Mar 1, 2021 by
tautschnig
Loading…
3 tasks done
Message handler: add quote_begin, quote_end commands
#5696
opened Dec 25, 2020 by
tautschnig
Loading…
2 of 3 tasks
Rework memory allocation failure checks and options
#5401
opened Jun 30, 2020 by
danpoe
Loading…
4 of 5 tasks
Specify exactly what the comment at the top of the file should be
#5394
opened Jun 25, 2020 by
thk123
Loading…
3 tasks done
ProTip!
Updated in the last three days: updated:>2025-12-18.