Refactor process_goto_program so that all tools use common processing code#5807

Merged

tautschnig merged 21 commits intodiffblue:developfrom

martin-cs:refactor/process_goto_program

Feb 23, 2021

Commits on Feb 22, 2021

Create a stub for a common process_goto_program
martin
committed
Add remove_asm to goto-analyzer to make program processing more consistent
martin
committed
Enable the CPROVER library for goto-analyzer
martin
committed
Add 'malloc may fail' initialization to goto-diff
martin
committed
Add string abstraction to goto-analyzer and goto-diff
martin
committed
Replace the use of cmdline with options in goto-analyzer and goto-diff
martin
committed
Replace the parsing of goto_check options with the appropriate macro
martin
committed
Add memory mapped IO support to goto-analyzer
martin
committed
Add partial inlining as an optional part of process_goto_program
martin
committed
Make the call to rewrite-union configurable
martin
committed
Add options that goto-check uses to the macros
martin
committed
Enable goto_check in goto-analyzer
martin
committed
goto-analyzer now adds the rounding mode to floating-point operations
martin
committed
More string abstraction to be common processing of goto-programs
martin
committed
Move the update functions earlier so that they are common between tools
martin
committed
Change the text of the logging message so that it is the same as CBMC
martin
committed
Move the majority of process_goto_program out of the individual tools
martin
committed
Fix up the doxygen warnings
martin
committed
Fix unit test that uses some, but not all, of CBMC's option parsing
martin
committed
Enabling goto_check in goto-analyzer adds 7 instructions to the test
martin
committed
Fix typo in comments

martin-cs
and
peterschrammel
authored

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refactor process_goto_program so that all tools use common processing code#5807

Commits on Feb 22, 2021

Create a stub for a common process_goto_program

Add remove_asm to goto-analyzer to make program processing more consistent

Enable the CPROVER library for goto-analyzer

Add 'malloc may fail' initialization to goto-diff

Add string abstraction to goto-analyzer and goto-diff

Replace the use of cmdline with options in goto-analyzer and goto-diff

Replace the parsing of goto_check options with the appropriate macro

Add memory mapped IO support to goto-analyzer

Add partial inlining as an optional part of process_goto_program

Make the call to rewrite-union configurable

Add options that goto-check uses to the macros

Enable goto_check in goto-analyzer

goto-analyzer now adds the rounding mode to floating-point operations

More string abstraction to be common processing of goto-programs

Move the update functions earlier so that they are common between tools

Change the text of the logging message so that it is the same as CBMC

Move the majority of process_goto_program out of the individual tools

Fix up the doxygen warnings

Fix unit test that uses some, but not all, of CBMC's option parsing

Enabling goto_check in goto-analyzer adds 7 instructions to the test

Fix typo in comments