process_goto_program.cpp File Reference

Get a Goto Program. More...

#include "process_goto_program.h"
#include <util/message.h>
#include <util/options.h>
#include <goto-programs/adjust_float_expressions.h>
#include <goto-programs/goto_inline.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/instrument_preconditions.h>
#include <goto-programs/mm_io.h>
#include <goto-programs/remove_complex.h>
#include <goto-programs/remove_function_pointers.h>
#include <goto-programs/remove_returns.h>
#include <goto-programs/remove_vector.h>
#include <goto-programs/rewrite_rw_ok.h>
#include <goto-programs/rewrite_union.h>
#include <goto-programs/string_abstraction.h>
#include <ansi-c/goto-conversion/goto_check_c.h>
#include <ansi-c/goto-conversion/string_instrumentation.h>
#include "goto_check.h"

Include dependency graph for process_goto_program.cpp:

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...

Detailed Description

Get a Goto Program.

Definition in file process_goto_program.cpp.

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.