Skip to content

Add support for exporting function pointer targets at all callsites. #5289

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.

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

Closed

Conversation

NlightNFotis
Copy link
Contributor

@NlightNFotis NlightNFotis commented Apr 8, 2020

This adds an extra flag to goto-analyzer that allows it to write function pointer targets for all call sites in a json format, like this:

{
  "use_f.function_pointer_call.1": [ "f", "h", "g" ]
}

IMPORTANT: This PR's contributions is the two last commits.

  • 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.

owen-mc-diffblue and others added 30 commits March 24, 2020 15:53
as a new abstract object.
There is no value in wrapping an object with no additional information,
and there is currently some problems with wrapping
There is currently some inconsistency between how the value set and the
interval domains handle wrapping. Specifically, the value set returns an
unwrapped object when eval'd, whereas the interval domain returns a
wrapped object. Since the rest of the code is compatible with the
interval suggestion, we temporarily disable wrapping if using value set
The variable sensitivity domain is always on, if we're using the
variable sensitivity domain object factory
Use from_expr instead of constant_expr::get_value() so we don't print hex values
for the new value-set abstraction.
for the new value-set abstraction.
It was written in 2017 but was #if 0-ed out, so it needs to be updated to compile now.
ADA-496 has been filed to fix this test up and reintroduce it.
This adds a new option, --restrict-function-pointer, to goto-instrument. This
lets a user specify a list of possible pointer targets for specific function
pointer call sites, rather than have remove_function_pointers guess possible
values. The intended purpose behind this is to prevent excessive symex time
wasted on exploring paths the user knows the program can never actually take.
Add --get-fp-values option to goto-analyzer for all
callsites in json format to be fed to goto-instrument.
@hannes-steffenhagen-diffblue
Copy link
Contributor

Please only review be933ca, the rest are from other PRs and will probably go away/change anyway.

Copy link
Contributor

@danpoe danpoe left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Only reviewed commit be933ca which looks good. Are there any tests yet for the feature? Please also add the label dependent - do not merge and mention the PR it depends on in the title.

Co-authored-by: hannes-steffenhagen-diffblue <[email protected]>
@NlightNFotis
Copy link
Contributor Author

NlightNFotis commented Jun 11, 2020

This was implemented in #5300, #5309 and #5311.

@NlightNFotis NlightNFotis deleted the ada-482 branch October 20, 2020 15:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants