Code

Lazy function loading#1563

Code

Merged

mgudemann merged 21 commits intodiffblue:developdiffblue/cbmc:developfrom

NathanJPhillips:feature/lazy-loadingNathanJPhillips/cbmc:feature/lazy-loadingCopy head branch name to clipboard

Jan 3, 2018

Commits

Commits on Dec 20, 2017

• Introduce lazy_goto_modelt

  Show description for c078858
  NathanJPhillips

  committed
  c078858

  Copy full SHA for c078858

• Make goto_convert_functions not add directly to function map

  Show description for 05a8da2
  NathanJPhillips

  committed
  05a8da2

  Copy full SHA for 05a8da2

• Allow convert_lazy_method on functions that don't have a lazy body

  Show description for 0c05be6
  NathanJPhillips

  committed
  0c05be6

  Copy full SHA for 0c05be6

• Allow post-processing functions to run on a function-by-function basis

  NathanJPhillips

  committed
  7e1ecc9

  Copy full SHA for 7e1ecc9

• Add lazy_goto_functions_mapt

  Show description for a659bc0
  NathanJPhillips

  committed
  a659bc0

  Copy full SHA for a659bc0

• Moved call to final to lazy_goto_modelt::finalize

  Show description for aa5440b
  NathanJPhillips

  committed
  aa5440b

  Copy full SHA for aa5440b

• Recreate initialize in final

  Show description for 5f06e36
  NathanJPhillips

  committed
  5f06e36

  Copy full SHA for 5f06e36

• Update load_all_functions

  Show description for 2ba1364
  NathanJPhillips

  committed
  2ba1364

  Copy full SHA for 2ba1364

• Do type-checking as a function pass

  Show description for e3e44c8
  NathanJPhillips

  committed
  e3e44c8

  Copy full SHA for e3e44c8

• Don't erase symbol in java_bytecode_convert_methodt::convert

  Show description for 87c6b28
  NathanJPhillips

  committed
  87c6b28

  Copy full SHA for 87c6b28

• Encapsulate maps in language_filest

  NathanJPhillips

  committed
  c938b08

  Copy full SHA for c938b08

• Always allow the main function not to have a body

  NathanJPhillips

  committed
  7e52e22

  Copy full SHA for 7e52e22

• Always convert the main function from bytecode into the symbol_table

  Show description for 3779782
  NathanJPhillips

  committed
  3779782

  Copy full SHA for 3779782

• Do lowering of java_new as a function-level pass

  NathanJPhillips

  committed
  166563f

  Copy full SHA for 166563f

• Fix new tests to use lazy loading

  NathanJPhillips

  committed
  cb09d8e

  Copy full SHA for cb09d8e

• Fix new test to run remove_java_new pass

  NathanJPhillips

  committed
  f759f25

  Copy full SHA for f759f25

• Reset counter used by get_fresh_aux_symbol in unit tests

  Show description for 441d269
  NathanJPhillips

  committed
  441d269

  Copy full SHA for 441d269

• Update test to handle changed symbol creation order

  Show description for ef02f4d
  NathanJPhillips

  committed
  ef02f4d

  Copy full SHA for ef02f4d

• Encapsulate lazy_goto_modelt::goto_functions

  NathanJPhillips

  committed
  b0cd57b

  Copy full SHA for b0cd57b

• Change template parameter name to not clash with existing type

  NathanJPhillips

  committed
  f96efb4

  Copy full SHA for f96efb4

• Store symbol type instead of followed type when clean casting

  Show description for a2cf16d
  NathanJPhillips

  committed
  a2cf16d

  Copy full SHA for a2cf16d