Skip to content

Add support for null pointer and address of expression conversion in incremental SMT2 backend. #6781

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

Jump to bottom
Merged
merged 7 commits into from
Apr 9, 2022
Merged

Add support for null pointer and address of expression conversion in incremental SMT2 backend. #6781

merged 7 commits into from
Apr 9, 2022

Conversation

thomasspriggs
Copy link
Contributor

This PR adds support for null pointer and address of expression to SMT term conversion in the incremental SMT2 back end.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@thomasspriggs
Add conversion of null pointer to smt terms
4879051
@thomasspriggs
Add object tracking
79766cb
@thomasspriggs
Extend unit test of extract_bits conversion with integer bounds
3a353a6 
Because instances of this expression are constructed using integer
bounds rather than bit vector bounds, as part of the left shift overflow
checks.
@thomasspriggs thomasspriggs force-pushed the tas/smt_address_of branch 2 times, most recently from eb3f69e to 62c108b Compare April 8, 2022 10:20
@thomasspriggs
Add support for converting integer constants into bit vectors
a0f253e 
This is required for the following refactor because it requires all
sub-expressions to be convertible to smt terms whereas the current
implementation only requires sub expressions which are recursed into to
be convertible. These integer constants which need converting can be
found as sub expressions of extract bits expressions.
@thomasspriggs
Refactor expr to smt term conversion to be non-recursive
eb2070a
@thomasspriggs
Add conversion of address_of(symbol) to SMT terms
908d76e
@thomasspriggs
Add incremental smt2 with null pointers regression test
41629be
@thomasspriggs thomasspriggs merged commit 89ca306 into diffblue:develop Apr 9, 2022
@thomasspriggs thomasspriggs deleted the tas/smt_address_of branch April 11, 2022 13:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@NlightNFotis NlightNFotis NlightNFotis approved these changes

@TGWDB TGWDB TGWDB approved these changes

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@tautschnig tautschnig Awaiting requested review from tautschnig tautschnig is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@chris-ryder chris-ryder Awaiting requested review from chris-ryder

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@thomasspriggs @NlightNFotis @TGWDB