Skip to content

Filter value sets in symex #4288

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.

Sign up for GitHub

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

Merged
merged 18 commits into from
Mar 26, 2019
Merged

Filter value sets in symex #4288

Changes from 1 commit
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
7713e8a
Move apply_condition from symex_assume_l2 to symex_assume
Mar 21, 2019
94b71ea
Move apply_goto_condition into goto_symext
Mar 21, 2019
d4f0d94
Pass original guard to apply_goto_condition
Mar 21, 2019
4e0ba71
Make non-const version of find_entry
Mar 25, 2019
0e8bb88
Factor out value_sett::get_entry_for_symbol
Mar 25, 2019
24925b6
filter value sets at gotos and assumes
Mar 25, 2019
1859818
Try to speed up try_filter_value_sets
Mar 21, 2019
5baedb2
Update tests for symex excluding null pointers
Mar 21, 2019
d9ad548
Create paths-lifo-expected-failure tag for tests
Mar 21, 2019
ffafa86
Refactor value_set_dereferencet
Mar 21, 2019
a555406
Use build_reference_to when filtering value sets
Mar 21, 2019
c361ff7
Move pointer_offset_sum
Mar 21, 2019
f3c31ff
Fix bug in simplify_dereference_rec
Mar 21, 2019
7e3ca83
Skip unknown elements in value set
Mar 21, 2019
805a409
Add tests for symex value-set filtering
Mar 21, 2019
6d9d1f8
Add tests for value-set filtering for virtual method calls
Mar 21, 2019
692eaa1
Speed up erasing from value sets
Mar 26, 2019
0544470
Remove const-cast from value_sett::get_entry
smowton Mar 26, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Skip unknown elements in value set 
We should try to filter them out
  • Loading branch information
Owen committed Mar 26, 2019
commit 7e3ca83d9a7f25586231b984ac6f8f368cfa22a3
5 changes: 5 additions & 0 deletions src/goto-symex/symex_main.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -617,6 +617,11 @@ void goto_symext::try_filter_value_sets(
// used if the condition is false, and vice versa.
for(const auto &value_set_element : value_set_elements)
{
if(value_set_element.id() == ID_unknown)
{
continue;
}

const bool exclude_null_derefs = false;
value_set_dereferencet::valuet possible_value =
value_set_dereferencet::build_reference_to(
Expand Down