Code

Filter value sets in symex#4288

Code

Merged

owen-mc-diffblue merged 18 commits intodiffblue:developdiffblue/cbmc:developfrom

owen-mc-diffblue:owen/symex-filter-value-setsowen-mc-diffblue/cbmc:owen/symex-filter-value-setsCopy head branch name to clipboard

Mar 26, 2019

Commits

Commits on Mar 26, 2019

• Move apply_condition from symex_assume_l2 to symex_assume

  Show description for 7713e8a
  

  Owen

  committed
  7713e8a

  Copy full SHA for 7713e8a

• Move apply_goto_condition into goto_symext

  Show description for 94b71ea
  

  Owen

  committed
  94b71ea

  Copy full SHA for 94b71ea

• Pass original guard to apply_goto_condition

  Show description for d4f0d94
  

  Owen

  committed
  d4f0d94

  Copy full SHA for d4f0d94

• Make non-const version of find_entry

  

  Owen

  committed
  4e0ba71

  Copy full SHA for 4e0ba71

• Factor out value_sett::get_entry_for_symbol

  Show description for 0e8bb88
  

  Owen

  committed
  0e8bb88

  Copy full SHA for 0e8bb88

• filter value sets at gotos and assumes

  Show description for 24925b6
  

  Owen

  committed
  24925b6

  Copy full SHA for 24925b6

• Try to speed up try_filter_value_sets

  Show description for 1859818
  

  Owen

  committed
  1859818

  Copy full SHA for 1859818

• Update tests for symex excluding null pointers

  Show description for 5baedb2
  

  Owen

  committed
  5baedb2

  Copy full SHA for 5baedb2

• Create paths-lifo-expected-failure tag for tests

  Show description for d9ad548
  

  Owen

  committed
  d9ad548

  Copy full SHA for d9ad548

• Refactor value_set_dereferencet

  Show description for ffafa86
  

  Owen

  committed
  ffafa86

  Copy full SHA for ffafa86

• Use build_reference_to when filtering value sets

  

  Owen

  committed
  a555406

  Copy full SHA for a555406

• Move pointer_offset_sum

  Show description for c361ff7
  

  Owen

  committed
  c361ff7

  Copy full SHA for c361ff7

• Fix bug in simplify_dereference_rec

  Show description for f3c31ff
  

  Owen

  committed
  f3c31ff

  Copy full SHA for f3c31ff

• Skip unknown elements in value set

  Show description for 7e3ca83
  

  Owen

  committed
  7e3ca83

  Copy full SHA for 7e3ca83

• Add tests for symex value-set filtering

  

  Owen

  committed
  805a409

  Copy full SHA for 805a409

• Add tests for value-set filtering for virtual method calls

  Show description for 6d9d1f8
  

  Owen

  committed
  6d9d1f8

  Copy full SHA for 6d9d1f8

• Speed up erasing from value sets

  

  Owen

  committed
  692eaa1

  Copy full SHA for 692eaa1

• Remove const-cast from value_sett::get_entry

  

  smowton

  authored and

  Owen

  committed
  0544470

  Copy full SHA for 0544470