Code

C Support Changes#581

Code

Merged

peterschrammel merged 11 commits intodiffblue:test-gen-supportdiffblue/cbmc:test-gen-supportfrom thk123:feature/c-support-changesthk123/cbmc:feature/c-support-changesCopy head branch name to clipboardMar 10, 2017

+299-17

Commits

Commits on Mar 6, 2017

• Generate stub method for opaque functions

  Show description for 03a4213
  

  thk123

  committed
  03a4213

  Copy full SHA for 03a4213

• Don't create stub for CPROVER_ functions

  Show description for 06b36cd
  

  thk123

  committed
  06b36cd

  Copy full SHA for 06b36cd

• Create stub argument identifiers for functions with parameters

  Show description for 4b6e9c9
  

  thk123

  committed
  4b6e9c9

  Copy full SHA for 4b6e9c9

• Pass the whole parameter in when generating the symbol

  Show description for ddd2cae
  

  thk123

  committed
  ddd2cae

  Copy full SHA for ddd2cae

• Refactored method for generating return symbol name to languaget

  Show description for b12d2e7
  

  thk123

  committed
  b12d2e7

  Copy full SHA for b12d2e7

• Added a flag for enabling opaque method stubs

  Show description for 13038bf
  

  thk123

  committed
  13038bf

  Copy full SHA for 13038bf

• Use the system_library_symbols when generating stubs

  Show description for f9bfbbe
  

  thk123

  committed
  f9bfbbe

  Copy full SHA for f9bfbbe

• Added comment explaining the type of symbols we aren't stubbing

  

  thk123

  committed
  473dc89

  Copy full SHA for 473dc89

• Adding simple regression for struct function

  Show description for 519e08b
  

  thk123

  committed
  519e08b

  Copy full SHA for 519e08b

• Use the symbol in expr2c

  

  thk123

  committed
  0e755e6

  Copy full SHA for 0e755e6

Commits on Mar 10, 2017

• Call the generate_opqaue_stubs from final

  Show description for 8f68c25
  

  thk123

  committed
  8f68c25

  Copy full SHA for 8f68c25