goto_inline_class.cpp File Reference

Function Inlining. More...

#include "goto_inline_class.h"
#include <cassert>
#include <util/prefix.h>
#include <util/cprover_prefix.h>
#include <util/base_type.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/expr_util.h>
#include "remove_skip.h"
#include "goto_inline.h"

Include dependency graph for goto_inline_class.cpp:

Go to the source code of this file.

Functions
void	replace_location (source_locationt &dest, const source_locationt &new_location)
void	replace_location (exprt &dest, const source_locationt &new_location)

Detailed Description

Function Inlining.

Definition in file goto_inline_class.cpp.

Function Documentation

replace_location() [1/2]

void replace_location	(	source_locationt &	dest,
		const source_locationt &	new_location
	)

Definition at line 319 of file goto_inline_class.cpp.

References comment(), dstringt::empty(), source_locationt::get_comment(), source_locationt::get_property_class(), source_locationt::get_property_id(), source_locationt::set_comment(), source_locationt::set_property_class(), and source_locationt::set_property_id().

Referenced by goto_inlinet::insert_function_body(), and replace_location().

replace_location() [2/2]

void replace_location	(	exprt &	dest,
		const source_locationt &	new_location
	)

Definition at line 342 of file goto_inline_class.cpp.

References exprt::add_source_location(), irept::find(), Forall_operands, irept::is_not_nil(), and replace_location().