Fix up symbol naming checks so --validate-goto-model can be enabled in regression testing.#3767

Merged

chrisr-diffblue merged 11 commits intodiffblue:developfrom chrisr-diffblue:validate_goto_programs_symbol_check_fixup

Jan 28, 2019

+170-39

Commits on Jan 28, 2019

Fix base_name of return' symbol to match its name
chrisr-diffblue
committed
Fix base_name of argc' symbol to match its name
chrisr-diffblue
committed
Ensure the gcc_builtin_va_arg symbol has a mode
chrisr-diffblue
committed
Make #anon symbols have consistent naming between base_name and name
chrisr-diffblue
committed
Ensure the '$exception_flag' symbol has a valid mode
chrisr-diffblue
committed
Refine symbol well-formedness checks to handle special cases
chrisr-diffblue
committed
Correct validation check for return statements from void functions
chrisr-diffblue
committed
Correct symbol table type check in cases where return removal has modified types
chrisr-diffblue
committed
Make goto_programt::instructiont::validate() accept incomplete array types
chrisr-diffblue
committed
Make goto_programt::instructiont::validate() accept differing return types
chrisr-diffblue
committed
enable --validate-goto-model for all cbmc regressions

Daniel Kroening
authored and
chrisr-diffblue
committed