Handle empty type in incremental SMT2 decision procedure#8907
Draft
tautschnig wants to merge 1 commit intodiffblue:developfrom
Draft
Handle empty type in incremental SMT2 decision procedure#8907tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig wants to merge 1 commit intodiffblue:developfrom
Conversation
Skip symbols and nondet symbols with empty_typet (void) in gather_dependent_expressions to avoid attempting SMT sort conversion. Add early return in send_function_definition for empty-typed expressions as a defensive measure. Handle equality over empty type in set_to by treating it as vacuously true, matching the behavior of the non-incremental SMT2 backend. Remove no-new-smt exclusion tag from havoc_slice_checks and memset_null regression tests since they now pass with the incremental SMT2 backend. Fixes: diffblue#8077
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8907 +/- ##
========================================
Coverage 80.41% 80.41%
========================================
Files 1703 1703
Lines 188398 188407 +9
Branches 73 73
========================================
+ Hits 151496 151506 +10
+ Misses 36902 36901 -1 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Skip symbols and nondet symbols with empty_typet (void) in gather_dependent_expressions to avoid attempting SMT sort conversion. Add early return in send_function_definition for empty-typed expressions as a defensive measure. Handle equality over empty type in set_to by treating it as vacuously true, matching the behavior of the non-incremental SMT2 backend.
Remove no-new-smt exclusion tag from havoc_slice_checks and memset_null regression tests since they now pass with the incremental SMT2 backend.
Fixes: #8077