Skip to content

Refactor/move abstract interpreter functionality into goto analyzer 1 #7120

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

Open
wants to merge 4 commits into
base: develop
Choose a base branch
from

Conversation

martin-cs
Copy link
Collaborator

The first part of moving functionality that is basically "run the abstract interpreter and then ..." from goto-instrument to goto-analyzer. I'm doing this to remove duplication of functionality, add configurability (the options on goto-analyzer are not completely orthogonal but they are a lot better than at the moment), add testing and to try to slim down goto-instrument so that it is a bit more closer to it's original intent of performing goto-model to goto-model transformations. Please say if you disagree with this as a line of refactoring.

This will also provide a more radical alternative than #7111 to resolving some of the issues with #7041.

martin added 4 commits September 11, 2022 12:26
It is already supported, tested and documented so this is straight-forward.
The biggest change is migrating and updating tests.
There is not much to do as this is already supported, tested and documented
in goto-analyzer and there are no tests for this in goto-instrument.
The functionality is already present and tested so there is not much to do.
@codecov
Copy link

codecov bot commented Sep 11, 2022

Codecov Report

Merging #7120 (ffb9246) into develop (8b7b7a9) will decrease coverage by 0.04%.
The diff coverage is 32.00%.

@@             Coverage Diff             @@
##           develop    #7120      +/-   ##
===========================================
- Coverage    77.92%   77.87%   -0.05%     
===========================================
  Files         1576     1576              
  Lines       181645   181643       -2     
===========================================
- Hits        141541   141458      -83     
- Misses       40104    40185      +81     
Impacted Files Coverage Δ
src/goto-analyzer/goto_analyzer_parse_options.cpp 71.42% <0.00%> (-0.85%) ⬇️
.../goto-instrument/goto_instrument_parse_options.cpp 70.32% <0.00%> (-0.76%) ⬇️
...rc/goto-instrument/goto_instrument_parse_options.h 100.00% <ø> (ø)
src/solvers/lowering/byte_operators.cpp 92.60% <ø> (ø)
src/solvers/prop/bdd_expr.cpp 93.02% <ø> (ø)
src/util/pointer_expr.h 88.23% <ø> (ø)
src/solvers/smt2/smt2_conv.cpp 68.69% <88.88%> (+0.03%) ⬆️
src/analyses/constant_propagator.h 66.66% <0.00%> (-15.69%) ⬇️
src/analyses/constant_propagator.cpp 83.17% <0.00%> (-12.30%) ⬇️
src/util/graph.h 88.92% <0.00%> (-7.92%) ⬇️
... and 2 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

@tautschnig tautschnig self-assigned this Sep 17, 2022
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

THANK YOU for this cleanup!!! Would you mind also updating the man page to reflect these changes?

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.

4 participants