CBMC
process_goto_program.h File Reference
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

bool process_goto_program (goto_modelt &goto_model, const optionst &options, messaget &log)
 Common processing and simplification of goto_programts. More...
 

Function Documentation

◆ process_goto_program()

bool process_goto_program ( goto_modelt goto_model,
const optionst options,
messaget log 
)

Common processing and simplification of goto_programts.

This includes removing a number of more complex types (vectors, complex, etc.) and constructs (returns, function pointers, etc.). This is can be used after initialize_goto_model but before analysis. It is not mandatory but is used by most tools.

Definition at line 35 of file process_goto_program.cpp.