Skip to content
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

Proof Slicing: make dependency tracking optional #3309

Merged
merged 7 commits into from Oct 25, 2023

Conversation

FliegendeWurst
Copy link
Member

@FliegendeWurst FliegendeWurst commented Oct 20, 2023

Fixes #3301 by adding an option to disable the dependency tracker and adding a way to create the dependency graph after the proof is done.

cc @unp1

@FliegendeWurst FliegendeWurst added the keyext.slicing Module: keyext.slicing label Oct 20, 2023
@codecov
Copy link

codecov bot commented Oct 20, 2023

Codecov Report

Merging #3309 (2be318e) into main (099d076) will decrease coverage by 0.01%.
The diff coverage is 28.57%.

❗ Current head 2be318e differs from pull request most recent head 5d76195. Consider uploading reports for the commit 5d76195 to get more accurate results

@@             Coverage Diff              @@
##               main    #3309      +/-   ##
============================================
- Coverage     37.79%   37.79%   -0.01%     
- Complexity    16844    16857      +13     
============================================
  Files          2051     2052       +1     
  Lines        125329   125566     +237     
  Branches      21190    21249      +59     
============================================
+ Hits          47370    47456      +86     
- Misses        72121    72272     +151     
  Partials       5838     5838              
Files Coverage Δ
...ore/src/main/java/de/uka/ilkd/key/rule/Taclet.java 77.96% <ø> (+1.84%) ⬆️
...y_project/slicing/analysis/DependencyAnalyzer.java 85.24% <100.00%> (+0.04%) ⬆️
...core/src/main/java/de/uka/ilkd/key/proof/Node.java 70.28% <0.00%> (-0.26%) ⬇️
.../java/org/key_project/slicing/SlicingSettings.java 38.46% <60.00%> (+5.12%) ⬆️
...e/src/main/java/de/uka/ilkd/key/logic/Sequent.java 62.30% <62.50%> (+0.40%) ⬆️
...core/src/main/java/de/uka/ilkd/key/proof/Goal.java 75.20% <50.00%> (+<0.01%) ⬆️
...g/key_project/slicing/SlicingSettingsProvider.java 10.71% <0.00%> (-1.79%) ⬇️
...org/key_project/slicing/graph/DependencyGraph.java 57.14% <54.54%> (-0.33%) ⬇️
...ava/org/key_project/slicing/DependencyTracker.java 54.54% <17.39%> (-28.41%) ⬇️

... and 87 files with indirect coverage changes

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

@github-actions
Copy link

github-actions bot commented Oct 20, 2023

Thank you for your contribution.

The test artifacts are available on Artiweb.
The newest artifact is here.

@unp1 unp1 self-requested a review October 20, 2023 16:26
... if the dependency tracker isn't always on
Copy link
Member

@unp1 unp1 left a comment

Choose a reason for hiding this comment

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

Thanks a lot for your effort. Please find some remarks that are hopefully useful.

Copy link
Member

@unp1 unp1 left a comment

Choose a reason for hiding this comment

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

Thanks!

@unp1 unp1 added this pull request to the merge queue Oct 25, 2023
Merged via the queue into KeYProject:main with commit 043c97c Oct 25, 2023
12 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
keyext.slicing Module: keyext.slicing Robustness
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Proof Slicer always active
2 participants