instrument_preconditions.cpp File Reference

#include "instrument_preconditions.h"
#include <util/replace_symbol.h>
#include "goto_model.h"

Include dependency graph for instrument_preconditions.cpp:

Go to the source code of this file.

Functions
std::vector< goto_programt::const_targett >	get_preconditions (const symbol_exprt &function, const goto_functionst &goto_functions)
void	remove_preconditions (goto_programt &goto_program)
replace_symbolt	actuals_replace_map (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, const namespacet &ns)
void	instrument_preconditions (const goto_modelt &goto_model, goto_programt &goto_program)
void	instrument_preconditions (goto_modelt &goto_model)
void	remove_preconditions (goto_functiont &goto_function)
void	remove_preconditions (goto_modelt &goto_model)

Function Documentation

actuals_replace_map()

replace_symbolt actuals_replace_map	(	const exprt &	lhs,
		const exprt &	function,
		const exprt::operandst &	arguments,
		const namespacet &	ns
	)

Definition at line 72 of file instrument_preconditions.cpp.

get_preconditions()

std::vector<goto_programt::const_targett> get_preconditions	(	const symbol_exprt &	function,
		const goto_functionst &	goto_functions
	)

Definition at line 18 of file instrument_preconditions.cpp.

instrument_preconditions() [1/2]

void instrument_preconditions	(	const goto_modelt &	goto_model,
		goto_programt &	goto_program
	)

Definition at line 99 of file instrument_preconditions.cpp.

instrument_preconditions() [2/2]

void instrument_preconditions

(

goto_modelt &

goto_model

)

Definition at line 143 of file instrument_preconditions.cpp.

remove_preconditions() [1/3]

void remove_preconditions

(

goto_functiont &

goto_function

)

Definition at line 162 of file instrument_preconditions.cpp.

remove_preconditions() [2/3]

void remove_preconditions

(

goto_modelt &

goto_model

)

Definition at line 167 of file instrument_preconditions.cpp.

remove_preconditions() [3/3]

void remove_preconditions

(

goto_programt &

goto_program

)

Definition at line 53 of file instrument_preconditions.cpp.