Skip to content

Take libraries out of test coverage #259

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
peterschrammel opened this issue Oct 19, 2016 · 4 comments
Closed

Take libraries out of test coverage #259

peterschrammel opened this issue Oct 19, 2016 · 4 comments

Comments

@peterschrammel
Copy link
Member

@kroening, is this about built-ins or user-specified libraries?

@kroening
Copy link
Member

built-ins

@peterschrammel peterschrammel self-assigned this Oct 19, 2016
@peterschrammel
Copy link
Member Author

The problem is a combination of the following:

  1. partial inlining is done before instrumenting coverage goals
  2. goto_inline tries to replace the source locations of hidden functions (i.e. built-ins) (not quite -- because it seems that locations are re-introduced through remove_returns -- I haven't investigated that further)
  3. instrument_cover_goals is unable to know where the inlined code came from

@kroening, is there any reason why 2. is necessary?

@kroening
Copy link
Member

kroening commented Nov 1, 2016

2: To hide them -- in particular, the goal is to have assertions appear in the place where the function is called.

@peterschrammel
Copy link
Member Author

peterschrammel commented Nov 1, 2016

Ok. Then I use ID_hide (already set in goto_inline) to identify code from built-ins.

peterschrammel added a commit to peterschrammel/cbmc that referenced this issue Apr 8, 2017
smowton added a commit to smowton/cbmc that referenced this issue May 9, 2018
…_callsite_specialiser

Add CSVSA and its specializer
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants