Code

Clean Const Function Pointer Removal#519

Code

Merged

kroening merged 46 commits intodiffblue:masterdiffblue/cbmc:masterfrom

thk123:feature/clean-fp-removalthk123/cbmc:feature/clean-fp-removalCopy head branch name to clipboard

Apr 4, 2017

Commits

Commits on Mar 24, 2017

• Adding tests for function pointer removal

  Show description for 89562ca
  

  thk123

  committed
  89562ca

  Copy full SHA for 89562ca

• Made remove_function_pointers inherit from messaget

  Show description for 995f504
  

  thk123

  committed
  995f504

  Copy full SHA for 995f504

• First implemention of the new approach

  

  thk123

  committed
  563a351

  Copy full SHA for 563a351

• Support for removing the typecast

  

  thk123

  committed
  3b3acd6

  Copy full SHA for 3b3acd6

• Adding support for top level pointers and typecasts

  

  thk123

  committed
  e4829eb

  Copy full SHA for e4829eb

• Fixing arrays containing null pointers

  

  thk123

  committed
  11f15ee

  Copy full SHA for 11f15ee

• Correctly deal with const structures

  

  thk123

  committed
  a479c98

  Copy full SHA for a479c98

• Fixing component access and const access

  

  thk123

  committed
  921f0b7

  Copy full SHA for 921f0b7

• Fixing todo to use separate array

  Show description for b814d65
  

  thk123

  committed
  b814d65

  Copy full SHA for b814d65

• Corrected const-ness for components

  Show description for 22ca113
  

  thk123

  committed
  22ca113

  Copy full SHA for 22ca113

• Handle failure to squash the value when getting out of an array

  

  thk123

  committed
  d87dffd

  Copy full SHA for d87dffd

• Correcting const check for pointers

  

  thk123

  committed
  f51b252

  Copy full SHA for f51b252

• Adding examples to tests of what the const prevents

  

  thk123

  committed
  1fbfbbc

  Copy full SHA for 1fbfbbc

• Corrected const check for no FP pointers

  

  thk123

  committed
  5ab672a

  Copy full SHA for 5ab672a

• Added tests to cover a couple of missed lines

  Show description for 0499b44
  

  thk123

  committed
  0499b44

  Copy full SHA for 0499b44

• Fixed issue with structs with other components

  Show description for 208ef2b
  

  thk123

  committed
  208ef2b

  Copy full SHA for 208ef2b

• Adding test for another way the previous bug could be exhibited

  

  thk123

  committed
  3da26cd

  Copy full SHA for 3da26cd

• Adding a test variation of 44 without the consts that fails correctly

  

  thk123

  committed
  eefba98

  Copy full SHA for eefba98

• Squash constant symbols first

  Show description for 132801a
  

  thk123

  committed
  132801a

  Copy full SHA for 132801a

• Fixed major bug with non const structs

  Show description for 931b239
  

  thk123

  committed
  931b239

  Copy full SHA for 931b239

• Removing redundant code

  Show description for 2e94125
  

  thk123

  committed
  2e94125

  Copy full SHA for 2e94125

• Added logging for all the ways the FP removal might not complete

  

  thk123

  committed
  63afb80

  Copy full SHA for 63afb80

• Adding consistency checks for the output

  Show description for 9da5ba2
  

  thk123

  committed
  9da5ba2

  Copy full SHA for 9da5ba2

• Adding comments to remove_const_function_pointers

  

  thk123

  committed
  d81f6cb

  Copy full SHA for d81f6cb

• Renamed all the tests

  Show description for 3e669c0
  

  thk123

  committed
  3e669c0

  Copy full SHA for 3e669c0

• Tidied up tests

  Show description for a6e71e0
  

  thk123

  authored and

  thk123

  committed
  a6e71e0

  Copy full SHA for a6e71e0

• Fixing compile errors for musketeer

  

  thk123

  authored and

  thk123

  committed
  ea5c151

  Copy full SHA for ea5c151

• Refactored resolve_index_of_function_call

  Show description for f68ff26
  

  thk123

  authored and

  thk123

  committed
  f68ff26

  Copy full SHA for f68ff26

• Split out functions from try_resolve_function_call

  

  thk123

  authored and

  thk123

  committed
  6298fea

  Copy full SHA for 6298fea

• Made the behaviour of try_resolve_function_call clearer

  Show description for 5d33d4d
  

  thk123

  authored and

  thk123

  committed
  5d33d4d

  Copy full SHA for 5d33d4d

• Split up try_resolve_expression into functions

  

  thk123

  authored and

  thk123

  committed
  a75957b

  Copy full SHA for a75957b

• Made other try_resolve*_function_call use the normal method

  

  thk123

  authored and

  thk123

  committed
  37660b1

  Copy full SHA for 37660b1

• Extracted element dealing with calling resolve on each result

  

  thk123

  authored and

  thk123

  committed
  8362233

  Copy full SHA for 8362233

• Adding the pointer check flag

  Show description for e57677e
  

  thk123

  authored and

  thk123

  committed
  e57677e

  Copy full SHA for e57677e

• Adding checks for NULL function pointers

  

  thk123

  authored and

  thk123

  committed
  0de6b17

  Copy full SHA for 0de6b17

• Renaming functions to more consistent name

  

  thk123

  authored and

  thk123

  committed
  10a08ef

  Copy full SHA for 10a08ef

• Swap to using an unorded set

  Show description for cf6a49a
  

  thk123

  authored and

  thk123

  committed
  cf6a49a

  Copy full SHA for cf6a49a

• Added flag for goto-instrument to just remove const function pointers

  Show description for db11c31
  

  thk123

  authored and

  thk123

  committed
  db11c31

  Copy full SHA for db11c31

• Check the GOTO program for loss of const

  Show description for 052da5a
  

  thk123

  authored and

  thk123

  committed
  052da5a

  Copy full SHA for 052da5a

• Added a couple of missed test cases.

  Show description for 6ba0469
  

  thk123

  authored and

  thk123

  committed
  6ba0469

  Copy full SHA for 6ba0469

• Fixing tests to work with new test.pl

  Show description for 18b5907
  

  thk123

  authored and

  thk123

  committed
  18b5907

  Copy full SHA for 18b5907

• Fixing missing new lines

  

  thk123

  authored and

  thk123

  committed
  2538f4f

  Copy full SHA for 2538f4f

• Split out the const check into own analysis

  Show description for 29e7e0d
  

  thk123

  committed
  29e7e0d

  Copy full SHA for 29e7e0d

• Descend all children of the same base type

  Show description for 649e0bf
  

  thk123

  committed
  649e0bf

  Copy full SHA for 649e0bf

• PR Feedback implementation

  Show description for 4607e73
  

  thk123

  committed
  4607e73

  Copy full SHA for 4607e73

• Use pointers in is_type_at_least_as_const_as

  Show description for d7c15ae
  

  thk123

  committed
  d7c15ae

  Copy full SHA for d7c15ae